Theorem: DiracSeq.integral (ForML/Dirac.lean)

State before:
b : ℝ
hb : 0 < b
⊢ ∫ (x : ℝ), DiracSeq b x = 1
Tactic:
simp [DiracSeq]
State after:
b : ℝ
hb : 0 < b
⊢ ∫ (x : ℝ), b / sqrt π * rexp (-(b * x) ^ 2) = 1

State before:
b : ℝ
hb : 0 < b
⊢ ∫ (x : ℝ), b / sqrt π * rexp (-(b * x) ^ 2) = 1
Tactic:
simp [integral_mul_left]
State after:
b : ℝ
hb : 0 < b
⊢ b / sqrt π * ∫ (a : ℝ), rexp (-(b * a) ^ 2) = 1

State before:
b : ℝ
hb : 0 < b
⊢ b / sqrt π * ∫ (a : ℝ), rexp (-(b * a) ^ 2) = 1
Tactic:
simp [mul_pow]
State after:
b : ℝ
hb : 0 < b
⊢ b / sqrt π * ∫ (a : ℝ), rexp (-(b ^ 2 * a ^ 2)) = 1

State before:
b : ℝ
hb : 0 < b
⊢ b / sqrt π * ∫ (a : ℝ), rexp (-(b ^ 2 * a ^ 2)) = 1
Tactic:
have h := integral_gaussian
State after:
b : ℝ
hb : 0 < b
h : ∀ (b : ℝ), ∫ (x : ℝ), rexp (-b * x ^ 2) = sqrt (π / b)
⊢ b / sqrt π * ∫ (a : ℝ), rexp (-(b ^ 2 * a ^ 2)) = 1

State before:
b : ℝ
hb : 0 < b
h : ∀ (b : ℝ), ∫ (x : ℝ), rexp (-b * x ^ 2) = sqrt (π / b)
⊢ b / sqrt π * ∫ (a : ℝ), rexp (-(b ^ 2 * a ^ 2)) = 1
Tactic:
simp at h
State after:
b : ℝ
hb : 0 < b
h : ∀ (b : ℝ), ∫ (x : ℝ), rexp (-(b * x ^ 2)) = sqrt (π / b)
⊢ b / sqrt π * ∫ (a : ℝ), rexp (-(b ^ 2 * a ^ 2)) = 1

State before:
b : ℝ
hb : 0 < b
h : ∀ (b : ℝ), ∫ (x : ℝ), rexp (-(b * x ^ 2)) = sqrt (π / b)
⊢ b / sqrt π * ∫ (a : ℝ), rexp (-(b ^ 2 * a ^ 2)) = 1
Tactic:
simp [h]
State after:
b : ℝ
hb : 0 < b
h : ∀ (b : ℝ), ∫ (x : ℝ), rexp (-(b * x ^ 2)) = sqrt (π / b)
⊢ b / sqrt π * sqrt (π / b ^ 2) = 1

State before:
b : ℝ
hb : 0 < b
h : ∀ (b : ℝ), ∫ (x : ℝ), rexp (-(b * x ^ 2)) = sqrt (π / b)
⊢ b / sqrt π * sqrt (π / b ^ 2) = 1
Tactic:
clear h
State after:
b : ℝ
hb : 0 < b
⊢ b / sqrt π * sqrt (π / b ^ 2) = 1

State before:
b : ℝ
hb : 0 < b
⊢ b / sqrt π * sqrt (π / b ^ 2) = 1
Tactic:
rw [sqrt_div pi_pos.le]
State after:
b : ℝ
hb : 0 < b
⊢ b / sqrt π * (sqrt π / sqrt (b ^ 2)) = 1

State before:
b : ℝ
hb : 0 < b
⊢ b / sqrt π * (sqrt π / sqrt (b ^ 2)) = 1
Tactic:
rw [sqrt_sq hb.le]
State after:
b : ℝ
hb : 0 < b
⊢ b / sqrt π * (sqrt π / b) = 1

State before:
b : ℝ
hb : 0 < b
⊢ b / sqrt π * (sqrt π / b) = 1
Tactic:
rw [div_mul_div_comm]
State after:
b : ℝ
hb : 0 < b
⊢ b * sqrt π / (sqrt π * b) = 1

State before:
b : ℝ
hb : 0 < b
⊢ b * sqrt π / (sqrt π * b) = 1
Tactic:
rw [mul_comm]
State after:
b : ℝ
hb : 0 < b
⊢ sqrt π * b / (sqrt π * b) = 1

State before:
b : ℝ
hb : 0 < b
⊢ sqrt π * b / (sqrt π * b) = 1
Tactic:
rw [div_self]
State after:
b : ℝ
hb : 0 < b
⊢ sqrt π * b ≠ 0

State before:
b : ℝ
hb : 0 < b
⊢ sqrt π * b ≠ 0
Tactic:
apply ne_of_gt
State after:
case h
b : ℝ
hb : 0 < b
⊢ 0 < sqrt π * b

State before:
case h
b : ℝ
hb : 0 < b
⊢ 0 < sqrt π * b
Tactic:
exact mul_pos sqrt_pi_pos hb
State after:
no goals