awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
⊢ @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ x ^ s * rexp (-b * HPow.hPow (β := ℕ) x 2)) volume
have rw : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s * rexp (-b * HPow.hPow (β := ℕ) x 2))
    (Iio 0) volume ∧
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (x : ℝ) ↦ x ^ s * rexp (-b * HPow.hPow (β := ℕ) x 2)) (Ioi 0) volume
Tactic: rw [← integrableOn_univ, ← @Iio_union_Ici _ _ (0 : ℝ), integrableOn_union,
    integrableOn_Ici_iff_integrableOn_Ioi]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
      (fun (x : ℝ) ↦ x ^ s * rexp (-b * HPow.hPow (β := ℕ) x 2)) (Iio 0) volume ∧
    IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
      (fun (x : ℝ) ↦ x ^ s * rexp (-b * HPow.hPow (β := ℕ) x 2)) (Ioi 0) volume
have refine : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s * rexp (-b * HPow.hPow (β := ℕ) x 2))
  (Iio 0) volume
Tactic: refine ⟨?_, integrableOn_rpow_mul_exp_neg_mul_sq hb hs⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (x : ℝ) ↦ x ^ s * rexp (-b * HPow.hPow (β := ℕ) x 2)) (Iio 0) volume
have rw : IntegrableOn (α := ℝ) (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
  ((fun (x : ℝ) ↦ x ^ s * rexp (-b * HPow.hPow (β := ℕ) x 2)) ∘ Neg.neg) (Neg.neg ⁻¹' Iio 0) volume
Tactic: rw [← (Measure.measurePreserving_neg (volume : Measure ℝ)).integrableOn_comp_preimage
      (Homeomorph.neg ℝ).measurableEmbedding]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
⊢ IntegrableOn (α := ℝ) (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    ((fun (x : ℝ) ↦ x ^ s * rexp (-b * HPow.hPow (β := ℕ) x 2)) ∘ Neg.neg) (Neg.neg ⁻¹' Iio 0) volume
have simp : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
  (fun (x : ℝ) ↦ (-x) ^ s * rexp (-b * HPow.hPow (β := ℕ) x 2)) (Ioi 0) volume
Tactic: simp only [Function.comp_def, neg_sq, neg_preimage, neg_Iio, neg_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (x : ℝ) ↦ (-x) ^ s * rexp (-b * HPow.hPow (β := ℕ) x 2)) (Ioi 0) volume
have hf : AEStronglyMeasurable (β := ℝ) (m₀ := MeasureSpace.toMeasurableSpace)
  (fun (x : ℝ) ↦ (-x) ^ s * rexp (-b * HPow.hPow (β := ℕ) x 2)) (Measure.restrict volume (Ioi 0))
Tactic: apply Integrable.mono' (integrableOn_rpow_mul_exp_neg_mul_sq hb hs)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
hf :
  AEStronglyMeasurable (β := ℝ) (m₀ := MeasureSpace.toMeasurableSpace)
    (fun (x : ℝ) ↦ (-x) ^ s * rexp (-b * HPow.hPow (β := ℕ) x 2)) (Measure.restrict volume (Ioi 0))
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (x : ℝ) ↦ (-x) ^ s * rexp (-b * HPow.hPow (β := ℕ) x 2)) (Ioi 0) volume
have h : ∀ᵐ (a : ℝ) ∂Measure.restrict volume (Ioi 0),
  ‖(-a) ^ s * rexp (-b * HPow.hPow (β := ℕ) a 2)‖ ≤ a ^ s * rexp (-b * HPow.hPow (β := ℕ) a 2)
Tactic: apply Integrable.mono' (integrableOn_rpow_mul_exp_neg_mul_sq hb hs)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := MeasureSpace.toMeasurableSpace)
    (fun (x : ℝ) ↦ (-x) ^ s * rexp (-b * HPow.hPow (β := ℕ) x 2)) (Measure.restrict volume (Ioi 0))
have hf : Measurable (β := ℝ) fun (x : ℝ) ↦ (-x) ^ s * rexp (-b * HPow.hPow (β := ℕ) x 2)
Tactic: apply Measurable.aestronglyMeasurable
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (hypothesis)
Goal:
b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
⊢ ∀ᵐ (a : ℝ) ∂Measure.restrict volume (Ioi 0),
    ‖(-a) ^ s * rexp (-b * HPow.hPow (β := ℕ) a 2)‖ ≤ a ^ s * rexp (-b * HPow.hPow (β := ℕ) a 2)
have this : MeasurableSet (α := ℝ) (Ioi 0)
Tactic: have : MeasurableSet (Ioi (0 : ℝ)) := measurableSet_Ioi
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
this : MeasurableSet (α := ℝ) (Ioi 0)
⊢ ∀ᵐ (a : ℝ) ∂Measure.restrict volume (Ioi 0),
    ‖(-a) ^ s * rexp (-b * HPow.hPow (β := ℕ) a 2)‖ ≤ a ^ s * rexp (-b * HPow.hPow (β := ℕ) a 2)
have h : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioi 0) x),
  ‖(-x) ^ s * rexp (-b * HPow.hPow (β := ℕ) x 2)‖ ≤ x ^ s * rexp (-b * HPow.hPow (β := ℕ) x 2)
Tactic: filter_upwards [ae_restrict_mem this] with x hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (hypothesis)
Goal:
b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
this : MeasurableSet (α := ℝ) (Ioi 0)
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ ‖(-x) ^ s * rexp (-b * HPow.hPow (β := ℕ) x 2)‖ ≤ x ^ s * rexp (-b * HPow.hPow (β := ℕ) x 2)
have h'x : 0 ≤ x
Tactic: have h'x : 0 ≤ x := le_of_lt hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
this : MeasurableSet (α := ℝ) (Ioi 0)
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
h'x : 0 ≤ x
⊢ ‖(-x) ^ s * rexp (-b * HPow.hPow (β := ℕ) x 2)‖ ≤ x ^ s * rexp (-b * HPow.hPow (β := ℕ) x 2)
have h : |(-x) ^ s| * rexp (-b * HPow.hPow (β := ℕ) x 2) ≤ x ^ s * rexp (-b * HPow.hPow (β := ℕ) x 2)
Tactic: rw [Real.norm_eq_abs, abs_mul, abs_of_nonneg (exp_pos _).le]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
this : MeasurableSet (α := ℝ) (Ioi 0)
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
h'x : 0 ≤ x
⊢ |(-x) ^ s| * rexp (-b * HPow.hPow (β := ℕ) x 2) ≤ x ^ s * rexp (-b * HPow.hPow (β := ℕ) x 2)
have apply : |(-x) ^ s| ≤ x ^ s
Tactic: apply mul_le_mul_of_nonneg_right _ (exp_pos _).le
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℝ
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ rexp (-b * HPow.hPow (β := ℕ) x 2))
      (Ioi 0) volume ↔
    0 < b
