awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (hypothesis)
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)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) =
    ((↑π : ℂ) / b) ^ (1 / 2) / 2
have 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)
Tactic: rw [← integral_add_compl this (integrable_cexp_neg_mul_sq hb), compl_Ioi] at full_integral
Cleared hypotheses: full_integral, this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (hypothesis)
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))
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) =
    ((↑π : ℂ) / b) ^ (1 / 2) / 2
have full_integral₁ : 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
Cleared hypotheses: full_integral, this_1, this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
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))
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) =
    ((↑π : ℂ) / b) ^ (1 / 2) / 2
have rwa : Ne (α := ℂ) 2 0
Tactic: rwa [eq_div_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
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)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) =
    ((↑π : ℂ) / b) ^ (1 / 2) / 2
have 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))
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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (hypothesis)
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))
have 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))
Tactic: have := intervalIntegral.integral_comp_sub_left (a := 0) (b := c)
      (fun x => cexp (-b * (x : ℂ) ^ 2)) 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (hypothesis)
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)
⊢ 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))
have this₁ : ∀ (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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (hypothesis)
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))
⊢ 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))
have 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)))
Tactic: have t1 :=
    intervalIntegral_tendsto_integral_Ioi 0 (integrable_cexp_neg_mul_sq hb).integrableOn tendsto_id
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
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 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)))
have 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)))
Tactic: simp_rw [this]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
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)))
have refine : IntegrableOn (ε := ℂ) (mα := Real.measurableSpace) (fun (x : ℝ) ↦ cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) (Iic 0)
  volume
Tactic: refine intervalIntegral_tendsto_integral_Iic _ ?_ tendsto_neg_atTop_atBot
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (hypothesis)
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)))
⊢ 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))
have t2 : 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: 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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℝ
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      rexp (-b * HPow.hPow (β := ℕ) x 2)) =
    √(π / b) / 2
have inl : ∀ (hb : b ≤ 0),
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      rexp (-b * HPow.hPow (β := ℕ) x 2)) =
    √(π / b) / 2
Tactic: rcases le_or_gt b 0 with (hb | hb)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℝ
inl :
  ∀ (hb : b ≤ 0),
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        rexp (-b * HPow.hPow (β := ℕ) x 2)) =
      √(π / b) / 2
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      rexp (-b * HPow.hPow (β := ℕ) x 2)) =
    √(π / b) / 2
have inr : ∀ (hb : 0 < b),
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      rexp (-b * HPow.hPow (β := ℕ) x 2)) =
    √(π / b) / 2
Tactic: rcases le_or_gt b 0 with (hb | hb)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℝ
hb : b ≤ 0
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      rexp (-b * HPow.hPow (β := ℕ) x 2)) =
    √(π / b) / 2
have inl : π / b ≤ 0
Tactic: rw [integral_undef, sqrt_eq_zero_of_nonpos, zero_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℝ
hb : b ≤ 0
inl : π / b ≤ 0
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      rexp (-b * HPow.hPow (β := ℕ) x 2)) =
    √(π / b) / 2
have inl₁ : ¬@Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ rexp (-b * HPow.hPow (β := ℕ) x 2))
    (Measure.restrict volume (Ioi 0))
Tactic: rw [integral_undef, sqrt_eq_zero_of_nonpos, zero_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℝ
hb : b ≤ 0
⊢ ¬@Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ rexp (-b * HPow.hPow (β := ℕ) x 2))
      (Measure.restrict volume (Ioi 0))
have inl : ¬IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ rexp (-b * HPow.hPow (β := ℕ) x 2)) (Ioi 0)
    volume
Tactic: rwa [← IntegrableOn, integrableOn_Ioi_exp_neg_mul_sq_iff, not_lt]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℝ
hb : b ≤ 0
inl :
  ¬IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ rexp (-b * HPow.hPow (β := ℕ) x 2))
      (Ioi 0) volume
⊢ ¬@Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ rexp (-b * HPow.hPow (β := ℕ) x 2))
      (Measure.restrict volume (Ioi 0))
have inl₁ : ¬0 < b
Tactic: rwa [← IntegrableOn, integrableOn_Ioi_exp_neg_mul_sq_iff, not_lt]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℝ
hb : 0 < b
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      rexp (-b * HPow.hPow (β := ℕ) x 2)) =
    √(π / b) / 2
