awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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) * x⁻¹) = 2 * rexp (-1 * HPow.hPow (β := ℕ) x 2)
have h : x ^ HSub.hSub (α := ℝ) 2 1 = x
Tactic: simp [field, (ne_of_lt (show 0 < x from hx)).symm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
⊢ √π = 2 * (√(π / 1) / 2)
have h : √π = 2 * (√π / 2)
Tactic: rw [div_one, ← mul_div_assoc, mul_comm, mul_div_cancel_right₀ _ (two_ne_zero' ℝ)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
h : √π = 2 * (√π / 2)
⊢ √π = 2 * (√(π / 1) / 2)
have h₁ : √π = 2 * √π / 2
Tactic: rw [div_one, ← mul_div_assoc, mul_comm, mul_div_cancel_right₀ _ (two_ne_zero' ℝ)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
h : √π = 2 * (√π / 2)
h₁ : √π = 2 * √π / 2
⊢ √π = 2 * (√(π / 1) / 2)
have h₂ : √π = √π * 2 / 2
Tactic: rw [div_one, ← mul_div_assoc, mul_comm, mul_div_cancel_right₀ _ (two_ne_zero' ℝ)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
h : √π = 2 * (√π / 2)
h₁ : √π = 2 * √π / 2
h₂ : √π = √π * 2 / 2
⊢ √π = 2 * (√(π / 1) / 2)
have h₃ : √π = √π
Tactic: rw [div_one, ← mul_div_assoc, mul_comm, mul_div_cancel_right₀ _ (two_ne_zero' ℝ)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
⊢ Gamma (1 / 2) = (↑π : ℂ) ^ (1 / 2)
have h : Gamma (1 / 2) = (↑(Real.Gamma (1 / 2)) : ℂ)
Tactic: convert! congr_arg ((↑) : ℝ → ℂ) Real.Gamma_one_half_eq
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
h : Gamma (1 / 2) = (↑(Real.Gamma (1 / 2)) : ℂ)
⊢ Gamma (1 / 2) = (↑π : ℂ) ^ (1 / 2)
have h₁ : (↑π : ℂ) ^ (1 / 2) = (↑√π : ℂ)
Tactic: convert! congr_arg ((↑) : ℝ → ℂ) Real.Gamma_one_half_eq
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
⊢ (↑π : ℂ) ^ (1 / 2) = (↑√π : ℂ)
have h : (↑π : ℂ) ^ (1 / 2) = (↑(π ^ (1 / 2)) : ℂ)
Tactic: rw [sqrt_eq_rpow, ofReal_cpow pi_pos.le, ofReal_div, ofReal_ofNat, ofReal_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
h : (↑π : ℂ) ^ (1 / 2) = (↑(π ^ (1 / 2)) : ℂ)
⊢ (↑π : ℂ) ^ (1 / 2) = (↑√π : ℂ)
have h₁ : (↑π : ℂ) ^ (1 / 2) = (↑π : ℂ) ^ (↑(1 / 2) : ℂ)
Tactic: rw [sqrt_eq_rpow, ofReal_cpow pi_pos.le, ofReal_div, ofReal_ofNat, ofReal_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
h : (↑π : ℂ) ^ (1 / 2) = (↑(π ^ (1 / 2)) : ℂ)
h₁ : (↑π : ℂ) ^ (1 / 2) = (↑π : ℂ) ^ (↑(1 / 2) : ℂ)
⊢ (↑π : ℂ) ^ (1 / 2) = (↑√π : ℂ)
have h₂ : (↑π : ℂ) ^ (1 / 2) = (↑π : ℂ) ^ ((↑1 : ℂ) / (↑2 : ℂ))
Tactic: rw [sqrt_eq_rpow, ofReal_cpow pi_pos.le, ofReal_div, ofReal_ofNat, ofReal_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
h : (↑π : ℂ) ^ (1 / 2) = (↑(π ^ (1 / 2)) : ℂ)
h₁ : (↑π : ℂ) ^ (1 / 2) = (↑π : ℂ) ^ (↑(1 / 2) : ℂ)
h₂ : (↑π : ℂ) ^ (1 / 2) = (↑π : ℂ) ^ ((↑1 : ℂ) / (↑2 : ℂ))
⊢ (↑π : ℂ) ^ (1 / 2) = (↑√π : ℂ)
have h₃ : (↑π : ℂ) ^ (1 / 2) = (↑π : ℂ) ^ ((↑1 : ℂ) / 2)
Tactic: rw [sqrt_eq_rpow, ofReal_cpow pi_pos.le, ofReal_div, ofReal_ofNat, ofReal_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
h : (↑π : ℂ) ^ (1 / 2) = (↑(π ^ (1 / 2)) : ℂ)
h₁ : (↑π : ℂ) ^ (1 / 2) = (↑π : ℂ) ^ (↑(1 / 2) : ℂ)
h₂ : (↑π : ℂ) ^ (1 / 2) = (↑π : ℂ) ^ ((↑1 : ℂ) / (↑2 : ℂ))
h₃ : (↑π : ℂ) ^ (1 / 2) = (↑π : ℂ) ^ ((↑1 : ℂ) / 2)
⊢ (↑π : ℂ) ^ (1 / 2) = (↑√π : ℂ)
have h₄ : (↑π : ℂ) ^ (1 / 2) = (↑π : ℂ) ^ HDiv.hDiv (α := ℂ) 1 2
Tactic: rw [sqrt_eq_rpow, ofReal_cpow pi_pos.le, ofReal_div, ofReal_ofNat, ofReal_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
⊢ Gamma (HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1 + 1 / 2) =
    (↑(HMul.hMul (α := ℕ) 2 0 + 1)‼ : ℝ) * √π / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 0 1)
have zero : 1 / 2 * √π = √π / 2
Tactic: simp [-one_div, add_comm (1 : ℝ), Gamma_add_one, Gamma_one_half_eq]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
k : ℕ
ih : Gamma (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 + 1 / 2) = (↑(2 * k + 1)‼ : ℝ) * √π / HPow.hPow (α := ℝ) 2 (k + 1)
⊢ Gamma (HAdd.hAdd (α := ℝ) (↑(k + 1) : ℝ) 1 + 1 / 2) =
    (↑(2 * (k + 1) + 1)‼ : ℝ) * √π / HPow.hPow (α := ℝ) 2 (k + 1 + 1)
have succ : (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 + 1 / 2) * ((↑(2 * k + 1)‼ : ℝ) * √π / HPow.hPow (α := ℝ) 2 (k + 1)) =
  (↑(2 * k + HMul.hMul (α := ℕ) 2 1 + 1)‼ : ℝ) * √π / HPow.hPow (α := ℝ) 2 (k + 1 + 1)
Tactic: rw [add_right_comm, Gamma_add_one (by positivity), Nat.cast_add, Nat.cast_one, ih, Nat.mul_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
k : ℕ
ih : Gamma (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 + 1 / 2) = (↑(2 * k + 1)‼ : ℝ) * √π / HPow.hPow (α := ℝ) 2 (k + 1)
⊢ (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 + 1 / 2) * ((↑(2 * k + 1)‼ : ℝ) * √π / HPow.hPow (α := ℝ) 2 (k + 1)) =
    (↑(2 * k + HMul.hMul (α := ℕ) 2 1 + 1)‼ : ℝ) * √π / HPow.hPow (α := ℝ) 2 (k + 1 + 1)
have succ : (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 + 2⁻¹) * ((↑(2 * k + 1)‼ : ℝ) * √π / HPow.hPow (α := ℝ) 2 (k + 1)) =
  (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1 + 2) * (↑(2 * k + 1)‼ : ℝ) * √π / HPow.hPow (α := ℝ) 2 (k + 1 + 1)
Tactic: simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
k : ℕ
⊢ Gamma (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 + 1 / 2) = (↑(2 * k + 1)‼ : ℝ) * √π / HPow.hPow (α := ℝ) 2 (k + 1)
have zero : Gamma (HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1 + 1 / 2) =
  (↑(HMul.hMul (α := ℕ) 2 0 + 1)‼ : ℝ) * √π / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 0 1)
Tactic: induction k with
  | zero => simp [-one_div, add_comm (1 : ℝ), Gamma_add_one, Gamma_one_half_eq]; ring
  | succ k ih =>
    rw [add_right_comm, Gamma_add_one (by positivity), Nat.cast_add, Nat.cast_one, ih, Nat.mul_add]
    simp
    ring
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
k : ℕ
zero :
  Gamma (HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1 + 1 / 2) =
    (↑(HMul.hMul (α := ℕ) 2 0 + 1)‼ : ℝ) * √π / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 0 1)
⊢ Gamma (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 + 1 / 2) = (↑(2 * k + 1)‼ : ℝ) * √π / HPow.hPow (α := ℝ) 2 (k + 1)
have succ : ∀ (k : ℕ)
  (ih : Gamma (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 + 1 / 2) = (↑(2 * k + 1)‼ : ℝ) * √π / HPow.hPow (α := ℝ) 2 (k + 1)),
  Gamma (HAdd.hAdd (α := ℝ) (↑(k + 1) : ℝ) 1 + 1 / 2) =
    (↑(2 * (k + 1) + 1)‼ : ℝ) * √π / HPow.hPow (α := ℝ) 2 (k + 1 + 1)
Tactic: induction k with
  | zero => simp [-one_div, add_comm (1 : ℝ), Gamma_add_one, Gamma_one_half_eq]; ring
  | succ k ih =>
    rw [add_right_comm, Gamma_add_one (by positivity), Nat.cast_add, Nat.cast_one, ih, Nat.mul_add]
    simp
    ring
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
k : ℕ
⊢ Gamma ((↑k : ℝ) + 1 / 2) = (↑(2 * k - 1)‼ : ℝ) * √π / HPow.hPow (α := ℝ) 2 k
have zero : Gamma ((↑0 : ℝ) + 1 / 2) = (↑(HMul.hMul (α := ℕ) 2 0 - 1)‼ : ℝ) * √π / HPow.hPow (α := ℝ) (β := ℕ) 2 0
Tactic: cases k with
  | zero => simp [-one_div, Gamma_one_half_eq]
  | succ k => simpa [-one_div, mul_add] using Gamma_nat_add_one_add_half k
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
k : ℕ
zero : Gamma ((↑0 : ℝ) + 1 / 2) = (↑(HMul.hMul (α := ℕ) 2 0 - 1)‼ : ℝ) * √π / HPow.hPow (α := ℝ) (β := ℕ) 2 0
⊢ Gamma ((↑k : ℝ) + 1 / 2) = (↑(2 * k - 1)‼ : ℝ) * √π / HPow.hPow (α := ℝ) 2 k
have succ : ∀ (k : ℕ), Gamma ((↑(k + 1) : ℝ) + 1 / 2) = (↑(2 * (k + 1) - 1)‼ : ℝ) * √π / HPow.hPow (α := ℝ) 2 (k + 1)
Tactic: cases k with
  | zero => simp [-one_div, Gamma_one_half_eq]
  | succ k => simpa [-one_div, mul_add] using Gamma_nat_add_one_add_half k
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation (goal)
Goal:
a : ℝ
ha : a < 0
b s : ℝ
this :
  IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ rexp (a * HPow.hPow (β := ℕ) x 2 + b * x)) fun (x : ℝ) ↦ rexp (-x)
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ rexp (a * HPow.hPow (β := ℕ) x 2 + b * x)) fun (x : ℝ) ↦ x ^ s
have refine : IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ rexp (-x)) fun (x : ℝ) ↦ x ^ s
Tactic: refine this.trans ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation (goal)
Goal:
a : ℝ
ha : a < 0
b s : ℝ
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ rexp (a * HPow.hPow (β := ℕ) x 2 + b * x)) fun (x : ℝ) ↦ x ^ s
have suffices : IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ rexp (a * HPow.hPow (β := ℕ) x 2 + b * x)) fun (x : ℝ) ↦ rexp (-x)
Tactic: suffices (fun x ↦ rexp (a * x ^ 2 + b * x)) =o[atTop] (fun x ↦ rexp (-x)) by
    refine this.trans ?_
    simpa only [neg_one_mul] using isLittleO_exp_neg_mul_rpow_atTop zero_lt_one s
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation (goal)
Goal:
a : ℝ
ha : a < 0
b s : ℝ
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ rexp (a * HPow.hPow (β := ℕ) x 2 + b * x)) fun (x : ℝ) ↦ rexp (-x)
have rw : Tendsto (β := ℝ) (fun (x : ℝ) ↦ -x - (a * HPow.hPow (β := ℕ) x 2 + b * x)) atTop atTop
Tactic: rw [isLittleO_exp_comp_exp_comp]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation (goal)
Goal:
a : ℝ
ha : a < 0
b s : ℝ
⊢ Eq (α := (x : ℝ) → ℝ) (fun (x : ℝ) ↦ -x - (a * HPow.hPow (β := ℕ) x 2 + b * x)) fun (x : ℝ) ↦ x * (-a * x - (b + 1))
have h : ∀ (x : ℝ), -x - (a * HPow.hPow (β := ℕ) x 2 + b * x) = x * (-a * x - (b + 1))
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation (hypothesis)
Goal:
a : ℝ
ha : a < 0
b s : ℝ
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ -x - (a * HPow.hPow (β := ℕ) x 2 + b * x)) atTop atTop
have this : Eq (α := (x : ℝ) → ℝ) (fun (x : ℝ) ↦ -x - (a * HPow.hPow (β := ℕ) x 2 + b * x)) fun (x : ℝ) ↦ x * (-a * x - (b + 1))
Tactic: have : (fun x ↦ -x - (a * x ^ 2 + b * x)) = fun x ↦ x * (-a * x - (b + 1)) := by
    ext1 x; ring_nf
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation (goal)
Goal:
a : ℝ
ha : a < 0
b s : ℝ
this :
  Eq (α := (x : ℝ) → ℝ) (fun (x : ℝ) ↦ -x - (a * HPow.hPow (β := ℕ) x 2 + b * x)) fun (x : ℝ) ↦ x * (-a * x - (b + 1))
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ -x - (a * HPow.hPow (β := ℕ) x 2 + b * x)) atTop atTop
have rw : Tendsto (β := ℝ) (fun (x : ℝ) ↦ x * (-a * x - (b + 1))) atTop atTop
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation (goal)
Goal:
a : ℂ
ha : a.re < 0
b : ℂ
s : ℝ
⊢ IsLittleO (E := ℂ) (F := ℝ) atTop (fun (x : ℝ) ↦ cexp (a * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + b * (↑x : ℂ)))
    fun (x : ℝ) ↦ x ^ s
have a₁ : IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ ‖cexp (a * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + b * (↑x : ℂ))‖)
  fun (x : ℝ) ↦ x ^ s
Tactic: apply Asymptotics.IsLittleO.of_norm_left
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation (goal)
Goal:
a : ℂ
ha : a.re < 0
b : ℂ
s : ℝ
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ ‖cexp (a * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + b * (↑x : ℂ))‖)
    fun (x : ℝ) ↦ x ^ s
have h : ∀ (x : ℝ), ‖cexp (a * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + b * (↑x : ℂ))‖ = rexp (a.re * HPow.hPow (β := ℕ) x 2 + b.re * x)
Tactic: convert! rexp_neg_quadratic_isLittleO_rpow_atTop ha b.re s with x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation (goal)
Goal:
a : ℂ
ha : a.re < 0
b : ℂ
s x : ℝ
⊢ ‖cexp (a * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + b * (↑x : ℂ))‖ = rexp (a.re * HPow.hPow (β := ℕ) x 2 + b.re * x)
have h : rexp (a * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + b * (↑x : ℂ)).re = rexp (a.re * HPow.hPow (β := ℕ) x 2 + b.re * x)
Tactic: simp_rw [Complex.norm_exp, add_re, ← ofReal_pow, mul_comm (_ : ℂ) ↑(_ : ℝ),
      re_ofReal_mul, mul_comm _ (re _)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation (goal)
Goal:
a : ℂ
ha : a.re < 0
b : ℂ
s x : ℝ
h : rexp (a * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + b * (↑x : ℂ)).re = rexp (a.re * HPow.hPow (β := ℕ) x 2 + b.re * x)
⊢ ‖cexp (a * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + b * (↑x : ℂ))‖ = rexp (a.re * HPow.hPow (β := ℕ) x 2 + b.re * x)
have h₁ : rexp ((a * HPow.hPow (β := ℕ) (↑x : ℂ) 2).re + (b * (↑x : ℂ)).re) = rexp (a.re * HPow.hPow (β := ℕ) x 2 + b.re * x)
Tactic: simp_rw [Complex.norm_exp, add_re, ← ofReal_pow, mul_comm (_ : ℂ) ↑(_ : ℝ),
      re_ofReal_mul, mul_comm _ (re _)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation (goal)
Goal:
a : ℂ
ha : a.re < 0
b : ℂ
s x : ℝ
h : rexp (a * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + b * (↑x : ℂ)).re = rexp (a.re * HPow.hPow (β := ℕ) x 2 + b.re * x)
h₁ : rexp ((a * HPow.hPow (β := ℕ) (↑x : ℂ) 2).re + (b * (↑x : ℂ)).re) = rexp (a.re * HPow.hPow (β := ℕ) x 2 + b.re * x)
⊢ ‖cexp (a * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + b * (↑x : ℂ))‖ = rexp (a.re * HPow.hPow (β := ℕ) x 2 + b.re * x)
have h₂ : rexp ((a * (↑(HPow.hPow (β := ℕ) x 2) : ℂ)).re + (b * (↑x : ℂ)).re) = rexp (a.re * HPow.hPow (β := ℕ) x 2 + b.re * x)
Tactic: simp_rw [Complex.norm_exp, add_re, ← ofReal_pow, mul_comm (_ : ℂ) ↑(_ : ℝ),
      re_ofReal_mul, mul_comm _ (re _)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation (goal)
Goal:
a : ℂ
ha : a.re < 0
b : ℂ
s x : ℝ
h : rexp (a * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + b * (↑x : ℂ)).re = rexp (a.re * HPow.hPow (β := ℕ) x 2 + b.re * x)
h₁ : rexp ((a * HPow.hPow (β := ℕ) (↑x : ℂ) 2).re + (b * (↑x : ℂ)).re) = rexp (a.re * HPow.hPow (β := ℕ) x 2 + b.re * x)
h₂ :
  rexp ((a * (↑(HPow.hPow (β := ℕ) x 2) : ℂ)).re + (b * (↑x : ℂ)).re) = rexp (a.re * HPow.hPow (β := ℕ) x 2 + b.re * x)
⊢ ‖cexp (a * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + b * (↑x : ℂ))‖ = rexp (a.re * HPow.hPow (β := ℕ) x 2 + b.re * x)
have h₃ : rexp (((↑(HPow.hPow (β := ℕ) x 2) : ℂ) * a).re + ((↑x : ℂ) * b).re) = rexp (a.re * HPow.hPow (β := ℕ) x 2 + b.re * x)
Tactic: simp_rw [Complex.norm_exp, add_re, ← ofReal_pow, mul_comm (_ : ℂ) ↑(_ : ℝ),
      re_ofReal_mul, mul_comm _ (re _)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation (goal)
Goal:
a : ℂ
ha : a.re < 0
b : ℂ
s x : ℝ
h : rexp (a * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + b * (↑x : ℂ)).re = rexp (a.re * HPow.hPow (β := ℕ) x 2 + b.re * x)
h₁ : rexp ((a * HPow.hPow (β := ℕ) (↑x : ℂ) 2).re + (b * (↑x : ℂ)).re) = rexp (a.re * HPow.hPow (β := ℕ) x 2 + b.re * x)
h₂ :
  rexp ((a * (↑(HPow.hPow (β := ℕ) x 2) : ℂ)).re + (b * (↑x : ℂ)).re) = rexp (a.re * HPow.hPow (β := ℕ) x 2 + b.re * x)
h₃ :
  rexp (((↑(HPow.hPow (β := ℕ) x 2) : ℂ) * a).re + ((↑x : ℂ) * b).re) = rexp (a.re * HPow.hPow (β := ℕ) x 2 + b.re * x)
⊢ ‖cexp (a * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + b * (↑x : ℂ))‖ = rexp (a.re * HPow.hPow (β := ℕ) x 2 + b.re * x)
have h₄ : rexp (HPow.hPow (β := ℕ) x 2 * a.re + x * b.re) = rexp (a.re * HPow.hPow (β := ℕ) x 2 + b.re * x)
Tactic: simp_rw [Complex.norm_exp, add_re, ← ofReal_pow, mul_comm (_ : ℂ) ↑(_ : ℝ),
      re_ofReal_mul, mul_comm _ (re _)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation (goal)
Goal:
a : ℂ
ha : a.re < 0
b : ℂ
s : ℝ
⊢ IsLittleO (E := ℂ) (F := ℝ) (cocompact ℝ) (fun (x : ℝ) ↦ cexp (a * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + b * (↑x : ℂ)))
    fun (x : ℝ) ↦ |x| ^ s
have rw : (IsLittleO (E := ℂ) (F := ℝ) atBot (fun (x : ℝ) ↦ cexp (a * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + b * (↑x : ℂ))) fun (x : ℝ) ↦
    |x| ^ s) ∧
  IsLittleO (E := ℂ) (F := ℝ) atTop (fun (x : ℝ) ↦ cexp (a * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + b * (↑x : ℂ)))
    fun (x : ℝ) ↦ |x| ^ s
Tactic: rw [cocompact_eq_atBot_atTop, isLittleO_sup]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation (goal)
Goal:
a : ℂ
ha : a.re < 0
b : ℂ
s : ℝ
⊢ (IsLittleO (E := ℂ) (F := ℝ) atBot (fun (x : ℝ) ↦ cexp (a * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + b * (↑x : ℂ)))
      fun (x : ℝ) ↦ |x| ^ s) ∧
    IsLittleO (E := ℂ) (F := ℝ) atTop (fun (x : ℝ) ↦ cexp (a * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + b * (↑x : ℂ)))
      fun (x : ℝ) ↦ |x| ^ s
have left : IsLittleO (E := ℂ) (F := ℝ) atBot (fun (x : ℝ) ↦ cexp (a * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + b * (↑x : ℂ))) fun (x : ℝ) ↦
  |x| ^ s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation (goal)
Goal:
a : ℂ
ha : a.re < 0
b : ℂ
s : ℝ
left :
  IsLittleO (E := ℂ) (F := ℝ) atBot (fun (x : ℝ) ↦ cexp (a * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + b * (↑x : ℂ)))
    fun (x : ℝ) ↦ |x| ^ s
⊢ (IsLittleO (E := ℂ) (F := ℝ) atBot (fun (x : ℝ) ↦ cexp (a * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + b * (↑x : ℂ)))
      fun (x : ℝ) ↦ |x| ^ s) ∧
    IsLittleO (E := ℂ) (F := ℝ) atTop (fun (x : ℝ) ↦ cexp (a * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + b * (↑x : ℂ)))
      fun (x : ℝ) ↦ |x| ^ s
have right : IsLittleO (E := ℂ) (F := ℝ) atTop (fun (x : ℝ) ↦ cexp (a * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + b * (↑x : ℂ))) fun (x : ℝ) ↦
  |x| ^ s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation (goal)
Goal:
a : ℂ
ha : a.re < 0
b : ℂ
s : ℝ
⊢ IsLittleO (E := ℂ) (F := ℝ) atBot (fun (x : ℝ) ↦ cexp (a * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + b * (↑x : ℂ)))
    fun (x : ℝ) ↦ |x| ^ s
have left : EventuallyEq (β := ℝ) atBot ((fun (x : ℝ) ↦ x ^ s) ∘ Neg.neg) fun (x : ℝ) ↦ |x| ^ s
Tactic: refine ((cexp_neg_quadratic_isLittleO_rpow_atTop ha (-b) s).comp_tendsto
      Filter.tendsto_neg_atBot_atTop).congr' (Eventually.of_forall fun x ↦ by simp) ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation (goal)
Goal:
a : ℂ
ha : a.re < 0
b : ℂ
s : ℝ
⊢ EventuallyEq (β := ℝ) atBot ((fun (x : ℝ) ↦ x ^ s) ∘ Neg.neg) fun (x : ℝ) ↦ |x| ^ s
have left : ∀ (x : ℝ) (hx : x < 0), Eq (α := ℝ) (((fun (x : ℝ) ↦ x ^ s) ∘ Neg.neg) x) ((fun (x : ℝ) ↦ |x| ^ s) x)
Tactic: refine (eventually_lt_atBot 0).mp (Eventually.of_forall fun x hx ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation (goal)
Goal:
a : ℂ
ha : a.re < 0
b : ℂ
s : ℝ
⊢ IsLittleO (E := ℂ) (F := ℝ) atTop (fun (x : ℝ) ↦ cexp (a * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + b * (↑x : ℂ)))
    fun (x : ℝ) ↦ |x| ^ s
have right : EventuallyEq (β := ℝ) atTop (fun (x : ℝ) ↦ x ^ s) fun (x : ℝ) ↦ |x| ^ s
Tactic: refine (cexp_neg_quadratic_isLittleO_rpow_atTop ha b s).congr' EventuallyEq.rfl ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation (goal)
Goal:
a : ℂ
ha : a.re < 0
b : ℂ
s : ℝ
⊢ EventuallyEq (β := ℝ) atTop (fun (x : ℝ) ↦ x ^ s) fun (x : ℝ) ↦ |x| ^ s
have right : ∀ (x : ℝ) (hx : 0 < x), Eq (α := ℝ) ((fun (x : ℝ) ↦ x ^ s) x) ((fun (x : ℝ) ↦ |x| ^ s) x)
Tactic: refine (eventually_gt_atTop 0).mp (Eventually.of_forall fun x hx ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation (goal)
Goal:
a : ℝ
ha : 0 < a
s x : ℝ
| rexp (-a * HPow.hPow (β := ℕ) x 2)
have rw : rexp (-a * HPow.hPow (β := ℕ) |x| 2)
Tactic: rw [← sq_abs]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation (goal)
Goal:
a : ℝ
ha : 0 < a
s : ℝ
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ |x| ^ s * rexp (-a * HPow.hPow (β := ℕ) x 2)) (cocompact ℝ) (𝓝 0)
have conv : Tendsto (β := ℝ) (fun (x : ℝ) ↦ |x| ^ s * rexp (-a * HPow.hPow (β := ℕ) |x| 2)) (cocompact ℝ) (𝓝 0)
Tactic: conv in rexp _ => rw [← sq_abs]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation (goal)
Goal:
a : ℝ
ha : 0 < a
s : ℝ
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ |x| ^ s * rexp (-a * HPow.hPow (β := ℕ) |x| 2)) (cocompact ℝ) (𝓝 0)
have rw : Tendsto (β := ℝ) (fun (x : ℝ) ↦ |x| ^ s * rexp (-a * HPow.hPow (β := ℕ) |x| 2)) (comap abs atTop) (𝓝 0)
Tactic: rw [cocompact_eq_atBot_atTop, ← comap_abs_atTop]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation (goal)
Goal:
a : ℝ
ha : 0 < a
s : ℝ
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ |x| ^ s * rexp (-a * HPow.hPow (β := ℕ) |x| 2)) (comap abs atTop) (𝓝 0)
have erw : Tendsto (β := ℝ) (fun (y : ℝ) ↦ y ^ s * rexp (-a * HPow.hPow (β := ℕ) y 2)) atTop (𝓝 0)
Tactic: erw [tendsto_comap'_iff (m := fun y => y ^ s * rexp (-a * y ^ 2))
      (mem_atTop_sets.mpr ⟨0, fun b hb => ⟨b, abs_of_nonneg hb⟩⟩)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation (goal)
Goal:
a : ℂ
ha : 0 < a.re
s : ℝ
⊢ IsLittleO (E := ℂ) (F := ℝ) (cocompact ℝ) (fun (x : ℝ) ↦ cexp (-a * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) fun (x : ℝ) ↦
    |x| ^ s
have h : Eq (α := ℝ → ℂ) (fun (x : ℝ) ↦ cexp (-a * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) fun (x : ℝ) ↦
  cexp (-a * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + 0 * (↑x : ℂ))
Tactic: convert! cexp_neg_quadratic_isLittleO_abs_rpow_cocompact (?_ : (-a).re < 0) 0 s using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation (goal)
Goal:
a : ℂ
ha : 0 < a.re
s : ℝ
h :
  Eq (α := ℝ → ℂ) (fun (x : ℝ) ↦ cexp (-a * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) fun (x : ℝ) ↦
    cexp (-a * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + 0 * (↑x : ℂ))
⊢ IsLittleO (E := ℂ) (F := ℝ) (cocompact ℝ) (fun (x : ℝ) ↦ cexp (-a * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) fun (x : ℝ) ↦
    |x| ^ s
have convert! : (-a).re < 0
Tactic: convert! cexp_neg_quadratic_isLittleO_abs_rpow_cocompact (?_ : (-a).re < 0) 0 s using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation (goal)
Goal:
a : ℂ
ha : 0 < a.re
s : ℝ
⊢ Eq (α := ℝ → ℂ) (fun (x : ℝ) ↦ cexp (-a * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) fun (x : ℝ) ↦
    cexp (-a * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + 0 * (↑x : ℂ))
have h : Eq (α := ℝ → ℂ) (fun (x : ℝ) ↦ cexp (-a * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) fun (x : ℝ) ↦
  cexp (-a * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + 0)
Tactic: simp_rw [zero_mul, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation (goal)
Goal:
a : ℂ
ha : 0 < a.re
s : ℝ
⊢ (-a).re < 0
have rwa : -a.re < 0
Tactic: rwa [neg_re, neg_lt_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation (goal)
Goal:
a : ℂ
ha : 0 < a.re
b : ℂ
f : ℝ → ℂ := fun (x : ℝ) ↦ cexp (-(↑π : ℂ) * a * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + 2 * (↑π : ℂ) * b * (↑x : ℂ))
⊢ Continuous f
have refine_1 : Continuous (Y := ℂ) fun (x : ℝ) ↦ -(↑π : ℂ) * a * HPow.hPow (β := ℕ) (↑x : ℂ) 2
Tactic: refine Complex.continuous_exp.comp (Continuous.add ?_ ?_)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation (goal)
Goal:
a : ℂ
ha : 0 < a.re
b : ℂ
f : ℝ → ℂ := fun (x : ℝ) ↦ cexp (-(↑π : ℂ) * a * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + 2 * (↑π : ℂ) * b * (↑x : ℂ))
refine_1 : Continuous (Y := ℂ) fun (x : ℝ) ↦ -(↑π : ℂ) * a * HPow.hPow (β := ℕ) (↑x : ℂ) 2
⊢ Continuous f
have refine_2 : Continuous (Y := ℂ) fun (x : ℝ) ↦ 2 * (↑π : ℂ) * b * (↑x : ℂ)
Tactic: refine Complex.continuous_exp.comp (Continuous.add ?_ ?_)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation (hypothesis)
Goal:
a : ℂ
ha : 0 < a.re
b : ℂ
f : ℝ → ℂ := fun (x : ℝ) ↦ cexp (-(↑π : ℂ) * a * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + 2 * (↑π : ℂ) * b * (↑x : ℂ))
⊢ ∑' (n : ℤ), cexp (-(↑π : ℂ) * a * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 + 2 * (↑π : ℂ) * b * (↑n : ℂ)) =
    1 / a ^ (1 / 2) * ∑' (n : ℤ), cexp (-(↑π : ℂ) / a * HPow.hPow (β := ℕ) ((↑n : ℂ) + I * b) 2)
have hCf : Continuous f
Tactic: have hCf : Continuous f := by
    refine Complex.continuous_exp.comp (Continuous.add ?_ ?_)
    · exact continuous_const.mul (Complex.continuous_ofReal.pow 2)
    · exact continuous_const.mul Complex.continuous_ofReal
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation (hypothesis)
Goal:
a : ℂ
ha : 0 < a.re
b : ℂ
f : ℝ → ℂ := fun (x : ℝ) ↦ cexp (-(↑π : ℂ) * a * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + 2 * (↑π : ℂ) * b * (↑x : ℂ))
hCf : Continuous f
⊢ ∑' (n : ℤ), cexp (-(↑π : ℂ) * a * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 + 2 * (↑π : ℂ) * b * (↑n : ℂ)) =
    1 / a ^ (1 / 2) * ∑' (n : ℤ), cexp (-(↑π : ℂ) / a * HPow.hPow (β := ℕ) ((↑n : ℂ) + I * b) 2)
have hFf : 𝓕 f = fun (x : ℝ) ↦ 1 / a ^ (1 / 2) * cexp (-(↑π : ℂ) / a * HPow.hPow (β := ℕ) ((↑x : ℂ) + I * b) 2)
Tactic: have hFf : 𝓕 f = fun x : ℝ ↦ 1 / a ^ (1 / 2 : ℂ) * cexp (-π / a * (x + I * b) ^ 2) :=
    fourier_gaussian_pi' ha b