have refine : ∀
  (h :
    IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ rexp (-b * HPow.hPow (β := ℕ) x 2))
      (Ioi 0) volume),
  0 < b
Tactic: refine ⟨fun h => ?_, fun h => (integrable_exp_neg_mul_sq h).integrableOn⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℝ
h :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ rexp (-b * HPow.hPow (β := ℕ) x 2))
    (Ioi 0) volume
⊢ 0 < b
have by_contra! : ∀ (hb : b ≤ 0), False
Tactic: by_contra! hb
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℝ
h :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ rexp (-b * HPow.hPow (β := ℕ) x 2))
    (Ioi 0) volume
hb : b ≤ 0
⊢ ∫⁻ (x : ℝ) in Ioi 0, 1 ≤ ∫⁻ (x : ℝ) in Ioi 0, (↑‖rexp (-b * HPow.hPow (β := ℕ) x 2)‖₊ : ENNReal)
have apply : ∀ (x : ℝ), 1 ≤ (↑‖rexp (-b * HPow.hPow (β := ℕ) x 2)‖₊ : ENNReal)
Tactic: apply lintegral_mono (fun x ↦ _)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℝ
h :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ rexp (-b * HPow.hPow (β := ℕ) x 2))
    (Ioi 0) volume
hb : b ≤ 0
⊢ ∀ (x : ℝ), 1 ≤ (↑‖rexp (-b * HPow.hPow (β := ℕ) x 2)‖₊ : ENNReal)
have simp : ∀ (x : ℝ), b * HPow.hPow (β := ℕ) x 2 ≤ 0
Tactic: simp only [neg_mul, ENNReal.one_le_coe_iff, ← toNNReal_one, toNNReal_le_iff_le_coe,
      Real.norm_of_nonneg (exp_pos _).le, coe_nnnorm, one_le_exp_iff, Right.nonneg_neg_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (hypothesis)
Goal:
b : ℝ
h :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ rexp (-b * HPow.hPow (β := ℕ) x 2))
    (Ioi 0) volume