have inr : (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
    (↑(rexp (-b * HPow.hPow (β := ℕ) x 2)) : ℂ)) =
  (↑(√(π / b) / 2) : ℂ)
Tactic: rw [← RCLike.ofReal_inj (K := ℂ), ← integral_ofReal, ← RCLike.algebraMap_eq_ofReal,
    coe_algebraMap]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℝ
hb : 0 < b
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      (↑(rexp (-b * HPow.hPow (β := ℕ) x 2)) : ℂ)) =
    (↑(√(π / b) / 2) : ℂ)
have h : ∀ (x : ℝ), (↑(rexp (-b * HPow.hPow (β := ℕ) x 2)) : ℂ) = cexp (-(↑b : ℂ) * HPow.hPow (β := ℕ) (↑x : ℂ) 2)
Tactic: convert! integral_gaussian_complex_Ioi (by rwa [ofReal_re] : 0 < (b : ℂ).re)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℝ
hb : 0 < b
h : ∀ (x : ℝ), (↑(rexp (-b * HPow.hPow (β := ℕ) x 2)) : ℂ) = cexp (-(↑b : ℂ) * HPow.hPow (β := ℕ) (↑x : ℂ) 2)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      (↑(rexp (-b * HPow.hPow (β := ℕ) x 2)) : ℂ)) =
    (↑(√(π / b) / 2) : ℂ)
have h₁ : (↑(√(π / b) / 2) : ℂ) = ((↑π : ℂ) / (↑b : ℂ)) ^ (1 / 2) / 2
Tactic: convert! integral_gaussian_complex_Ioi (by rwa [ofReal_re] : 0 < (b : ℂ).re)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℝ
hb : 0 < b
⊢ (↑(√(π / b) / 2) : ℂ) = ((↑π : ℂ) / (↑b : ℂ)) ^ (1 / 2) / 2
have h : (↑(π / b) : ℂ) ^ (↑(1 / 2) : ℂ) / (↑2 : ℂ) = (↑(π / b) : ℂ) ^ (1 / 2) / 2
Tactic: rw [sqrt_eq_rpow, ← ofReal_div, ofReal_div, ofReal_cpow]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℝ
hb : 0 < b
h : (↑(π / b) : ℂ) ^ (↑(1 / 2) : ℂ) / (↑2 : ℂ) = (↑(π / b) : ℂ) ^ (1 / 2) / 2
⊢ (↑(√(π / b) / 2) : ℂ) = ((↑π : ℂ) / (↑b : ℂ)) ^ (1 / 2) / 2
have h₁ : 0 ≤ π / b
Tactic: rw [sqrt_eq_rpow, ← ofReal_div, ofReal_div, ofReal_cpow]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
⊢ Gamma (1 / 2) = √π
have rw : (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
    (2 * x ^ HSub.hSub (α := ℝ) 2 1) • (rexp (-HPow.hPow (β := ℝ) x 2) * HPow.hPow (β := ℝ) x 2 ^ (1 / 2 - 1))) =
  √π
Tactic: rw [Gamma_eq_integral one_half_pos, ← integral_comp_rpow_Ioi_of_pos zero_lt_two]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      (2 * x ^ HSub.hSub (α := ℝ) 2 1) • (rexp (-HPow.hPow (β := ℝ) x 2) * HPow.hPow (β := ℝ) x 2 ^ (1 / 2 - 1))) =
    √π
have h : (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
    (2 * x ^ HSub.hSub (α := ℝ) 2 1) • (rexp (-HPow.hPow (β := ℝ) x 2) * HPow.hPow (β := ℝ) x 2 ^ (1 / 2 - 1))) =
  HMul.hMul (α := ℝ) 2
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      rexp (-1 * HPow.hPow (β := ℕ) x 2))
Tactic: convert! congr_arg (fun x : ℝ => 2 * x) (integral_gaussian_Ioi 1) using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
h :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      (2 * x ^ HSub.hSub (α := ℝ) 2 1) • (rexp (-HPow.hPow (β := ℝ) x 2) * HPow.hPow (β := ℝ) x 2 ^ (1 / 2 - 1))) =
    HMul.hMul (α := ℝ) 2
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        rexp (-1 * HPow.hPow (β := ℕ) x 2))
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      (2 * x ^ HSub.hSub (α := ℝ) 2 1) • (rexp (-HPow.hPow (β := ℝ) x 2) * HPow.hPow (β := ℝ) x 2 ^ (1 / 2 - 1))) =
    √π
