awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
nv : ∀ {b : ℂ}, 0 < b.re → b ≠ 0
this : ∀ (x : ℝ), cexp (-1 * HPow.hPow (β := ℕ) (↑x : ℂ) 2) = (↑(rexp (-1 * HPow.hPow (β := ℕ) x 2)) : ℂ)
rw :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ rexp (-1 * HPow.hPow (β := ℕ) x 2)) =
    (π / 1) ^ HDiv.hDiv (α := ℝ) 1 2
hx : 0 ≤ π / 1
⊢ (↑(@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ rexp (-1 * HPow.hPow (β := ℕ) x 2)) : ℂ) =
    (↑(π / 1) : ℂ) ^ (↑(HDiv.hDiv (α := ℝ) 1 2) : ℂ)

Tactic:
rw [← ofReal_cpow, ofReal_inj]

Premises used: Complex.ofReal_cpow, Complex.ofReal_inj
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
nv : ∀ {b : ℂ}, 0 < b.re → b ≠ 0
this : ∀ (x : ℝ), cexp (-1 * HPow.hPow (β := ℕ) (↑x : ℂ) 2) = (↑(rexp (-1 * HPow.hPow (β := ℕ) x 2)) : ℂ)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ rexp (-1 * HPow.hPow (β := ℕ) x 2)) = √(π / 1)

Tactic:
integral_gaussian (1 : ℝ)

Premises used: integral_gaussian, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
nv : ∀ {b : ℂ}, 0 < b.re → b ≠ 0
this : ∀ (x : ℝ), cexp (-1 * HPow.hPow (β := ℕ) (↑x : ℂ) 2) = (↑(rexp (-1 * HPow.hPow (β := ℕ) x 2)) : ℂ)
h : (π / 1) ^ HDiv.hDiv (α := ℝ) 1 2 = √(π / 1)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ rexp (-1 * HPow.hPow (β := ℕ) x 2)) =
    (π / 1) ^ HDiv.hDiv (α := ℝ) 1 2

Tactic:
convert! integral_gaussian (1 : ℝ) using 1

Premises used: integral_gaussian, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
nv : ∀ {b : ℂ}, 0 < b.re → b ≠ 0
this : ∀ (x : ℝ), cexp (-1 * HPow.hPow (β := ℕ) (↑x : ℂ) 2) = (↑(rexp (-1 * HPow.hPow (β := ℕ) x 2)) : ℂ)
h h₁ : (π / 1) ^ HDiv.hDiv (α := ℝ) 1 2 = (π / 1) ^ (1 / 2)
⊢ (π / 1) ^ HDiv.hDiv (α := ℝ) 1 2 = √(π / 1)

Tactic:
rw [sqrt_eq_rpow]

Premises used: Real.sqrt_eq_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
nv : ∀ {b : ℂ}, 0 < b.re → b ≠ 0
this : ∀ (x : ℝ), cexp (-1 * HPow.hPow (β := ℕ) (↑x : ℂ) 2) = (↑(rexp (-1 * HPow.hPow (β := ℕ) x 2)) : ℂ)
hx : 0 ≤ π
⊢ 0 ≤ π / 1

Tactic:
rw [div_one]

Premises used: div_one
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
nv : ∀ {b : ℂ}, 0 < b.re → b ≠ 0
this : ∀ (x : ℝ), cexp (-1 * HPow.hPow (β := ℕ) (↑x : ℂ) 2) = (↑(rexp (-1 * HPow.hPow (β := ℕ) x 2)) : ℂ)
⊢ 0 ≤ π

Tactic:
pi_pos.le

Premises used: Real.pi_pos, LT.lt.le
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
nv : ∀ {b : ℂ}, 0 < b.re → b ≠ 0
this : ∀ (x : ℝ), cexp (-1 * HPow.hPow (β := ℕ) (↑x : ℂ) 2) = (↑(rexp (-1 * HPow.hPow (β := ℕ) x 2)) : ℂ)
⊢ 0 ≤ π

Tactic:
exact pi_pos.le