hb : b ≤ 0
⊢ False
have this : ∫⁻ (x : ℝ) in Ioi 0, 1 ≤ ∫⁻ (x : ℝ) in Ioi 0, (↑‖rexp (-b * HPow.hPow (β := ℕ) x 2)‖₊ : ENNReal)
Tactic: have : ∫⁻ _ : ℝ in Ioi 0, 1 ≤ ∫⁻ x : ℝ in Ioi 0, ‖exp (-b * x ^ 2)‖₊ := by
    apply lintegral_mono (fun x ↦ _)
    simp only [neg_mul, ENNReal.one_le_coe_iff, ← toNNReal_one, toNNReal_le_iff_le_coe,
      Real.norm_of_nonneg (exp_pos _).le, coe_nnnorm, one_le_exp_iff, Right.nonneg_neg_iff]
    exact fun x ↦ mul_nonpos_of_nonpos_of_nonneg hb (sq_nonneg x)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℂ
x : ℝ
⊢ ‖cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)‖ = rexp (-b.re * HPow.hPow (β := ℕ) x 2)
have rw : rexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2).re = rexp (-b.re * HPow.hPow (β := ℕ) x 2)
Tactic: rw [norm_exp, ← ofReal_pow, mul_comm (-b) _, re_ofReal_mul, neg_re, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℂ
x : ℝ
rw : rexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2).re = rexp (-b.re * HPow.hPow (β := ℕ) x 2)
⊢ ‖cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)‖ = rexp (-b.re * HPow.hPow (β := ℕ) x 2)
have rw₁ : rexp (-b * (↑(HPow.hPow (β := ℕ) x 2) : ℂ)).re = rexp (-b.re * HPow.hPow (β := ℕ) x 2)
Tactic: rw [norm_exp, ← ofReal_pow, mul_comm (-b) _, re_ofReal_mul, neg_re, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℂ
x : ℝ
rw : rexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2).re = rexp (-b.re * HPow.hPow (β := ℕ) x 2)
rw₁ : rexp (-b * (↑(HPow.hPow (β := ℕ) x 2) : ℂ)).re = rexp (-b.re * HPow.hPow (β := ℕ) x 2)
⊢ ‖cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)‖ = rexp (-b.re * HPow.hPow (β := ℕ) x 2)
have rw₂ : rexp ((↑(HPow.hPow (β := ℕ) x 2) : ℂ) * -b).re = rexp (-b.re * HPow.hPow (β := ℕ) x 2)
Tactic: rw [norm_exp, ← ofReal_pow, mul_comm (-b) _, re_ofReal_mul, neg_re, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℂ
x : ℝ
rw : rexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2).re = rexp (-b.re * HPow.hPow (β := ℕ) x 2)
rw₁ : rexp (-b * (↑(HPow.hPow (β := ℕ) x 2) : ℂ)).re = rexp (-b.re * HPow.hPow (β := ℕ) x 2)
rw₂ : rexp ((↑(HPow.hPow (β := ℕ) x 2) : ℂ) * -b).re = rexp (-b.re * HPow.hPow (β := ℕ) x 2)
⊢ ‖cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)‖ = rexp (-b.re * HPow.hPow (β := ℕ) x 2)
have rw₃ : rexp (HPow.hPow (β := ℕ) x 2 * (-b).re) = rexp (-b.re * HPow.hPow (β := ℕ) x 2)
Tactic: rw [norm_exp, ← ofReal_pow, mul_comm (-b) _, re_ofReal_mul, neg_re, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℂ
x : ℝ
rw : rexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2).re = rexp (-b.re * HPow.hPow (β := ℕ) x 2)
rw₁ : rexp (-b * (↑(HPow.hPow (β := ℕ) x 2) : ℂ)).re = rexp (-b.re * HPow.hPow (β := ℕ) x 2)
rw₂ : rexp ((↑(HPow.hPow (β := ℕ) x 2) : ℂ) * -b).re = rexp (-b.re * HPow.hPow (β := ℕ) x 2)
rw₃ : rexp (HPow.hPow (β := ℕ) x 2 * (-b).re) = rexp (-b.re * HPow.hPow (β := ℕ) x 2)
⊢ ‖cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)‖ = rexp (-b.re * HPow.hPow (β := ℕ) x 2)
have rw₄ : rexp (HPow.hPow (β := ℕ) x 2 * -b.re) = rexp (-b.re * HPow.hPow (β := ℕ) x 2)
Tactic: rw [norm_exp, ← ofReal_pow, mul_comm (-b) _, re_ofReal_mul, neg_re, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℂ
x : ℝ
rw : rexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2).re = rexp (-b.re * HPow.hPow (β := ℕ) x 2)
rw₁ : rexp (-b * (↑(HPow.hPow (β := ℕ) x 2) : ℂ)).re = rexp (-b.re * HPow.hPow (β := ℕ) x 2)
rw₂ : rexp ((↑(HPow.hPow (β := ℕ) x 2) : ℂ) * -b).re = rexp (-b.re * HPow.hPow (β := ℕ) x 2)
rw₃ : rexp (HPow.hPow (β := ℕ) x 2 * (-b).re) = rexp (-b.re * HPow.hPow (β := ℕ) x 2)
rw₄ : rexp (HPow.hPow (β := ℕ) x 2 * -b.re) = rexp (-b.re * HPow.hPow (β := ℕ) x 2)
⊢ ‖cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)‖ = rexp (-b.re * HPow.hPow (β := ℕ) x 2)
have rw₅ : rexp (-b.re * HPow.hPow (β := ℕ) x 2) = rexp (-b.re * HPow.hPow (β := ℕ) x 2)
Tactic: rw [norm_exp, ← ofReal_pow, mul_comm (-b) _, re_ofReal_mul, neg_re, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℂ
hb : 0 < b.re
⊢ @Integrable ℂ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) volume
have refine : @HasFiniteIntegral _ ℂ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) volume
Tactic: refine ⟨by fun_prop, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℂ
hb : 0 < b.re
⊢ @HasFiniteIntegral _ ℂ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
    volume
