-- Mathlib/Analysis/SpecialFunctions/Gaussian/GaussianIntegral.lean
theorem integral_gaussian_complex_Ioi {b : ℂ} (hb : 0 < re b) :
    ∫ x : ℝ in Ioi 0, cexp (-b * (x : ℂ) ^ 2) = (π / b) ^ (1 / 2 : ℂ) / 2

Proof state:
b : ℂ
hb : 0 < b.re
full_integral :
  ∫ (x : ℝ) in Ioi 0, cexp (-b * ↑x ^ 2) ∂volume + ∫ (x : ℝ) in Iic 0, cexp (-b * ↑x ^ 2) ∂volume = (↑π / b) ^ (1 / 2)
this✝ : MeasurableSet (Ioi 0)
this : ∀ (c : ℝ), ∫ (x : ℝ) in 0 ..c, cexp (-b * ↑x ^ 2) = ∫ (x : ℝ) in -c..0, cexp (-b * ↑x ^ 2)
⊢ ∫ (x : ℝ) in Iic 0, cexp (-b * ↑x ^ 2) = ∫ (x : ℝ) in Ioi 0, cexp (-b * ↑x ^ 2)

Tactic:
have t1 :=
  intervalIntegral_tendsto_integral_Ioi 0 (integrable_cexp_neg_mul_sq hb).integrableOn tendsto_id

Result:
b : ℂ
hb : 0 < b.re
full_integral :
  ∫ (x : ℝ) in Ioi 0, cexp (-b * ↑x ^ 2) ∂volume + ∫ (x : ℝ) in Iic 0, cexp (-b * ↑x ^ 2) ∂volume = (↑π / b) ^ (1 / 2)
this✝ : MeasurableSet (Ioi 0)
this : ∀ (c : ℝ), ∫ (x : ℝ) in 0 ..c, cexp (-b * ↑x ^ 2) = ∫ (x : ℝ) in -c..0, cexp (-b * ↑x ^ 2)
t1 :
  Tendsto (fun i => ∫ (x : ℝ) in 0 ..id i, cexp (-b * ↑x ^ 2)) atTop
    (𝓝 (∫ (x : ℝ) in Ioi 0, cexp (-b * ↑x ^ 2) ∂volume))
⊢ ∫ (x : ℝ) in Iic 0, cexp (-b * ↑x ^ 2) = ∫ (x : ℝ) in Ioi 0, cexp (-b * ↑x ^ 2)

Proof state:
b : ℂ
hb : 0 < b.re
full_integral :
  ∫ (x : ℝ) in Ioi 0, cexp (-b * ↑x ^ 2) ∂volume + ∫ (x : ℝ) in Iic 0, cexp (-b * ↑x ^ 2) ∂volume = (↑π / b) ^ (1 / 2)
this✝ : MeasurableSet (Ioi 0)
c : ℝ
this : ∫ (x : ℝ) in 0 ..c, cexp (-b * ↑(0 - x) ^ 2) = ∫ (x : ℝ) in 0 - c..0 - 0, cexp (-b * ↑x ^ 2)
⊢ ∫ (x : ℝ) in 0 ..c, cexp (-b * ↑x ^ 2) = ∫ (x : ℝ) in -c..0, cexp (-b * ↑x ^ 2)

Tactic:
simpa [zero_sub, neg_sq, neg_zero] using this

Result:
no goals

Proof state:
b : ℂ
hb : 0 < b.re
⊢ ∫ (x : ℝ) in Ioi 0, cexp (-b * ↑x ^ 2) = (↑π / b) ^ (1 / 2) / 2

Tactic:
have full_integral := integral_gaussian_complex hb

Result:
b : ℂ
hb : 0 < b.re
full_integral : ∫ (x : ℝ), cexp (-b * ↑x ^ 2) = (↑π / b) ^ (1 / 2)
⊢ ∫ (x : ℝ) in Ioi 0, cexp (-b * ↑x ^ 2) = (↑π / b) ^ (1 / 2) / 2

Proof state:
b : ℂ
hb : 0 < b.re
full_integral :
  ∫ (x : ℝ) in Ioi 0, cexp (-b * ↑x ^ 2) ∂volume + ∫ (x : ℝ) in Iic 0, cexp (-b * ↑x ^ 2) ∂volume = (↑π / b) ^ (1 / 2)
this✝ : MeasurableSet (Ioi 0)
this : ∀ (c : ℝ), ∫ (x : ℝ) in 0 ..c, cexp (-b * ↑x ^ 2) = ∫ (x : ℝ) in -c..0, cexp (-b * ↑x ^ 2)
t1 :
  Tendsto (fun i => ∫ (x : ℝ) in 0 ..id i, cexp (-b * ↑x ^ 2)) atTop
    (𝓝 (∫ (x : ℝ) in Ioi 0, cexp (-b * ↑x ^ 2) ∂volume))