have h₁ : √π = 2 * (√(π / 1) / 2)
Tactic: convert! congr_arg (fun x : ℝ => 2 * x) (integral_gaussian_Ioi 1) using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      (2 * x ^ HSub.hSub (α := ℝ) 2 1) • (rexp (-HPow.hPow (β := ℝ) x 2) * HPow.hPow (β := ℝ) x 2 ^ (1 / 2 - 1))) =
    HMul.hMul (α := ℝ) 2
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        rexp (-1 * HPow.hPow (β := ℕ) x 2))
have h : Eq (α := ℝ)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
    (2 * x ^ HSub.hSub (α := ℝ) 2 1) • (rexp (-HPow.hPow (β := ℝ) x 2) * HPow.hPow (β := ℝ) x 2 ^ (1 / 2 - 1)))
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦
    2 * rexp (-1 * HPow.hPow (β := ℕ) a 2))
Tactic: rw [← integral_const_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      (2 * x ^ HSub.hSub (α := ℝ) 2 1) • (rexp (-HPow.hPow (β := ℝ) x 2) * HPow.hPow (β := ℝ) x 2 ^ (1 / 2 - 1)))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦
      2 * rexp (-1 * HPow.hPow (β := ℕ) a 2))
have h : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioi 0) x),
  (2 * x ^ HSub.hSub (α := ℝ) 2 1) • (rexp (-HPow.hPow (β := ℝ) x 2) * HPow.hPow (β := ℝ) x 2 ^ (1 / 2 - 1)) =
    2 * rexp (-1 * HPow.hPow (β := ℕ) x 2)
Tactic: refine setIntegral_congr_fun measurableSet_Ioi fun x hx => ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ HPow.hPow (β := ℝ) x 2 ^ (1 / 2 - 1) = x⁻¹
have rw : x ^ (2 * (1 / 2 - 1)) = x⁻¹
Tactic: rw [← rpow_mul (le_of_lt hx)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ x ^ (2 * (1 / 2 - 1)) = x⁻¹
have norm_num : HPow.hPow (β := ℝ) x (-1) = x⁻¹
Tactic: norm_num
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ HPow.hPow (β := ℝ) x (-1) = x⁻¹
have rw : (HPow.hPow (β := ℝ) x 1)⁻¹ = x⁻¹
Tactic: rw [rpow_neg (le_of_lt hx), rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
rw : (HPow.hPow (β := ℝ) x 1)⁻¹ = x⁻¹
⊢ HPow.hPow (β := ℝ) x (-1) = x⁻¹
have rw₁ : x⁻¹ = x⁻¹
Tactic: rw [rpow_neg (le_of_lt hx), rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (hypothesis)
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ (2 * x ^ HSub.hSub (α := ℝ) 2 1) • (rexp (-HPow.hPow (β := ℝ) x 2) * HPow.hPow (β := ℝ) x 2 ^ (1 / 2 - 1)) =
    2 * rexp (-1 * HPow.hPow (β := ℕ) x 2)
have this : HPow.hPow (β := ℝ) x 2 ^ (1 / 2 - 1) = x⁻¹
Tactic: have : (x ^ (2 : ℝ)) ^ (1 / (2 : ℝ) - 1) = x⁻¹ := by
      rw [← rpow_mul (le_of_lt hx)]
      norm_num
      rw [rpow_neg (le_of_lt hx), rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
this : HPow.hPow (β := ℝ) x 2 ^ (1 / 2 - 1) = x⁻¹
⊢ (2 * x ^ HSub.hSub (α := ℝ) 2 1) • (rexp (-HPow.hPow (β := ℝ) x 2) * HPow.hPow (β := ℝ) x 2 ^ (1 / 2 - 1)) =
    2 * rexp (-1 * HPow.hPow (β := ℕ) x 2)
have h : 2 * x ^ HSub.hSub (α := ℝ) 2 1 * (rexp (-HPow.hPow (β := ℝ) x 2) * x⁻¹) = 2 * rexp (-1 * HPow.hPow (β := ℕ) x 2)
Tactic: rw [smul_eq_mul, this]