have rw : @HasFiniteIntegral _ ℝ _ MeasureSpace.toMeasurableSpace (fun (a : ℝ) ↦ ‖cexp (-b * HPow.hPow (β := ℕ) (↑a : ℂ) 2)‖)
  volume
Tactic: rw [← hasFiniteIntegral_norm_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℂ
hb : 0 < b.re
⊢ @HasFiniteIntegral _ ℝ _ MeasureSpace.toMeasurableSpace (fun (a : ℝ) ↦ ‖cexp (-b * HPow.hPow (β := ℕ) (↑a : ℂ) 2)‖)
    volume
have simp_rw : @HasFiniteIntegral _ ℝ _ MeasureSpace.toMeasurableSpace (fun (a : ℝ) ↦ rexp (-b.re * HPow.hPow (β := ℕ) a 2)) volume
Tactic: simp_rw [norm_cexp_neg_mul_sq]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℂ
hb : 0 < b.re
⊢ @Integrable ℂ _ _ _ MeasureSpace.toMeasurableSpace
    (fun (x : ℝ) ↦ (↑x : ℂ) * cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) volume
have refine_1 : Continuous (Y := ℂ) fun (x : ℝ) ↦ -b * HPow.hPow (β := ℕ) (↑x : ℂ) 2
Tactic: refine ⟨(continuous_ofReal.mul (Complex.continuous_exp.comp ?_)).aestronglyMeasurable, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℂ
hb : 0 < b.re
refine_1 : Continuous (Y := ℂ) fun (x : ℝ) ↦ -b * HPow.hPow (β := ℕ) (↑x : ℂ) 2
⊢ @Integrable ℂ _ _ _ MeasureSpace.toMeasurableSpace
    (fun (x : ℝ) ↦ (↑x : ℂ) * cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) volume
have refine_2 : @HasFiniteIntegral _ ℂ _ MeasureSpace.toMeasurableSpace
  (fun (x : ℝ) ↦ (↑x : ℂ) * cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) volume
Tactic: refine ⟨(continuous_ofReal.mul (Complex.continuous_exp.comp ?_)).aestronglyMeasurable, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (hypothesis)
Goal:
b : ℂ
hb : 0 < b.re
⊢ @HasFiniteIntegral _ ℂ _ MeasureSpace.toMeasurableSpace
    (fun (x : ℝ) ↦ (↑x : ℂ) * cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) volume
have this : @HasFiniteIntegral _ ℝ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ x * rexp (-b.re * HPow.hPow (β := ℕ) x 2)) volume
Tactic: have := (integrable_mul_exp_neg_mul_sq hb).hasFiniteIntegral
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℂ
hb : 0 < b.re
this :
  @HasFiniteIntegral _ ℝ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ x * rexp (-b.re * HPow.hPow (β := ℕ) x 2))
    volume
