awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℝ
hb : 0 < b
⊢ HPow.hPow (α := ℝ) (β := ℕ)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ rexp (-b * HPow.hPow (β := ℕ) x 2)) 2 =
    HPow.hPow (β := ℕ) (√(π / b)) 2
have inr : HPow.hPow (α := ℂ) (β := ℕ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ (↑(rexp (-b * HPow.hPow (β := ℕ) x 2)) : ℂ))
    2 =
  (↑π : ℂ) / (↑b : ℂ)
Tactic: rw [← ofReal_inj, ofReal_pow, ← coe_algebraMap, RCLike.algebraMap_eq_ofReal, ← integral_ofReal,
    sq_sqrt (div_pos pi_pos hb).le, ← RCLike.algebraMap_eq_ofReal, coe_algebraMap, ofReal_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℝ
hb : 0 < b
⊢ HPow.hPow (α := ℂ) (β := ℕ)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦
        (↑(rexp (-b * HPow.hPow (β := ℕ) x 2)) : ℂ))
      2 =
    (↑π : ℂ) / (↑b : ℂ)
have h : ∀ (x : ℝ), (↑(rexp (-b * HPow.hPow (β := ℕ) x 2)) : ℂ) = cexp (-(↑b : ℂ) * HPow.hPow (β := ℕ) (↑x : ℂ) 2)
Tactic: convert! integral_gaussian_sq_complex (by rwa [ofReal_re] : 0 < (b : ℂ).re) with _ x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℝ
hb : 0 < b
x : ℝ
⊢ (↑(rexp (-b * HPow.hPow (β := ℕ) x 2)) : ℂ) = cexp (-(↑b : ℂ) * HPow.hPow (β := ℕ) (↑x : ℂ) 2)
have h : cexp (↑(-b * HPow.hPow (β := ℕ) x 2) : ℂ) = cexp (-(↑b : ℂ) * HPow.hPow (β := ℕ) (↑x : ℂ) 2)
Tactic: rw [ofReal_exp, ofReal_mul, ofReal_pow, ofReal_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℝ
hb : 0 < b
x : ℝ
h : cexp (↑(-b * HPow.hPow (β := ℕ) x 2) : ℂ) = cexp (-(↑b : ℂ) * HPow.hPow (β := ℕ) (↑x : ℂ) 2)
⊢ (↑(rexp (-b * HPow.hPow (β := ℕ) x 2)) : ℂ) = cexp (-(↑b : ℂ) * HPow.hPow (β := ℕ) (↑x : ℂ) 2)
have h₁ : cexp ((↑(-b) : ℂ) * (↑(HPow.hPow (β := ℕ) x 2) : ℂ)) = cexp (-(↑b : ℂ) * HPow.hPow (β := ℕ) (↑x : ℂ) 2)
Tactic: rw [ofReal_exp, ofReal_mul, ofReal_pow, ofReal_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℝ
hb : 0 < b
x : ℝ
h : cexp (↑(-b * HPow.hPow (β := ℕ) x 2) : ℂ) = cexp (-(↑b : ℂ) * HPow.hPow (β := ℕ) (↑x : ℂ) 2)
h₁ : cexp ((↑(-b) : ℂ) * (↑(HPow.hPow (β := ℕ) x 2) : ℂ)) = cexp (-(↑b : ℂ) * HPow.hPow (β := ℕ) (↑x : ℂ) 2)
⊢ (↑(rexp (-b * HPow.hPow (β := ℕ) x 2)) : ℂ) = cexp (-(↑b : ℂ) * HPow.hPow (β := ℕ) (↑x : ℂ) 2)
have h₂ : cexp ((↑(-b) : ℂ) * HPow.hPow (β := ℕ) (↑x : ℂ) 2) = cexp (-(↑b : ℂ) * HPow.hPow (β := ℕ) (↑x : ℂ) 2)
Tactic: rw [ofReal_exp, ofReal_mul, ofReal_pow, ofReal_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℝ
hb : 0 < b
x : ℝ
h : cexp (↑(-b * HPow.hPow (β := ℕ) x 2) : ℂ) = cexp (-(↑b : ℂ) * HPow.hPow (β := ℕ) (↑x : ℂ) 2)
h₁ : cexp ((↑(-b) : ℂ) * (↑(HPow.hPow (β := ℕ) x 2) : ℂ)) = cexp (-(↑b : ℂ) * HPow.hPow (β := ℕ) (↑x : ℂ) 2)
h₂ : cexp ((↑(-b) : ℂ) * HPow.hPow (β := ℕ) (↑x : ℂ) 2) = cexp (-(↑b : ℂ) * HPow.hPow (β := ℕ) (↑x : ℂ) 2)
⊢ (↑(rexp (-b * HPow.hPow (β := ℕ) x 2)) : ℂ) = cexp (-(↑b : ℂ) * HPow.hPow (β := ℕ) (↑x : ℂ) 2)
have h₃ : cexp (-(↑b : ℂ) * HPow.hPow (β := ℕ) (↑x : ℂ) 2) = cexp (-(↑b : ℂ) * HPow.hPow (β := ℕ) (↑x : ℂ) 2)
Tactic: rw [ofReal_exp, ofReal_mul, ofReal_pow, ofReal_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℂ
hb : 0 < b.re
f : ℂ → ℝ → ℂ := fun (c : ℂ) (x : ℝ) ↦ cexp (-c * HPow.hPow (β := ℕ) (↑x : ℂ) 2)
⊢ ContinuousAt (Y := ℂ)
    (fun (c : ℂ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ cexp (-c * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
    b
have obtain : ∀ (d : ℝ) (hd : 0 < d) (hd' : d < b.re),
  ContinuousAt (Y := ℂ)
    (fun (c : ℂ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ cexp (-c * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
    b
Tactic: obtain ⟨d, hd, hd'⟩ := exists_between hb
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℂ
hb : 0 < b.re
f : ℂ → ℝ → ℂ := fun (c : ℂ) (x : ℝ) ↦ cexp (-c * HPow.hPow (β := ℕ) (↑x : ℂ) 2)
d : ℝ
hd : 0 < d
hd' : d < b.re
⊢ ∀ᶠ (c : ℂ) in 𝓝 b, ∀ᵐ (x : ℝ), ‖f c x‖ ≤ rexp (-d * HPow.hPow (β := ℕ) x 2)
have refine : ∀ x ∈ re ⁻¹' Ioi d, ∀ᵐ (x_1 : ℝ), ‖f x x_1‖ ≤ rexp (-d * HPow.hPow (β := ℕ) x_1 2)
Tactic: refine eventually_of_mem ((continuous_re.isOpen_preimage _ isOpen_Ioi).mem_nhds hd') ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℂ
hb : 0 < b.re
f : ℂ → ℝ → ℂ := fun (c : ℂ) (x : ℝ) ↦ cexp (-c * HPow.hPow (β := ℕ) (↑x : ℂ) 2)
d : ℝ
hd : 0 < d
hd' : d < b.re
c : ℂ
hc : c ∈ re ⁻¹' Ioi d
⊢ ∀ᵐ (x : ℝ), ‖f c x‖ ≤ rexp (-d * HPow.hPow (β := ℕ) x 2)
have h : ∀ (x : ℝ), ‖f c x‖ ≤ rexp (-d * HPow.hPow (β := ℕ) x 2)
Tactic: filter_upwards with x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℂ
hb : 0 < b.re
f : ℂ → ℝ → ℂ := fun (c : ℂ) (x : ℝ) ↦ cexp (-c * HPow.hPow (β := ℕ) (↑x : ℂ) 2)
d : ℝ
hd : 0 < d
hd' : d < b.re
c : ℂ
hc : c ∈ re ⁻¹' Ioi d
x : ℝ
⊢ ‖f c x‖ ≤ rexp (-d * HPow.hPow (β := ℕ) x 2)
have h : rexp (-c.re * HPow.hPow (β := ℕ) x 2) ≤ rexp (-d * HPow.hPow (β := ℕ) x 2)
Tactic: rw [norm_cexp_neg_mul_sq]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℂ
hb : 0 < b.re
f : ℂ → ℝ → ℂ := fun (c : ℂ) (x : ℝ) ↦ cexp (-c * HPow.hPow (β := ℕ) (↑x : ℂ) 2)
d : ℝ
hd : 0 < d
hd' : d < b.re
c : ℂ
hc : c ∈ re ⁻¹' Ioi d
x : ℝ
⊢ rexp (-c.re * HPow.hPow (β := ℕ) x 2) ≤ rexp (-d * HPow.hPow (β := ℕ) x 2)
have h : d ≤ c.re
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (hypothesis)
Goal:
b : ℂ
hb : 0 < b.re
f : ℂ → ℝ → ℂ := fun (c : ℂ) (x : ℝ) ↦ cexp (-c * HPow.hPow (β := ℕ) (↑x : ℂ) 2)
d : ℝ
hd : 0 < d
hd' : d < b.re
⊢ ContinuousAt (Y := ℂ)
    (fun (c : ℂ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ cexp (-c * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
    b
have f_le_bd : ∀ᶠ (c : ℂ) in 𝓝 b, ∀ᵐ (x : ℝ), ‖f c x‖ ≤ rexp (-d * HPow.hPow (β := ℕ) x 2)
Tactic: have f_le_bd : ∀ᶠ c : ℂ in 𝓝 b, ∀ᵐ x : ℝ, ‖f c x‖ ≤ exp (-d * x ^ 2) := by
    refine eventually_of_mem ((continuous_re.isOpen_preimage _ isOpen_Ioi).mem_nhds hd') ?_
    intro c hc; filter_upwards with x
    rw [norm_cexp_neg_mul_sq]
    gcongr
    exact le_of_lt hc
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b_1 : ℂ
hb_1 : 0 < b_1.re
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_1 : ℂ
hb_1 : 0 < b_1.re
b : ℂ
hb : b = 0
⊢ b.re ≤ 0
have rw : re 0 ≤ 0
Tactic: rw [hb]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (hypothesis)
Goal:
b : ℂ
hb : 0 < b.re
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) =
    ((↑π : ℂ) / b) ^ (1 / 2)
have nv : ∀ {b : ℂ}, 0 < b.re → b ≠ 0
Tactic: have nv : ∀ {b : ℂ}, 0 < re b → b ≠ 0 := by intro b hb; contrapose! hb; rw [hb]; simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℂ
hb : 0 < b.re
nv : ∀ {b : ℂ}, 0 < b.re → b ≠ 0
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) =
    ((↑π : ℂ) / b) ^ (1 / 2)
have c : ContinuousOn (Y := ℂ)
  (fun {b : ℂ} ↦
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
  {c : ℂ | 0 < c.re}
Tactic: apply
    (convex_halfSpace_re_gt 0).isPreconnected.eq_of_sq_eq ?_ ?_ (fun c hc => ?_) (fun {c} hc => ?_)
      (by simp : 0 < re (1 : ℂ)) ?_ hb
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℂ
hb : 0 < b.re
nv : ∀ {b : ℂ}, 0 < b.re → b ≠ 0
c :
  ContinuousOn (Y := ℂ)
    (fun {b : ℂ} ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
    {c : ℂ | 0 < c.re}
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) =
    ((↑π : ℂ) / b) ^ (1 / 2)
have c₁ : ContinuousOn (Y := ℂ) (fun {b : ℂ} ↦ ((↑π : ℂ) / b) ^ (1 / 2)) {c : ℂ | 0 < c.re}
Tactic: apply
    (convex_halfSpace_re_gt 0).isPreconnected.eq_of_sq_eq ?_ ?_ (fun c hc => ?_) (fun {c} hc => ?_)
      (by simp : 0 < re (1 : ℂ)) ?_ hb
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℂ
hb : 0 < b.re
nv : ∀ {b : ℂ}, 0 < b.re → b ≠ 0
c :
  ContinuousOn (Y := ℂ)
    (fun {b : ℂ} ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
    {c : ℂ | 0 < c.re}
c₁ : ContinuousOn (Y := ℂ) (fun {b : ℂ} ↦ ((↑π : ℂ) / b) ^ (1 / 2)) {c : ℂ | 0 < c.re}
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) =
    ((↑π : ℂ) / b) ^ (1 / 2)
have c₂ : (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ cexp (-1 * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) =
  ((↑π : ℂ) / 1) ^ (1 / 2)
Tactic: apply
    (convex_halfSpace_re_gt 0).isPreconnected.eq_of_sq_eq ?_ ?_ (fun c hc => ?_) (fun {c} hc => ?_)
      (by simp : 0 < re (1 : ℂ)) ?_ hb
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℂ
hb : 0 < b.re
nv : ∀ {b : ℂ}, 0 < b.re → b ≠ 0
c :
  ContinuousOn (Y := ℂ)
    (fun {b : ℂ} ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
    {c : ℂ | 0 < c.re}
c₁ : ContinuousOn (Y := ℂ) (fun {b : ℂ} ↦ ((↑π : ℂ) / b) ^ (1 / 2)) {c : ℂ | 0 < c.re}
c₂ :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ cexp (-1 * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) =
    ((↑π : ℂ) / 1) ^ (1 / 2)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) =
    ((↑π : ℂ) / b) ^ (1 / 2)
have c₃ : ∀ (c : ℂ) (hc : Membership.mem (γ := Set ℂ) {c : ℂ | 0 < c.re} c),
  HPow.hPow (α := ℂ → ℂ) (β := ℕ)
      (fun {b : ℂ} ↦
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
      2 c =
    HPow.hPow (α := ℂ → ℂ) (β := ℕ) (fun {b : ℂ} ↦ ((↑π : ℂ) / b) ^ (1 / 2)) 2 c
Tactic: apply
    (convex_halfSpace_re_gt 0).isPreconnected.eq_of_sq_eq ?_ ?_ (fun c hc => ?_) (fun {c} hc => ?_)
      (by simp : 0 < re (1 : ℂ)) ?_ hb
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℂ
hb : 0 < b.re
nv : ∀ {b : ℂ}, 0 < b.re → b ≠ 0
c :
  ContinuousOn (Y := ℂ)
    (fun {b : ℂ} ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
    {c : ℂ | 0 < c.re}
c₁ : ContinuousOn (Y := ℂ) (fun {b : ℂ} ↦ ((↑π : ℂ) / b) ^ (1 / 2)) {c : ℂ | 0 < c.re}
c₂ :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ cexp (-1 * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) =
    ((↑π : ℂ) / 1) ^ (1 / 2)
c₃ :
  ∀ (c : ℂ) (hc : Membership.mem (γ := Set ℂ) {c : ℂ | 0 < c.re} c),
    HPow.hPow (α := ℂ → ℂ) (β := ℕ)
        (fun {b : ℂ} ↦
          @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦
            cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
        2 c =
      HPow.hPow (α := ℂ → ℂ) (β := ℕ) (fun {b : ℂ} ↦ ((↑π : ℂ) / b) ^ (1 / 2)) 2 c
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) =
    ((↑π : ℂ) / b) ^ (1 / 2)
have c₄ : ∀ {c : ℂ} (hc : Membership.mem (γ := Set ℂ) {c : ℂ | 0 < c.re} c), ((↑π : ℂ) / c) ^ (1 / 2) ≠ 0
Tactic: apply
    (convex_halfSpace_re_gt 0).isPreconnected.eq_of_sq_eq ?_ ?_ (fun c hc => ?_) (fun {c} hc => ?_)
      (by simp : 0 < re (1 : ℂ)) ?_ hb
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℂ
hb : 0 < b.re
nv : ∀ {b : ℂ}, 0 < b.re → b ≠ 0
⊢ ContinuousOn (Y := ℂ) (fun {b : ℂ} ↦ ((↑π : ℂ) / b) ^ (1 / 2)) {c : ℂ | 0 < c.re}
have continuousOn_of_forall_continuousAt : ∀ (b : ℂ) (hb : Membership.mem (γ := Set ℂ) {c : ℂ | 0 < c.re} b), 0 < ((↑π : ℂ) / b).re
Tactic: refine
      continuousOn_of_forall_continuousAt fun b hb =>
        (continuousAt_cpow_const (Or.inl ?_)).comp (continuousAt_const.div continuousAt_id (nv hb))
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b_1 : ℂ
hb_1 : 0 < b_1.re
nv : ∀ {b : ℂ}, 0 < b.re → b ≠ 0
b : ℂ
hb : Membership.mem (γ := Set ℂ) {c : ℂ | 0 < c.re} b
⊢ 0 < ((↑π : ℂ) / b).re
have rw : 0 < HDiv.hDiv (β := ℝ) (π * b.re) ((normSq : (a : ℂ) → ℝ) b : ℝ)
Tactic: rw [div_re, ofReal_im, ofReal_re, zero_mul, zero_div, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (hypothesis)
Goal:
b : ℂ
hb : 0 < b.re
nv : ∀ {b : ℂ}, 0 < b.re → b ≠ 0
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ cexp (-1 * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) =
    ((↑π : ℂ) / 1) ^ (1 / 2)
have this : ∀ (x : ℝ), cexp (-1 * HPow.hPow (β := ℕ) (↑x : ℂ) 2) = (↑(rexp (-1 * HPow.hPow (β := ℕ) x 2)) : ℂ)
Tactic: have : ∀ x : ℝ, cexp (-(1 : ℂ) * (x : ℂ) ^ 2) = exp (-(1 : ℝ) * x ^ 2) := by
      intro x
      simp only [ofReal_exp, neg_mul, one_mul, ofReal_neg, ofReal_pow]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
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 : ℝ) ↦ cexp (-1 * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) =
    ((↑π : ℂ) / 1) ^ (1 / 2)
have simp_rw : (↑(@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ rexp (-1 * HPow.hPow (β := ℕ) x 2)) : ℂ) =
  ((↑π : ℂ) / 1) ^ (1 / 2)
Tactic: simp_rw [this, ← coe_algebraMap, RCLike.algebraMap_eq_ofReal, integral_ofReal,
      ← RCLike.algebraMap_eq_ofReal, coe_algebraMap]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
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)) : ℂ)
| ((↑π : ℂ) / 1) ^ (1 / 2)
have a : (↑π : ℂ) / 1
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
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)) : ℂ)
a : (↑π : ℂ) / 1
| ((↑π : ℂ) / 1) ^ (1 / 2)
have a₁ : 1 / 2
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
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)) : ℂ)
| (↑π : ℂ) / 1
have a : (↑(π / 1) : ℂ)
Tactic: rw [← ofReal_one, ← ofReal_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
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)) : ℂ)
| 1 / 2
have a : (↑(HDiv.hDiv (α := ℝ) 1 2) : ℂ)
Tactic: rw [← ofReal_one, ← ofReal_ofNat, ← ofReal_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
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)) : ℂ)
| 1 / 2
have a : (↑1 : ℂ) / 2
Tactic: · rw [← ofReal_one, ← ofReal_ofNat, ← ofReal_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
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)) : ℂ)
a : (↑1 : ℂ) / 2
| 1 / 2
have a₁ : (↑1 : ℂ) / (↑2 : ℂ)
Tactic: · rw [← ofReal_one, ← ofReal_ofNat, ← ofReal_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
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)) : ℂ)
a : (↑1 : ℂ) / 2
a₁ : (↑1 : ℂ) / (↑2 : ℂ)
| 1 / 2
have a₂ : (↑(HDiv.hDiv (α := ℝ) 1 2) : ℂ)
Tactic: · rw [← ofReal_one, ← ofReal_ofNat, ← ofReal_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
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)) : ℂ)
| ((↑π : ℂ) / 1) ^ (1 / 2)
have a : (↑π : ℂ) / 1
Tactic: congr
      · rw [← ofReal_one, ← ofReal_div]
      · rw [← ofReal_one, ← ofReal_ofNat, ← ofReal_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
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)) : ℂ)
a : (↑π : ℂ) / 1
| ((↑π : ℂ) / 1) ^ (1 / 2)
have a₁ : 1 / 2
Tactic: congr
      · rw [← ofReal_one, ← ofReal_div]
      · rw [← ofReal_one, ← ofReal_ofNat, ← ofReal_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
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) ^ (1 / 2)
have conv_rhs : (↑(@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ rexp (-1 * HPow.hPow (β := ℕ) x 2)) : ℂ) =
  (↑(π / 1) : ℂ) ^ (↑(HDiv.hDiv (α := ℝ) 1 2) : ℂ)
