-- 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)
t1 :
  Tendsto (fun i => ∫ (x : ℝ) in 0 ..id i, cexp (-b * ↑x ^ 2)) atTop
    (𝓝 (∫ (x : ℝ) in Ioi 0, cexp (-b * ↑x ^ 2) ∂volume))
t2 : Tendsto (fun c => ∫ (x : ℝ) in 0 ..c, cexp (-b * ↑x ^ 2)) atTop (𝓝 (∫ (x : ℝ) in Iic 0, cexp (-b * ↑x ^ 2)))
⊢ ∫ (x : ℝ) in Iic 0, cexp (-b * ↑x ^ 2) = ∫ (x : ℝ) in Ioi 0, cexp (-b * ↑x ^ 2)

Tactic:
exact tendsto_nhds_unique t2 t1

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)
c : ℝ
⊢ ∫ (x : ℝ) in 0 ..c, cexp (-b * ↑x ^ 2) = ∫ (x : ℝ) in -c..0, cexp (-b * ↑x ^ 2)

Tactic:
have := intervalIntegral.integral_comp_sub_left (a := 0) (b := c)
  (fun x => cexp (-b * (x : ℂ) ^ 2)) 0

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)
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)

Proof state:
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)
⊢ 2 ≠ 0

Tactic:
exact two_ne_zero

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)
⊢ ∫ (x : ℝ) in Ioi 0, cexp (-b * ↑x ^ 2) = (↑π / b) ^ (1 / 2) / 2

Tactic:
suffices ∫ x : ℝ in Iic 0, cexp (-b * (x : ℂ) ^ 2) = ∫ x : ℝ in Ioi 0, cexp (-b * (x : ℂ) ^ 2) by
  rw [this, ← mul_two] at full_integral
  rwa [eq_div_iff]; exact two_ne_zero

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)
⊢ ∫ (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) * 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

Tactic:
rwa [eq_div_iff]

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)
⊢ 2 ≠ 0

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 : ℝ), ∫ (x : ℝ) in 0 ..c, cexp (-b * ↑x ^ 2) = ∫ (x : ℝ) in -c..0, cexp (-b * ↑x ^ 2)

Tactic:
intro c

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)
c : ℝ
⊢ ∫ (x : ℝ) in 0 ..c, cexp (-b * ↑x ^ 2) = ∫ (x : ℝ) in -c..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)
⊢ ∫ (x : ℝ) in Iic 0, cexp (-b * ↑x ^ 2) = ∫ (x : ℝ) in Ioi 0, cexp (-b * ↑x ^ 2)

Tactic:
have : ∀ c : ℝ, ∫ x in (0 : ℝ)..c, cexp (-b * (x : ℂ) ^ 2) =
    ∫ x in -c..0, cexp (-b * (x : ℂ) ^ 2) := by
  intro c
  have := intervalIntegral.integral_comp_sub_left (a := 0) (b := c)
    (fun x => cexp (-b * (x : ℂ) ^ 2)) 0
  simpa [zero_sub, neg_sq, neg_zero] using this

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)
⊢ ∫ (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)
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)

Tactic:
have t2 :
  Tendsto (fun c : ℝ => ∫ x : ℝ in (0 : ℝ)..c, cexp (-b * (x : ℂ) ^ 2)) atTop
    (𝓝 (∫ x : ℝ in Iic 0, cexp (-b * (x : ℂ) ^ 2))) := by
  simp_rw [this]
  refine intervalIntegral_tendsto_integral_Iic _ ?_ tendsto_neg_atTop_atBot
  apply (integrable_cexp_neg_mul_sq hb).integrableOn

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))
t2 : Tendsto (fun c => ∫ (x : ℝ) in 0 ..c, cexp (-b * ↑x ^ 2)) atTop (𝓝 (∫ (x : ℝ) in Iic 0, cexp (-b * ↑x ^ 2)))
⊢ ∫ (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 : ℝ), cexp (-b * ↑x ^ 2) = (↑π / b) ^ (1 / 2)
this : MeasurableSet (Ioi 0)
⊢ ∫ (x : ℝ) in Ioi 0, cexp (-b * ↑x ^ 2) = (↑π / b) ^ (1 / 2) / 2

Tactic:
rw [← integral_add_compl this (integrable_cexp_neg_mul_sq hb), compl_Ioi] at full_integral

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)
⊢ ∫ (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 0 ..c, cexp (-b * ↑x ^ 2)) atTop (𝓝 (∫ (x : ℝ) in Iic 0, cexp (-b * ↑x ^ 2)))

Tactic:
simp_rw [this]

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))
⊢ Tendsto (fun c => ∫ (x : ℝ) in -c..0, cexp (-b * ↑x ^ 2)) atTop (𝓝 (∫ (x : ℝ) in Iic 0, cexp (-b * ↑x ^ 2)))