⊢ @HasFiniteIntegral _ ℂ _ MeasureSpace.toMeasurableSpace
    (fun (x : ℝ) ↦ (↑x : ℂ) * cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) volume
have refine_2 : ∀
  (this :
    @HasFiniteIntegral _ ℝ _ MeasureSpace.toMeasurableSpace (fun (a : ℝ) ↦ ‖a * rexp (-b.re * HPow.hPow (β := ℕ) a 2)‖)
      volume),
  @HasFiniteIntegral _ ℝ _ MeasureSpace.toMeasurableSpace
    (fun (a : ℝ) ↦ ‖(↑a : ℂ) * cexp (-b * HPow.hPow (β := ℕ) (↑a : ℂ) 2)‖) volume
Tactic: rw [← hasFiniteIntegral_norm_iff] at this ⊢
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℂ
hb : 0 < b.re
this :
  @HasFiniteIntegral _ ℝ _ MeasureSpace.toMeasurableSpace (fun (a : ℝ) ↦ ‖a * rexp (-b.re * HPow.hPow (β := ℕ) a 2)‖)
    volume
⊢ @HasFiniteIntegral _ ℝ _ MeasureSpace.toMeasurableSpace
    (fun (a : ℝ) ↦ ‖(↑a : ℂ) * cexp (-b * HPow.hPow (β := ℕ) (↑a : ℂ) 2)‖) volume
have h : ∀ (x : ℝ), ‖(↑x : ℂ) * cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)‖ = ‖x * rexp (-b.re * HPow.hPow (β := ℕ) x 2)‖
Tactic: convert! this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℂ
hb : 0 < b.re
this :
  @HasFiniteIntegral _ ℝ _ MeasureSpace.toMeasurableSpace (fun (a : ℝ) ↦ ‖a * rexp (-b.re * HPow.hPow (β := ℕ) a 2)‖)
    volume
x : ℝ
⊢ ‖(↑x : ℂ) * cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)‖ = ‖x * rexp (-b.re * HPow.hPow (β := ℕ) x 2)‖
have h : ‖(↑x : ℂ)‖ * ‖cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)‖ = ‖x * rexp (-b.re * HPow.hPow (β := ℕ) x 2)‖
Tactic: rw [norm_mul, norm_mul, norm_cexp_neg_mul_sq b, norm_real, norm_of_nonneg (exp_pos _).le]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℂ
hb : 0 < b.re
this :
  @HasFiniteIntegral _ ℝ _ MeasureSpace.toMeasurableSpace (fun (a : ℝ) ↦ ‖a * rexp (-b.re * HPow.hPow (β := ℕ) a 2)‖)
    volume
x : ℝ
h : ‖(↑x : ℂ)‖ * ‖cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)‖ = ‖x * rexp (-b.re * HPow.hPow (β := ℕ) x 2)‖
⊢ ‖(↑x : ℂ) * cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)‖ = ‖x * rexp (-b.re * HPow.hPow (β := ℕ) x 2)‖
have h₁ : ‖(↑x : ℂ)‖ * ‖cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)‖ = ‖x‖ * ‖rexp (-b.re * HPow.hPow (β := ℕ) x 2)‖
Tactic: rw [norm_mul, norm_mul, norm_cexp_neg_mul_sq b, norm_real, norm_of_nonneg (exp_pos _).le]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℂ
hb : 0 < b.re
this :
  @HasFiniteIntegral _ ℝ _ MeasureSpace.toMeasurableSpace (fun (a : ℝ) ↦ ‖a * rexp (-b.re * HPow.hPow (β := ℕ) a 2)‖)
    volume