Premises used: Real.pi_pos, LT.lt.le
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
nv : ∀ {b : ℂ}, 0 < b.re → b ≠ 0
c : ℂ
hc : Membership.mem (γ := Set ℂ) {c : ℂ | 0 < c.re} c
rw : (↑π : ℂ) / c = ((↑π : ℂ) / c) ^ (1 / 2) * ((↑π : ℂ) / c) ^ (1 / 2)
⊢ HPow.hPow (α := ℂ) (β := ℕ)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ cexp (-c * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
      2 =
    HPow.hPow (β := ℕ) (((↑π : ℂ) / c) ^ (1 / 2)) 2

Tactic:
rw [integral_gaussian_sq_complex hc, sq]

Premises used: sq, integral_gaussian_sq_complex
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
nv : ∀ {b : ℂ}, 0 < b.re → b ≠ 0
c : ℂ
hc : Membership.mem (γ := Set ℂ) {c : ℂ | 0 < c.re} c
rw : HPow.hPow (β := ℂ) ((↑π : ℂ) / c) 1
| (↑π : ℂ) / c

Tactic:
rw [← cpow_one (↑π / c)]

Premises used: HDiv.hDiv, Complex.cpow_one
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
nv : ∀ {b : ℂ}, 0 < b.re → b ≠ 0
c : ℂ
hc : Membership.mem (γ := Set ℂ) {c : ℂ | 0 < c.re} c
conv_lhs : HPow.hPow (β := ℂ) ((↑π : ℂ) / c) 1 = ((↑π : ℂ) / c) ^ (1 / 2) * ((↑π : ℂ) / c) ^ (1 / 2)
⊢ (↑π : ℂ) / c = ((↑π : ℂ) / c) ^ (1 / 2) * ((↑π : ℂ) / c) ^ (1 / 2)

Tactic:
conv_lhs => rw [← cpow_one (↑π / c)]

Premises used: HDiv.hDiv, Complex.cpow_one
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
nv : ∀ {b : ℂ}, 0 < b.re → b ≠ 0
c : ℂ
hc : Membership.mem (γ := Set ℂ) {c : ℂ | 0 < c.re} c
rw : HPow.hPow (β := ℂ) ((↑π : ℂ) / c) 1 = ((↑π : ℂ) / c) ^ (1 / 2 + 1 / 2)
⊢ HPow.hPow (β := ℂ) ((↑π : ℂ) / c) 1 = ((↑π : ℂ) / c) ^ (1 / 2) * ((↑π : ℂ) / c) ^ (1 / 2)

Tactic:
rw [← cpow_add _ _ (div_ne_zero (ofReal_ne_zero.mpr pi_ne_zero) (nv hc))]

Premises used: Iff.mpr, Complex.ofReal_ne_zero, div_ne_zero, Complex.cpow_add, Real.pi_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
nv : ∀ {b : ℂ}, 0 < b.re → b ≠ 0
c : ℂ
hc : Membership.mem (γ := Set ℂ) {c : ℂ | 0 < c.re} c
⊢ HPow.hPow (β := ℂ) ((↑π : ℂ) / c) 1 = ((↑π : ℂ) / c) ^ (1 / 2 + 1 / 2)

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
nv : ∀ {b : ℂ}, 0 < b.re → b ≠ 0
c : ℂ
hc : Membership.mem (γ := Set ℂ) {c : ℂ | 0 < c.re} c
rw : ¬(↑π : ℂ) / c = 0 ∨ ¬1 / 2 ≠ 0
⊢ ((↑π : ℂ) / c) ^ (1 / 2) ≠ 0

Tactic:
rw [Ne, cpow_eq_zero_iff, not_and_or]

Premises used: Complex.cpow_eq_zero_iff, Ne, not_and_or
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
nv : ∀ {b : ℂ}, 0 < b.re → b ≠ 0
c : ℂ
hc : Membership.mem (γ := Set ℂ) {c : ℂ | 0 < c.re} c
⊢ ¬(↑π : ℂ) / c = 0 ∨ ¬1 / 2 ≠ 0

Tactic:
Or.inl (div_ne_zero (ofReal_ne_zero.mpr pi_ne_zero) (nv hc))

Premises used: Iff.mpr, Complex.ofReal_ne_zero, div_ne_zero, Or.inl, Real.pi_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
nv : ∀ {b : ℂ}, 0 < b.re → b ≠ 0
c : ℂ
hc : Membership.mem (γ := Set ℂ) {c : ℂ | 0 < c.re} c
⊢ ¬(↑π : ℂ) / c = 0 ∨ ¬1 / 2 ≠ 0

Tactic:
exact Or.inl (div_ne_zero (ofReal_ne_zero.mpr pi_ne_zero) (nv hc))

Premises used: Iff.mpr, Complex.ofReal_ne_zero, div_ne_zero, Or.inl, Real.pi_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) =
    ((↑π : ℂ) / b) ^ (1 / 2)