Tactic: conv_rhs =>
      congr
      · rw [← ofReal_one, ← ofReal_div]
      · rw [← ofReal_one, ← ofReal_ofNat, ← ofReal_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
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) : ℂ) ^ (↑(HDiv.hDiv (α := ℝ) 1 2) : ℂ)
have rw : (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ rexp (-1 * HPow.hPow (β := ℕ) x 2)) =
  (π / 1) ^ HDiv.hDiv (α := ℝ) 1 2
Tactic: rw [← ofReal_cpow, ofReal_inj]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
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
⊢ (↑(@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ rexp (-1 * HPow.hPow (β := ℕ) x 2)) : ℂ) =
    (↑(π / 1) : ℂ) ^ (↑(HDiv.hDiv (α := ℝ) 1 2) : ℂ)
have hx : 0 ≤ π / 1
Tactic: rw [← ofReal_cpow, ofReal_inj]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
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) ^ HDiv.hDiv (α := ℝ) 1 2
have h : (π / 1) ^ HDiv.hDiv (α := ℝ) 1 2 = √(π / 1)
Tactic: convert! integral_gaussian (1 : ℝ) using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
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)) : ℂ)
⊢ (π / 1) ^ HDiv.hDiv (α := ℝ) 1 2 = √(π / 1)
have h : (π / 1) ^ HDiv.hDiv (α := ℝ) 1 2 = (π / 1) ^ (1 / 2)
Tactic: rw [sqrt_eq_rpow]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
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 ≤ π / 1
have hx : 0 ≤ π
Tactic: rw [div_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
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 (α := ℂ) (β := ℕ)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ cexp (-c * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
      2 =
    HPow.hPow (β := ℕ) (((↑π : ℂ) / c) ^ (1 / 2)) 2
have rw : (↑π : ℂ) / c = ((↑π : ℂ) / c) ^ (1 / 2) * ((↑π : ℂ) / c) ^ (1 / 2)
Tactic: rw [integral_gaussian_sq_complex hc, sq]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℂ
hb : 0 < b.re
nv : ∀ {b : ℂ}, 0 < b.re → b ≠ 0
c : ℂ
hc : Membership.mem (γ := Set ℂ) {c : ℂ | 0 < c.re} c
| (↑π : ℂ) / c
have rw : HPow.hPow (β := ℂ) ((↑π : ℂ) / c) 1
Tactic: rw [← cpow_one (↑π / c)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℂ
hb : 0 < b.re
nv : ∀ {b : ℂ}, 0 < b.re → b ≠ 0
c : ℂ
hc : Membership.mem (γ := Set ℂ) {c : ℂ | 0 < c.re} c
⊢ (↑π : ℂ) / c = ((↑π : ℂ) / c) ^ (1 / 2) * ((↑π : ℂ) / c) ^ (1 / 2)
have conv_lhs : HPow.hPow (β := ℂ) ((↑π : ℂ) / c) 1 = ((↑π : ℂ) / c) ^ (1 / 2) * ((↑π : ℂ) / c) ^ (1 / 2)
Tactic: conv_lhs => rw [← cpow_one (↑π / c)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
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) * ((↑π : ℂ) / c) ^ (1 / 2)
have rw : HPow.hPow (β := ℂ) ((↑π : ℂ) / c) 1 = ((↑π : ℂ) / c) ^ (1 / 2 + 1 / 2)
Tactic: rw [← cpow_add _ _ (div_ne_zero (ofReal_ne_zero.mpr pi_ne_zero) (nv hc))]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℂ
hb : 0 < b.re
nv : ∀ {b : ℂ}, 0 < b.re → b ≠ 0
c : ℂ
hc : Membership.mem (γ := Set ℂ) {c : ℂ | 0 < c.re} c
⊢ ((↑π : ℂ) / c) ^ (1 / 2) ≠ 0
have rw : ¬(↑π : ℂ) / c = 0 ∨ ¬1 / 2 ≠ 0
Tactic: rw [Ne, cpow_eq_zero_iff, not_and_or]
-- 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 (x : ℝ) ↦
      cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) =
    ((↑π : ℂ) / b) ^ (1 / 2) / 2
have full_integral : (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) =
  ((↑π : ℂ) / b) ^ (1 / 2)
Tactic: have full_integral := integral_gaussian_complex hb
-- 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)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) =
    ((↑π : ℂ) / b) ^ (1 / 2) / 2
have this : MeasurableSet (α := ℝ) (Ioi 0)
Tactic: have : MeasurableSet (Ioi (0 : ℝ)) := measurableSet_Ioi