x : ℝ
h : ‖(↑x : ℂ)‖ * ‖cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)‖ = ‖x * rexp (-b.re * HPow.hPow (β := ℕ) x 2)‖
h₁ : ‖(↑x : ℂ)‖ * ‖cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)‖ = ‖x‖ * ‖rexp (-b.re * HPow.hPow (β := ℕ) x 2)‖
⊢ ‖(↑x : ℂ) * cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)‖ = ‖x * rexp (-b.re * HPow.hPow (β := ℕ) x 2)‖
have h₂ : ‖(↑x : ℂ)‖ * rexp (-b.re * HPow.hPow (β := ℕ) x 2) = ‖x‖ * ‖rexp (-b.re * HPow.hPow (β := ℕ) x 2)‖
Tactic: rw [norm_mul, norm_mul, norm_cexp_neg_mul_sq b, norm_real, norm_of_nonneg (exp_pos _).le]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℂ
hb : 0 < b.re
this :
  @HasFiniteIntegral _ ℝ _ MeasureSpace.toMeasurableSpace (fun (a : ℝ) ↦ ‖a * rexp (-b.re * HPow.hPow (β := ℕ) a 2)‖)
    volume
x : ℝ
h : ‖(↑x : ℂ)‖ * ‖cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)‖ = ‖x * rexp (-b.re * HPow.hPow (β := ℕ) x 2)‖
h₁ : ‖(↑x : ℂ)‖ * ‖cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)‖ = ‖x‖ * ‖rexp (-b.re * HPow.hPow (β := ℕ) x 2)‖
h₂ : ‖(↑x : ℂ)‖ * rexp (-b.re * HPow.hPow (β := ℕ) x 2) = ‖x‖ * ‖rexp (-b.re * HPow.hPow (β := ℕ) x 2)‖
⊢ ‖(↑x : ℂ) * cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)‖ = ‖x * rexp (-b.re * HPow.hPow (β := ℕ) x 2)‖
have h₃ : ‖x‖ * rexp (-b.re * HPow.hPow (β := ℕ) x 2) = ‖x‖ * ‖rexp (-b.re * HPow.hPow (β := ℕ) x 2)‖
Tactic: rw [norm_mul, norm_mul, norm_cexp_neg_mul_sq b, norm_real, norm_of_nonneg (exp_pos _).le]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℂ
hb : 0 < b.re
this :
  @HasFiniteIntegral _ ℝ _ MeasureSpace.toMeasurableSpace (fun (a : ℝ) ↦ ‖a * rexp (-b.re * HPow.hPow (β := ℕ) a 2)‖)
    volume
x : ℝ
h : ‖(↑x : ℂ)‖ * ‖cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)‖ = ‖x * rexp (-b.re * HPow.hPow (β := ℕ) x 2)‖
h₁ : ‖(↑x : ℂ)‖ * ‖cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)‖ = ‖x‖ * ‖rexp (-b.re * HPow.hPow (β := ℕ) x 2)‖
h₂ : ‖(↑x : ℂ)‖ * rexp (-b.re * HPow.hPow (β := ℕ) x 2) = ‖x‖ * ‖rexp (-b.re * HPow.hPow (β := ℕ) x 2)‖
h₃ : ‖x‖ * rexp (-b.re * HPow.hPow (β := ℕ) x 2) = ‖x‖ * ‖rexp (-b.re * HPow.hPow (β := ℕ) x 2)‖
⊢ ‖(↑x : ℂ) * cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)‖ = ‖x * rexp (-b.re * HPow.hPow (β := ℕ) x 2)‖
have h₄ : ‖x‖ * rexp (-b.re * HPow.hPow (β := ℕ) x 2) = ‖x‖ * rexp (-b.re * HPow.hPow (β := ℕ) x 2)
Tactic: rw [norm_mul, norm_mul, norm_cexp_neg_mul_sq b, norm_real, norm_of_nonneg (exp_pos _).le]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℂ
hb : 0 < b.re
⊢ b ≠ 0
have contrapose! : ∀ (hb : b = 0), b.re ≤ 0
Tactic: contrapose! hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℂ
hb : b = 0
⊢ b.re ≤ 0
have rw : re 0 ≤ 0
Tactic: rw [hb, zero_re]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℂ
hb : b = 0
rw : re 0 ≤ 0
⊢ b.re ≤ 0
have rw₁ : LE.le (α := ℝ) 0 0
Tactic: rw [hb, zero_re]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (hypothesis)
Goal:
b : ℂ
hb : 0 < b.re
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (r : ℝ) ↦
      (↑r : ℂ) * cexp (-b * HPow.hPow (β := ℕ) (↑r : ℂ) 2)) =
    (2 * b)⁻¹