Tactic:
have full_integral := integral_gaussian_complex hb
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
full_integral :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) =
    ((↑π : ℂ) / b) ^ (1 / 2)
⊢ MeasurableSet (α := ℝ) (Ioi 0)

Tactic:
have : MeasurableSet (Ioi (0 : ℝ)) := measurableSet_Ioi
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
full_integral :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) =
    ((↑π : ℂ) / b) ^ (1 / 2)
this : MeasurableSet (α := ℝ) (Ioi 0)
⊢ HAdd.hAdd (α := ℂ)
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Iic 0)) fun (x : ℝ) ↦
        cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) =
    ((↑π : ℂ) / b) ^ (1 / 2)

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

Premises used: MeasureTheory.integral_add_compl, Set.compl_Ioi, integrable_cexp_neg_mul_sq
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
full_integral :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) =
    ((↑π : ℂ) / b) ^ (1 / 2)
this : MeasurableSet (α := ℝ) (Ioi 0)
full_integral₁ :
  HAdd.hAdd (α := ℂ)
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Iic 0)) fun (x : ℝ) ↦
        cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) =
    ((↑π : ℂ) / b) ^ (1 / 2)
⊢ MeasurableSet (α := ℝ) (Ioi 0)

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

Premises used: MeasureTheory.integral_add_compl, Set.compl_Ioi, integrable_cexp_neg_mul_sq
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
full_integral :
  HAdd.hAdd (α := ℂ)
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Iic 0)) fun (x : ℝ) ↦
        cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) =
    ((↑π : ℂ) / b) ^ (1 / 2)
this_1 : MeasurableSet (α := ℝ) (Ioi 0)
this :
  Eq (α := ℂ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic 0)) fun (x : ℝ) ↦
      cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
⊢ HMul.hMul (α := ℂ)
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
      2 =
    ((↑π : ℂ) / b) ^ (1 / 2)

Tactic:
rw [this, ← mul_two] at full_integral

Premises used: mul_two
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
full_integral :
  HAdd.hAdd (α := ℂ)
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Iic 0)) fun (x : ℝ) ↦
        cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) =
    ((↑π : ℂ) / b) ^ (1 / 2)
this_1 : MeasurableSet (α := ℝ) (Ioi 0)
this :
  Eq (α := ℂ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic 0)) fun (x : ℝ) ↦
      cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
full_integral₁ :
  HMul.hMul (α := ℂ)
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
      2 =
    ((↑π : ℂ) / b) ^ (1 / 2)
⊢ MeasurableSet (α := ℝ) (Ioi 0)

Tactic:
rw [this, ← mul_two] at full_integral

Premises used: mul_two
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
full_integral :
  HAdd.hAdd (α := ℂ)
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Iic 0)) fun (x : ℝ) ↦
        cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) =
    ((↑π : ℂ) / b) ^ (1 / 2)
this_1 : MeasurableSet (α := ℝ) (Ioi 0)
this :
  Eq (α := ℂ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic 0)) fun (x : ℝ) ↦
      cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
full_integral₁ :
  HMul.hMul (α := ℂ)
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
      2 =
    ((↑π : ℂ) / b) ^ (1 / 2)