⊢ IntegrableOn (fun x => cexp (-b * ↑x ^ 2)) (Iic 0) volume

Tactic:
apply (integrable_cexp_neg_mul_sq hb).integrableOn

Result:
no goals

Proof state:
b : ℂ
hb : 0 < b.re
full_integral :
  ∫ (x : ℝ) in Ioi 0, cexp (-b * ↑x ^ 2) ∂volume + ∫ (x : ℝ) in Iic 0, cexp (-b * ↑x ^ 2) ∂volume = (↑π / b) ^ (1 / 2)
this✝ : MeasurableSet (Ioi 0)
this : ∫ (x : ℝ) in Iic 0, cexp (-b * ↑x ^ 2) = ∫ (x : ℝ) in Ioi 0, cexp (-b * ↑x ^ 2)
⊢ ∫ (x : ℝ) in Ioi 0, cexp (-b * ↑x ^ 2) = (↑π / b) ^ (1 / 2) / 2

Tactic:
rw [this, ← mul_two] at full_integral

Result:
b : ℂ
hb : 0 < b.re
full_integral : (∫ (x : ℝ) in Ioi 0, cexp (-b * ↑x ^ 2) ∂volume) * 2 = (↑π / b) ^ (1 / 2)
this✝ : MeasurableSet (Ioi 0)
this : ∫ (x : ℝ) in Iic 0, cexp (-b * ↑x ^ 2) = ∫ (x : ℝ) in Ioi 0, cexp (-b * ↑x ^ 2)
⊢ ∫ (x : ℝ) in Ioi 0, cexp (-b * ↑x ^ 2) = (↑π / b) ^ (1 / 2) / 2

Proof state:
b : ℂ
hb : 0 < b.re
full_integral : ∫ (x : ℝ), cexp (-b * ↑x ^ 2) = (↑π / b) ^ (1 / 2)
⊢ ∫ (x : ℝ) in Ioi 0, cexp (-b * ↑x ^ 2) = (↑π / b) ^ (1 / 2) / 2

Tactic:
have : MeasurableSet (Ioi (0 : ℝ)) := measurableSet_Ioi

Result:
b : ℂ
hb : 0 < b.re
full_integral : ∫ (x : ℝ), cexp (-b * ↑x ^ 2) = (↑π / b) ^ (1 / 2)
this : MeasurableSet (Ioi 0)
⊢ ∫ (x : ℝ) in Ioi 0, cexp (-b * ↑x ^ 2) = (↑π / b) ^ (1 / 2) / 2

Proof state:
b : ℂ
hb : 0 < b.re
full_integral :
  ∫ (x : ℝ) in Ioi 0, cexp (-b * ↑x ^ 2) ∂volume + ∫ (x : ℝ) in Iic 0, cexp (-b * ↑x ^ 2) ∂volume = (↑π / b) ^ (1 / 2)
this✝ : MeasurableSet (Ioi 0)
this : ∀ (c : ℝ), ∫ (x : ℝ) in 0 ..c, cexp (-b * ↑x ^ 2) = ∫ (x : ℝ) in -c..0, cexp (-b * ↑x ^ 2)
t1 :
  Tendsto (fun i => ∫ (x : ℝ) in 0 ..id i, cexp (-b * ↑x ^ 2)) atTop
    (𝓝 (∫ (x : ℝ) in Ioi 0, cexp (-b * ↑x ^ 2) ∂volume))
⊢ Tendsto (fun c => ∫ (x : ℝ) in -c..0, cexp (-b * ↑x ^ 2)) atTop (𝓝 (∫ (x : ℝ) in Iic 0, cexp (-b * ↑x ^ 2)))

Tactic:
refine intervalIntegral_tendsto_integral_Iic _ ?_ tendsto_neg_atTop_atBot

Result:
b : ℂ
hb : 0 < b.re
full_integral :
  ∫ (x : ℝ) in Ioi 0, cexp (-b * ↑x ^ 2) ∂volume + ∫ (x : ℝ) in Iic 0, cexp (-b * ↑x ^ 2) ∂volume = (↑π / b) ^ (1 / 2)
this✝ : MeasurableSet (Ioi 0)
this : ∀ (c : ℝ), ∫ (x : ℝ) in 0 ..c, cexp (-b * ↑x ^ 2) = ∫ (x : ℝ) in -c..0, cexp (-b * ↑x ^ 2)
t1 :
  Tendsto (fun i => ∫ (x : ℝ) in 0 ..id i, cexp (-b * ↑x ^ 2)) atTop
    (𝓝 (∫ (x : ℝ) in Ioi 0, cexp (-b * ↑x ^ 2) ∂volume))
⊢ IntegrableOn (fun x => cexp (-b * ↑x ^ 2)) (Iic 0) volume