have hb' : b ≠ 0
Tactic: have hb' : b ≠ 0 := by contrapose! hb; rw [hb, zero_re]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℂ
hb : 0 < b.re
hb' : b ≠ 0
x : ℂ
⊢ HasDerivAt (fun (x : ℂ) ↦ -(2 * b)⁻¹ * cexp (-b * HPow.hPow (β := ℕ) x 2)) (x * cexp (-b * HPow.hPow (β := ℕ) x 2)) x
have h : x * cexp (-b * HPow.hPow (β := ℕ) x 2) =
  -(2 * b)⁻¹ * (cexp (-b * HPow.hPow (β := ℕ) x 2) * (-b * ((↑2 : ℂ) * x ^ HSub.hSub (α := ℕ) 2 1)))
Tactic: convert! ((hasDerivAt_pow 2 x).const_mul (-b)).cexp.const_mul (-(2 * b)⁻¹) using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (hypothesis)
Goal:
b : ℂ
hb : 0 < b.re
hb' : b ≠ 0
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (r : ℝ) ↦
      (↑r : ℂ) * cexp (-b * HPow.hPow (β := ℕ) (↑r : ℂ) 2)) =
    (2 * b)⁻¹
have A : ∀ (x : ℂ),
  HasDerivAt (fun (x : ℂ) ↦ -(2 * b)⁻¹ * cexp (-b * HPow.hPow (β := ℕ) x 2)) (x * cexp (-b * HPow.hPow (β := ℕ) x 2)) x
Tactic: have A : ∀ x : ℂ, HasDerivAt (fun x => -(2 * b)⁻¹ * cexp (-b * x ^ 2))
    (x * cexp (-b * x ^ 2)) x := by
    intro x
    convert! ((hasDerivAt_pow 2 x).const_mul (-b)).cexp.const_mul (-(2 * b)⁻¹) using 1
    field
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℂ
hb : 0 < b.re
hb' : b ≠ 0
A :
  ∀ (x : ℂ),
    HasDerivAt (fun (x : ℂ) ↦ -(2 * b)⁻¹ * cexp (-b * HPow.hPow (β := ℕ) x 2)) (x * cexp (-b * HPow.hPow (β := ℕ) x 2))
      x
⊢ Tendsto (fun (y : ℝ) ↦ -(2 * b)⁻¹ * cexp (-b * HPow.hPow (β := ℕ) (↑y : ℂ) 2)) atTop (𝓝 (-(2 * b)⁻¹ * 0))
have refine : Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)‖) atTop (𝓝 0)
Tactic: refine Tendsto.const_mul _ (tendsto_zero_iff_norm_tendsto_zero.mpr ?_)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℂ
hb : 0 < b.re
hb' : b ≠ 0
A :
  ∀ (x : ℂ),
    HasDerivAt (fun (x : ℂ) ↦ -(2 * b)⁻¹ * cexp (-b * HPow.hPow (β := ℕ) x 2)) (x * cexp (-b * HPow.hPow (β := ℕ) x 2))
      x
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)‖) atTop (𝓝 0)
have simp_rw : Tendsto (β := ℝ) (fun (x : ℝ) ↦ rexp (-b.re * HPow.hPow (β := ℕ) x 2)) atTop (𝓝 0)
Tactic: simp_rw [norm_cexp_neg_mul_sq b]