this₁ : MeasurableSet (α := ℝ) (Ioi 0)
⊢ Eq (α := ℂ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic 0)) fun (x : ℝ) ↦
      cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))

Tactic:
rw [this, ← mul_two] at full_integral

Premises used: mul_two
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
full_integral :
  HMul.hMul (α := ℂ)
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
      2 =
    ((↑π : ℂ) / b) ^ (1 / 2)
this_1 : MeasurableSet (α := ℝ) (Ioi 0)
this :
  Eq (α := ℂ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic 0)) fun (x : ℝ) ↦
      cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
rwa : Ne (α := ℂ) 2 0
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) =
    ((↑π : ℂ) / b) ^ (1 / 2) / 2

Tactic:
rwa [eq_div_iff]

Premises used: eq_div_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
full_integral :
  HMul.hMul (α := ℂ)
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
      2 =
    ((↑π : ℂ) / b) ^ (1 / 2)
this_1 : MeasurableSet (α := ℝ) (Ioi 0)
this :
  Eq (α := ℂ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic 0)) fun (x : ℝ) ↦
      cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
⊢ Ne (α := ℂ) 2 0

Tactic:
two_ne_zero

Premises used: two_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
full_integral :
  HMul.hMul (α := ℂ)
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
      2 =
    ((↑π : ℂ) / b) ^ (1 / 2)
this_1 : MeasurableSet (α := ℝ) (Ioi 0)
this :
  Eq (α := ℂ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic 0)) fun (x : ℝ) ↦
      cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
⊢ Ne (α := ℂ) 2 0

Tactic:
exact two_ne_zero

Premises used: two_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
full_integral :
  HAdd.hAdd (α := ℂ)
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Iic 0)) fun (x : ℝ) ↦
        cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) =
    ((↑π : ℂ) / b) ^ (1 / 2)
this : MeasurableSet (α := ℝ) (Ioi 0)
suffices :
  Eq (α := ℂ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic 0)) fun (x : ℝ) ↦
      cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      cexp (-b * HPow.hPow (β := ℕ) (↑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
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
full_integral :
  HAdd.hAdd (α := ℂ)
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Iic 0)) fun (x : ℝ) ↦
        cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) =
    ((↑π : ℂ) / b) ^ (1 / 2)
this : MeasurableSet (α := ℝ) (Ioi 0)
c : ℝ
⊢ Eq (α := ℂ) (∫ (x : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) (↑(0 - x) : ℂ) 2))
    (∫ (x : ℝ) in 0 - c..HSub.hSub (α := ℝ) 0 0, cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))

Tactic:
have := intervalIntegral.integral_comp_sub_left (a := 0) (b := c)
      (fun x => cexp (-b * (x : ℂ) ^ 2)) 0
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
full_integral :
  HAdd.hAdd (α := ℂ)
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Iic 0)) fun (x : ℝ) ↦
        cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) =
    ((↑π : ℂ) / b) ^ (1 / 2)
this_1 : MeasurableSet (α := ℝ) (Ioi 0)
c : ℝ
this :
  Eq (α := ℂ) (∫ (x : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) (↑(0 - x) : ℂ) 2))
    (∫ (x : ℝ) in 0 - c..HSub.hSub (α := ℝ) 0 0, cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
⊢ Eq (α := ℂ) (∫ (x : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
    (∫ (x : ℝ) in -c..0, cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))

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

Premises used: neg_sq, neg_zero, zero_sub
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
full_integral :
  HAdd.hAdd (α := ℂ)
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Iic 0)) fun (x : ℝ) ↦
        cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) =
    ((↑π : ℂ) / b) ^ (1 / 2)
this : MeasurableSet (α := ℝ) (Ioi 0)
⊢ ∀ (c : ℝ),
    Eq (α := ℂ) (∫ (x : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
      (∫ (x : ℝ) in -c..0, cexp (-b * HPow.hPow (β := ℕ) (↑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
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
full_integral :
  HAdd.hAdd (α := ℂ)
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Iic 0)) fun (x : ℝ) ↦
        cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) =
    ((↑π : ℂ) / b) ^ (1 / 2)
this_1 : MeasurableSet (α := ℝ) (Ioi 0)
this :
  ∀ (c : ℝ),
    Eq (α := ℂ) (∫ (x : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
      (∫ (x : ℝ) in -c..0, cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
⊢ Tendsto (β := ℂ) (fun (i : ℝ) ↦ ∫ (x : ℝ) in 0..id i, cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) atTop
    (𝓝
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)))

Tactic:
have t1 :=
    intervalIntegral_tendsto_integral_Ioi 0 (integrable_cexp_neg_mul_sq hb).integrableOn tendsto_id
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
full_integral :
  HAdd.hAdd (α := ℂ)
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Iic 0)) fun (x : ℝ) ↦
        cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) =
    ((↑π : ℂ) / b) ^ (1 / 2)
this_1 : MeasurableSet (α := ℝ) (Ioi 0)
this :
  ∀ (c : ℝ),
    Eq (α := ℂ) (∫ (x : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
      (∫ (x : ℝ) in -c..0, cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
t1 :
  Tendsto (β := ℂ) (fun (i : ℝ) ↦ ∫ (x : ℝ) in 0..id i, cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) atTop
    (𝓝
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)))
simp_rw :
  Tendsto (β := ℂ) (fun (c : ℝ) ↦ ∫ (x : ℝ) in -c..0, cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) atTop
    (𝓝
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic 0)) fun (x : ℝ) ↦
        cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)))
⊢ Tendsto (β := ℂ) (fun (c : ℝ) ↦ ∫ (x : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) atTop
    (𝓝
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic 0)) fun (x : ℝ) ↦
        cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)))

Tactic:
simp_rw [this]
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
full_integral :
  HAdd.hAdd (α := ℂ)
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Iic 0)) fun (x : ℝ) ↦
        cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) =
    ((↑π : ℂ) / b) ^ (1 / 2)
this_1 : MeasurableSet (α := ℝ) (Ioi 0)
this :
  ∀ (c : ℝ),
    Eq (α := ℂ) (∫ (x : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
      (∫ (x : ℝ) in -c..0, cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
t1 :
  Tendsto (β := ℂ) (fun (i : ℝ) ↦ ∫ (x : ℝ) in 0..id i, cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) atTop
    (𝓝
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)))
⊢ Tendsto (β := ℂ) (fun (c : ℝ) ↦ ∫ (x : ℝ) in -c..0, cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) atTop
    (𝓝
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic 0)) fun (x : ℝ) ↦
        cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)))

Tactic:
intervalIntegral_tendsto_integral_Iic _ ?_ tendsto_neg_atTop_atBot

Premises used: MeasureTheory.intervalIntegral_tendsto_integral_Iic, Filter.tendsto_neg_atTop_atBot
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Goal:
b : ℂ
hb : 0 < b.re
full_integral :
  HAdd.hAdd (α := ℂ)
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Iic 0)) fun (x : ℝ) ↦
        cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) =
    ((↑π : ℂ) / b) ^ (1 / 2)
this_1 : MeasurableSet (α := ℝ) (Ioi 0)
this :
  ∀ (c : ℝ),
    Eq (α := ℂ) (∫ (x : ℝ) in 0..c, cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
      (∫ (x : ℝ) in -c..0, cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
t1 :
  Tendsto (β := ℂ) (fun (i : ℝ) ↦ ∫ (x : ℝ) in 0..id i, cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) atTop
    (𝓝
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)))
refine :
  IntegrableOn (ε := ℂ) (mα := Real.measurableSpace) (fun (x : ℝ) ↦ cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) (Iic 0)
    volume
⊢ Tendsto (β := ℂ) (fun (c : ℝ) ↦ ∫ (x : ℝ) in -c..0, cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) atTop
    (𝓝
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic 0)) fun (x : ℝ) ↦
        cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)))

Tactic:
refine intervalIntegral_tendsto_integral_Iic _ ?_ tendsto_neg_atTop_atBot

Premises used: MeasureTheory.intervalIntegral_tendsto_integral_Iic, Filter.tendsto_neg_atTop_atBot