awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℂ))
hCf : Continuous f
hFf : 𝓕 f = fun (x : ℝ) ↦ 1 / a ^ (1 / 2) * cexp (-(↑π : ℂ) / a * HPow.hPow (β := ℕ) ((↑x : ℂ) + I * b) 2)
⊢ 0 < ((↑π : ℂ) * a).re
have rw : 0 < π * a.re
Tactic: rw [re_ofReal_mul]
-- 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
hFf : 𝓕 f = fun (x : ℝ) ↦ 1 / a ^ (1 / 2) * cexp (-(↑π : ℂ) / a * HPow.hPow (β := ℕ) ((↑x : ℂ) + I * b) 2)
⊢ ∑' (n : ℤ), cexp (-(↑π : ℂ) * a * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 + 2 * (↑π : ℂ) * b * (↑n : ℂ)) =
    1 / a ^ (1 / 2) * ∑' (n : ℤ), cexp (-(↑π : ℂ) / a * HPow.hPow (β := ℕ) ((↑n : ℂ) + I * b) 2)
have h1 : 0 < ((↑π : ℂ) * a).re
Tactic: have h1 : 0 < (↑π * a).re := by
    rw [re_ofReal_mul]
    exact mul_pos pi_pos ha
-- 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 : ℂ))
hCf : Continuous f
hFf : 𝓕 f = fun (x : ℝ) ↦ 1 / a ^ (1 / 2) * cexp (-(↑π : ℂ) / a * HPow.hPow (β := ℕ) ((↑x : ℂ) + I * b) 2)
h1 : 0 < ((↑π : ℂ) * a).re
⊢ 0 < ((↑π : ℂ) / a).re
have rw : 0 < π * HDiv.hDiv (β := ℝ) a.re ((normSq : (a : ℂ) → ℝ) a : ℝ)
Tactic: rw [div_eq_mul_inv, re_ofReal_mul, inv_re]
-- 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 : ℂ))
hCf : Continuous f
hFf : 𝓕 f = fun (x : ℝ) ↦ 1 / a ^ (1 / 2) * cexp (-(↑π : ℂ) / a * HPow.hPow (β := ℕ) ((↑x : ℂ) + I * b) 2)
h1 : 0 < ((↑π : ℂ) * a).re
⊢ 0 < π * HDiv.hDiv (β := ℝ) a.re ((normSq : (a : ℂ) → ℝ) a : ℝ)
have refine : a ≠ 0
Tactic: refine mul_pos pi_pos (div_pos ha <| normSq_pos.mpr ?_)
-- 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 : ℂ))
hCf : Continuous f
hFf : 𝓕 f = fun (x : ℝ) ↦ 1 / a ^ (1 / 2) * cexp (-(↑π : ℂ) / a * HPow.hPow (β := ℕ) ((↑x : ℂ) + I * b) 2)
h1 : 0 < ((↑π : ℂ) * a).re
⊢ a ≠ 0
have contrapose! : ∀ (ha : a = 0), a.re ≤ 0
Tactic: contrapose! ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation (goal)
Goal:
a b : ℂ
f : ℝ → ℂ := fun (x : ℝ) ↦ cexp (-(↑π : ℂ) * a * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + 2 * (↑π : ℂ) * b * (↑x : ℂ))
hCf : Continuous f
hFf : 𝓕 f = fun (x : ℝ) ↦ 1 / a ^ (1 / 2) * cexp (-(↑π : ℂ) / a * HPow.hPow (β := ℕ) ((↑x : ℂ) + I * b) 2)
h1 : 0 < ((↑π : ℂ) * a).re
ha : a = 0
⊢ a.re ≤ 0
have rw : re 0 ≤ 0
Tactic: rw [ha, zero_re]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation (goal)
Goal:
a b : ℂ
f : ℝ → ℂ := fun (x : ℝ) ↦ cexp (-(↑π : ℂ) * a * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + 2 * (↑π : ℂ) * b * (↑x : ℂ))
hCf : Continuous f
hFf : 𝓕 f = fun (x : ℝ) ↦ 1 / a ^ (1 / 2) * cexp (-(↑π : ℂ) / a * HPow.hPow (β := ℕ) ((↑x : ℂ) + I * b) 2)
h1 : 0 < ((↑π : ℂ) * a).re
ha : a = 0
rw : re 0 ≤ 0
⊢ a.re ≤ 0
have rw₁ : LE.le (α := ℝ) 0 0
Tactic: rw [ha, zero_re]
-- 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
hFf : 𝓕 f = fun (x : ℝ) ↦ 1 / a ^ (1 / 2) * cexp (-(↑π : ℂ) / a * HPow.hPow (β := ℕ) ((↑x : ℂ) + I * b) 2)
h1 : 0 < ((↑π : ℂ) * a).re
⊢ ∑' (n : ℤ), cexp (-(↑π : ℂ) * a * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 + 2 * (↑π : ℂ) * b * (↑n : ℂ)) =
    1 / a ^ (1 / 2) * ∑' (n : ℤ), cexp (-(↑π : ℂ) / a * HPow.hPow (β := ℕ) ((↑n : ℂ) + I * b) 2)
have h2 : 0 < ((↑π : ℂ) / a).re
Tactic: have h2 : 0 < (↑π / a).re := by
    rw [div_eq_mul_inv, re_ofReal_mul, inv_re]
    refine mul_pos pi_pos (div_pos ha <| normSq_pos.mpr ?_)
    contrapose! ha
    rw [ha, zero_re]
-- 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 : ℂ))
hCf : Continuous f
hFf : 𝓕 f = fun (x : ℝ) ↦ 1 / a ^ (1 / 2) * cexp (-(↑π : ℂ) / a * HPow.hPow (β := ℕ) ((↑x : ℂ) + I * b) 2)
h1 : 0 < ((↑π : ℂ) * a).re
h2 : 0 < ((↑π : ℂ) / a).re
⊢ IsBigO (F := ℝ) (cocompact ℝ) f fun (x : ℝ) ↦ HPow.hPow (β := ℝ) |x| (-2)
have convert_2 : (-(↑π : ℂ) * a).re < 0
Tactic: convert! (cexp_neg_quadratic_isLittleO_abs_rpow_cocompact ?_ _ (-2)).isBigO
-- 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 : ℂ))
hCf : Continuous f
hFf : 𝓕 f = fun (x : ℝ) ↦ 1 / a ^ (1 / 2) * cexp (-(↑π : ℂ) / a * HPow.hPow (β := ℕ) ((↑x : ℂ) + I * b) 2)
h1 : 0 < ((↑π : ℂ) * a).re
h2 : 0 < ((↑π : ℂ) / a).re
⊢ (-(↑π : ℂ) * a).re < 0
have convert_2 : (-((↑π : ℂ) * a)).re < 0
Tactic: rwa [neg_mul, 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 : ℂ))
hCf : Continuous f
hFf : 𝓕 f = fun (x : ℝ) ↦ 1 / a ^ (1 / 2) * cexp (-(↑π : ℂ) / a * HPow.hPow (β := ℕ) ((↑x : ℂ) + I * b) 2)
h1 : 0 < ((↑π : ℂ) * a).re
h2 : 0 < ((↑π : ℂ) / a).re
convert_2 : (-((↑π : ℂ) * a)).re < 0
⊢ (-(↑π : ℂ) * a).re < 0
have convert_2₁ : -((↑π : ℂ) * a).re < 0
Tactic: rwa [neg_mul, neg_re, neg_lt_zero]
-- 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
hFf : 𝓕 f = fun (x : ℝ) ↦ 1 / a ^ (1 / 2) * cexp (-(↑π : ℂ) / a * HPow.hPow (β := ℕ) ((↑x : ℂ) + I * b) 2)
h1 : 0 < ((↑π : ℂ) * a).re
h2 : 0 < ((↑π : ℂ) / a).re
⊢ ∑' (n : ℤ), cexp (-(↑π : ℂ) * a * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 + 2 * (↑π : ℂ) * b * (↑n : ℂ)) =
    1 / a ^ (1 / 2) * ∑' (n : ℤ), cexp (-(↑π : ℂ) / a * HPow.hPow (β := ℕ) ((↑n : ℂ) + I * b) 2)
have f_bd : IsBigO (F := ℝ) (cocompact ℝ) f fun (x : ℝ) ↦ HPow.hPow (β := ℝ) |x| (-2)
Tactic: have f_bd : f =O[cocompact ℝ] (fun x => |x| ^ (-2 : ℝ)) := by
    convert! (cexp_neg_quadratic_isLittleO_abs_rpow_cocompact ?_ _ (-2)).isBigO
    rwa [neg_mul, 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 : ℂ))
hCf : Continuous f
hFf : 𝓕 f = fun (x : ℝ) ↦ 1 / a ^ (1 / 2) * cexp (-(↑π : ℂ) / a * HPow.hPow (β := ℕ) ((↑x : ℂ) + I * b) 2)
h1 : 0 < ((↑π : ℂ) * a).re
h2 : 0 < ((↑π : ℂ) / a).re
f_bd : IsBigO (F := ℝ) (cocompact ℝ) f fun (x : ℝ) ↦ HPow.hPow (β := ℝ) |x| (-2)
⊢ IsBigO (F := ℝ) (cocompact ℝ) (𝓕 f) fun (x : ℝ) ↦ HPow.hPow (β := ℝ) |x| (-2)
have rw : IsBigO (E := ℂ) (F := ℝ) (cocompact ℝ)
  (fun (x : ℝ) ↦ 1 / a ^ (1 / 2) * cexp (-(↑π : ℂ) / a * HPow.hPow (β := ℕ) ((↑x : ℂ) + I * b) 2)) fun (x : ℝ) ↦
  HPow.hPow (β := ℝ) |x| (-2)
Tactic: rw [hFf]
-- 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 : ℂ))
hCf : Continuous f
hFf : 𝓕 f = fun (x : ℝ) ↦ 1 / a ^ (1 / 2) * cexp (-(↑π : ℂ) / a * HPow.hPow (β := ℕ) ((↑x : ℂ) + I * b) 2)
h1 : 0 < ((↑π : ℂ) * a).re
h2 : 0 < ((↑π : ℂ) / a).re
f_bd : IsBigO (F := ℝ) (cocompact ℝ) f fun (x : ℝ) ↦ HPow.hPow (β := ℝ) |x| (-2)
x : ℝ
⊢ -(↑π : ℂ) / a * HPow.hPow (β := ℕ) ((↑x : ℂ) + I * b) 2 =
    -(↑π : ℂ) / a * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + -2 * (↑π : ℂ) * I * b / a * (↑x : ℂ) +
      (↑π : ℂ) * HPow.hPow (β := ℕ) b 2 / a
have ring_nf : -((↑π : ℂ) * a⁻¹ * (↑x : ℂ) * I * b * 2) - (↑π : ℂ) * a⁻¹ * HPow.hPow (β := ℕ) (↑x : ℂ) 2 -
    (↑π : ℂ) * a⁻¹ * HPow.hPow (β := ℕ) I 2 * HPow.hPow (β := ℕ) b 2 =
  -((↑π : ℂ) * a⁻¹ * (↑x : ℂ) * I * b * 2) - (↑π : ℂ) * a⁻¹ * HPow.hPow (β := ℕ) (↑x : ℂ) 2 +
    (↑π : ℂ) * a⁻¹ * HPow.hPow (β := ℕ) b 2
Tactic: ring_nf
-- 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 : ℂ))
hCf : Continuous f
hFf : 𝓕 f = fun (x : ℝ) ↦ 1 / a ^ (1 / 2) * cexp (-(↑π : ℂ) / a * HPow.hPow (β := ℕ) ((↑x : ℂ) + I * b) 2)
h1 : 0 < ((↑π : ℂ) * a).re
h2 : 0 < ((↑π : ℂ) / a).re
f_bd : IsBigO (F := ℝ) (cocompact ℝ) f fun (x : ℝ) ↦ HPow.hPow (β := ℝ) |x| (-2)
x : ℝ
⊢ -((↑π : ℂ) * a⁻¹ * (↑x : ℂ) * I * b * 2) - (↑π : ℂ) * a⁻¹ * HPow.hPow (β := ℕ) (↑x : ℂ) 2 -
      (↑π : ℂ) * a⁻¹ * HPow.hPow (β := ℕ) I 2 * HPow.hPow (β := ℕ) b 2 =
    -((↑π : ℂ) * a⁻¹ * (↑x : ℂ) * I * b * 2) - (↑π : ℂ) * a⁻¹ * HPow.hPow (β := ℕ) (↑x : ℂ) 2 +
      (↑π : ℂ) * a⁻¹ * HPow.hPow (β := ℕ) b 2
have rw : -((↑π : ℂ) * a⁻¹ * (↑x : ℂ) * I * b * 2) - (↑π : ℂ) * a⁻¹ * HPow.hPow (β := ℕ) (↑x : ℂ) 2 -
    (↑π : ℂ) * a⁻¹ * -1 * HPow.hPow (β := ℕ) b 2 =
  -((↑π : ℂ) * a⁻¹ * (↑x : ℂ) * I * b * 2) - (↑π : ℂ) * a⁻¹ * HPow.hPow (β := ℕ) (↑x : ℂ) 2 +
    (↑π : ℂ) * a⁻¹ * HPow.hPow (β := ℕ) b 2
Tactic: rw [I_sq]
-- 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
hFf : 𝓕 f = fun (x : ℝ) ↦ 1 / a ^ (1 / 2) * cexp (-(↑π : ℂ) / a * HPow.hPow (β := ℕ) ((↑x : ℂ) + I * b) 2)
h1 : 0 < ((↑π : ℂ) * a).re
h2 : 0 < ((↑π : ℂ) / a).re
f_bd : IsBigO (F := ℝ) (cocompact ℝ) f fun (x : ℝ) ↦ HPow.hPow (β := ℝ) |x| (-2)
⊢ IsBigO (E := ℂ) (F := ℝ) (cocompact ℝ)
    (fun (x : ℝ) ↦ 1 / a ^ (1 / 2) * cexp (-(↑π : ℂ) / a * HPow.hPow (β := ℕ) ((↑x : ℂ) + I * b) 2)) fun (x : ℝ) ↦
    HPow.hPow (β := ℝ) |x| (-2)
have this : ∀ (x : ℝ),
  -(↑π : ℂ) / a * HPow.hPow (β := ℕ) ((↑x : ℂ) + I * b) 2 =
    -(↑π : ℂ) / a * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + -2 * (↑π : ℂ) * I * b / a * (↑x : ℂ) +
      (↑π : ℂ) * HPow.hPow (β := ℕ) b 2 / a
Tactic: have : ∀ (x : ℝ), -↑π / a * (↑x + I * b) ^ 2 =
        -↑π / a * x ^ 2 + (-2 * π * I * b) / a * x + π * b ^ 2 / a := by
      intro x; ring_nf; rw [I_sq]; ring
-- 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 : ℂ))
hCf : Continuous f
hFf : 𝓕 f = fun (x : ℝ) ↦ 1 / a ^ (1 / 2) * cexp (-(↑π : ℂ) / a * HPow.hPow (β := ℕ) ((↑x : ℂ) + I * b) 2)
h1 : 0 < ((↑π : ℂ) * a).re
h2 : 0 < ((↑π : ℂ) / a).re
f_bd : IsBigO (F := ℝ) (cocompact ℝ) f fun (x : ℝ) ↦ HPow.hPow (β := ℝ) |x| (-2)
this :
  ∀ (x : ℝ),
    -(↑π : ℂ) / a * HPow.hPow (β := ℕ) ((↑x : ℂ) + I * b) 2 =
      -(↑π : ℂ) / a * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + -2 * (↑π : ℂ) * I * b / a * (↑x : ℂ) +
        (↑π : ℂ) * HPow.hPow (β := ℕ) b 2 / a
⊢ IsBigO (E := ℂ) (F := ℝ) (cocompact ℝ)
    (fun (x : ℝ) ↦ 1 / a ^ (1 / 2) * cexp (-(↑π : ℂ) / a * HPow.hPow (β := ℕ) ((↑x : ℂ) + I * b) 2)) fun (x : ℝ) ↦
    HPow.hPow (β := ℝ) |x| (-2)
have simp_rw : IsBigO (E := ℂ) (F := ℝ) (cocompact ℝ)
  (fun (x : ℝ) ↦
    1 / a ^ (1 / 2) *
      cexp
        (-(↑π : ℂ) / a * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + -2 * (↑π : ℂ) * I * b / a * (↑x : ℂ) +
          (↑π : ℂ) * HPow.hPow (β := ℕ) b 2 / a))
  fun (x : ℝ) ↦ HPow.hPow (β := ℝ) |x| (-2)
Tactic: simp_rw [this]
-- 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 : ℂ))
hCf : Continuous f
hFf : 𝓕 f = fun (x : ℝ) ↦ 1 / a ^ (1 / 2) * cexp (-(↑π : ℂ) / a * HPow.hPow (β := ℕ) ((↑x : ℂ) + I * b) 2)
h1 : 0 < ((↑π : ℂ) * a).re
h2 : 0 < ((↑π : ℂ) / a).re
f_bd : IsBigO (F := ℝ) (cocompact ℝ) f fun (x : ℝ) ↦ HPow.hPow (β := ℝ) |x| (-2)
this :
  ∀ (x : ℝ),
    -(↑π : ℂ) / a * HPow.hPow (β := ℕ) ((↑x : ℂ) + I * b) 2 =
      -(↑π : ℂ) / a * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + -2 * (↑π : ℂ) * I * b / a * (↑x : ℂ) +
        (↑π : ℂ) * HPow.hPow (β := ℕ) b 2 / a
| IsBigO (E := ℂ) (F := ℝ) (cocompact ℝ)
    (fun (x : ℝ) ↦
      1 / a ^ (1 / 2) *
        cexp
          (-(↑π : ℂ) / a * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + -2 * (↑π : ℂ) * I * b / a * (↑x : ℂ) +
            (↑π : ℂ) * HPow.hPow (β := ℕ) b 2 / a))
    fun (x : ℝ) ↦ HPow.hPow (β := ℝ) |x| (-2)
have h : ∀ (x : ℝ),
  1 / a ^ (1 / 2) *
    cexp
      (-(↑π : ℂ) / a * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + -2 * (↑π : ℂ) * I * b / a * (↑x : ℂ) +
        (↑π : ℂ) * HPow.hPow (β := ℕ) b 2 / a)
Tactic: enter [2, x]
-- 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 : ℂ))
hCf : Continuous f
hFf : 𝓕 f = fun (x : ℝ) ↦ 1 / a ^ (1 / 2) * cexp (-(↑π : ℂ) / a * HPow.hPow (β := ℕ) ((↑x : ℂ) + I * b) 2)
h1 : 0 < ((↑π : ℂ) * a).re
h2 : 0 < ((↑π : ℂ) / a).re
f_bd : IsBigO (F := ℝ) (cocompact ℝ) f fun (x : ℝ) ↦ HPow.hPow (β := ℝ) |x| (-2)
this :
  ∀ (x : ℝ),
    -(↑π : ℂ) / a * HPow.hPow (β := ℕ) ((↑x : ℂ) + I * b) 2 =
      -(↑π : ℂ) / a * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + -2 * (↑π : ℂ) * I * b / a * (↑x : ℂ) +
        (↑π : ℂ) * HPow.hPow (β := ℕ) b 2 / a
x : ℝ
| 1 / a ^ (1 / 2) *
    cexp
      (-(↑π : ℂ) / a * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + -2 * (↑π : ℂ) * I * b / a * (↑x : ℂ) +
        (↑π : ℂ) * HPow.hPow (β := ℕ) b 2 / a)
have h : cexp ((↑π : ℂ) * HPow.hPow (β := ℕ) b 2 / a) *
  (1 / a ^ (1 / 2) * cexp (-(↑π : ℂ) / a * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + -2 * (↑π : ℂ) * I * b / a * (↑x : ℂ)))
Tactic: rw [Complex.exp_add, ← mul_assoc _ _ (Complex.exp _), mul_comm]
-- 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 : ℂ))
hCf : Continuous f
hFf : 𝓕 f = fun (x : ℝ) ↦ 1 / a ^ (1 / 2) * cexp (-(↑π : ℂ) / a * HPow.hPow (β := ℕ) ((↑x : ℂ) + I * b) 2)
h1 : 0 < ((↑π : ℂ) * a).re
h2 : 0 < ((↑π : ℂ) / a).re
f_bd : IsBigO (F := ℝ) (cocompact ℝ) f fun (x : ℝ) ↦ HPow.hPow (β := ℝ) |x| (-2)
this :
  ∀ (x : ℝ),
    -(↑π : ℂ) / a * HPow.hPow (β := ℕ) ((↑x : ℂ) + I * b) 2 =
      -(↑π : ℂ) / a * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + -2 * (↑π : ℂ) * I * b / a * (↑x : ℂ) +
        (↑π : ℂ) * HPow.hPow (β := ℕ) b 2 / a
| IsBigO (E := ℂ) (F := ℝ) (cocompact ℝ)
    (fun (x : ℝ) ↦
      1 / a ^ (1 / 2) *
        cexp
          (-(↑π : ℂ) / a * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + -2 * (↑π : ℂ) * I * b / a * (↑x : ℂ) +
            (↑π : ℂ) * HPow.hPow (β := ℕ) b 2 / a))
    fun (x : ℝ) ↦ HPow.hPow (β := ℝ) |x| (-2)
have h : ∀ (x : ℝ),
  cexp ((↑π : ℂ) * HPow.hPow (β := ℕ) b 2 / a) *
    (1 / a ^ (1 / 2) * cexp (-(↑π : ℂ) / a * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + -2 * (↑π : ℂ) * I * b / a * (↑x : ℂ)))
Tactic: enter [2, x]; rw [Complex.exp_add, ← mul_assoc _ _ (Complex.exp _), mul_comm]
-- 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 : ℂ))
hCf : Continuous f
hFf : 𝓕 f = fun (x : ℝ) ↦ 1 / a ^ (1 / 2) * cexp (-(↑π : ℂ) / a * HPow.hPow (β := ℕ) ((↑x : ℂ) + I * b) 2)
h1 : 0 < ((↑π : ℂ) * a).re
h2 : 0 < ((↑π : ℂ) / a).re
f_bd : IsBigO (F := ℝ) (cocompact ℝ) f fun (x : ℝ) ↦ HPow.hPow (β := ℝ) |x| (-2)
this :
  ∀ (x : ℝ),
    -(↑π : ℂ) / a * HPow.hPow (β := ℕ) ((↑x : ℂ) + I * b) 2 =
      -(↑π : ℂ) / a * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + -2 * (↑π : ℂ) * I * b / a * (↑x : ℂ) +
        (↑π : ℂ) * HPow.hPow (β := ℕ) b 2 / a
⊢ IsBigO (E := ℂ) (F := ℝ) (cocompact ℝ)
    (fun (x : ℝ) ↦
      1 / a ^ (1 / 2) *
        cexp
          (-(↑π : ℂ) / a * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + -2 * (↑π : ℂ) * I * b / a * (↑x : ℂ) +
            (↑π : ℂ) * HPow.hPow (β := ℕ) b 2 / a))
    fun (x : ℝ) ↦ HPow.hPow (β := ℝ) |x| (-2)
have conv : IsBigO (E := ℂ) (F := ℝ) (cocompact ℝ)
  (fun (x : ℝ) ↦
    cexp ((↑π : ℂ) * HPow.hPow (β := ℕ) b 2 / a) *
      (1 / a ^ (1 / 2) * cexp (-(↑π : ℂ) / a * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + -2 * (↑π : ℂ) * I * b / a * (↑x : ℂ))))
  fun (x : ℝ) ↦ HPow.hPow (β := ℝ) |x| (-2)
Tactic: conv => enter [2, x]; rw [Complex.exp_add, ← mul_assoc _ _ (Complex.exp _), mul_comm]
-- 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 : ℂ))
hCf : Continuous f
hFf : 𝓕 f = fun (x : ℝ) ↦ 1 / a ^ (1 / 2) * cexp (-(↑π : ℂ) / a * HPow.hPow (β := ℕ) ((↑x : ℂ) + I * b) 2)
h1 : 0 < ((↑π : ℂ) * a).re
h2 : 0 < ((↑π : ℂ) / a).re
f_bd : IsBigO (F := ℝ) (cocompact ℝ) f fun (x : ℝ) ↦ HPow.hPow (β := ℝ) |x| (-2)
this :
  ∀ (x : ℝ),
    -(↑π : ℂ) / a * HPow.hPow (β := ℕ) ((↑x : ℂ) + I * b) 2 =
      -(↑π : ℂ) / a * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + -2 * (↑π : ℂ) * I * b / a * (↑x : ℂ) +
        (↑π : ℂ) * HPow.hPow (β := ℕ) b 2 / a
⊢ IsBigO (E := ℂ) (F := ℝ) (cocompact ℝ)
    (fun (x : ℝ) ↦
      cexp ((↑π : ℂ) * HPow.hPow (β := ℕ) b 2 / a) *
        (1 / a ^ (1 / 2) * cexp (-(↑π : ℂ) / a * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + -2 * (↑π : ℂ) * I * b / a * (↑x : ℂ))))
    fun (x : ℝ) ↦ HPow.hPow (β := ℝ) |x| (-2)
have refine : (-(↑π : ℂ) / a).re < 0
Tactic: refine ((cexp_neg_quadratic_isLittleO_abs_rpow_cocompact
      (?_) (-2 * ↑π * I * b / a) (-2)).isBigO.const_mul_left _).const_mul_left _
-- 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 : ℂ))
hCf : Continuous f
hFf : 𝓕 f = fun (x : ℝ) ↦ 1 / a ^ (1 / 2) * cexp (-(↑π : ℂ) / a * HPow.hPow (β := ℕ) ((↑x : ℂ) + I * b) 2)
h1 : 0 < ((↑π : ℂ) * a).re
h2 : 0 < ((↑π : ℂ) / a).re
f_bd : IsBigO (F := ℝ) (cocompact ℝ) f fun (x : ℝ) ↦ HPow.hPow (β := ℝ) |x| (-2)
this :
  ∀ (x : ℝ),
    -(↑π : ℂ) / a * HPow.hPow (β := ℕ) ((↑x : ℂ) + I * b) 2 =
      -(↑π : ℂ) / a * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + -2 * (↑π : ℂ) * I * b / a * (↑x : ℂ) +
        (↑π : ℂ) * HPow.hPow (β := ℕ) b 2 / a
⊢ (-(↑π : ℂ) / a).re < 0
have rwa : (-((↑π : ℂ) / a)).re < 0
Tactic: rwa [neg_div, 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 : ℂ))
hCf : Continuous f
hFf : 𝓕 f = fun (x : ℝ) ↦ 1 / a ^ (1 / 2) * cexp (-(↑π : ℂ) / a * HPow.hPow (β := ℕ) ((↑x : ℂ) + I * b) 2)
h1 : 0 < ((↑π : ℂ) * a).re
h2 : 0 < ((↑π : ℂ) / a).re
f_bd : IsBigO (F := ℝ) (cocompact ℝ) f fun (x : ℝ) ↦ HPow.hPow (β := ℝ) |x| (-2)
this :
  ∀ (x : ℝ),
    -(↑π : ℂ) / a * HPow.hPow (β := ℕ) ((↑x : ℂ) + I * b) 2 =
      -(↑π : ℂ) / a * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + -2 * (↑π : ℂ) * I * b / a * (↑x : ℂ) +
        (↑π : ℂ) * HPow.hPow (β := ℕ) b 2 / a
rwa : (-((↑π : ℂ) / a)).re < 0
⊢ (-(↑π : ℂ) / a).re < 0
have rwa₁ : -((↑π : ℂ) / a).re < 0
Tactic: rwa [neg_div, neg_re, neg_lt_zero]
-- 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
hFf : 𝓕 f = fun (x : ℝ) ↦ 1 / a ^ (1 / 2) * cexp (-(↑π : ℂ) / a * HPow.hPow (β := ℕ) ((↑x : ℂ) + I * b) 2)
h1 : 0 < ((↑π : ℂ) * a).re
h2 : 0 < ((↑π : ℂ) / a).re
f_bd : IsBigO (F := ℝ) (cocompact ℝ) f fun (x : ℝ) ↦ HPow.hPow (β := ℝ) |x| (-2)
⊢ ∑' (n : ℤ), cexp (-(↑π : ℂ) * a * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 + 2 * (↑π : ℂ) * b * (↑n : ℂ)) =
    1 / a ^ (1 / 2) * ∑' (n : ℤ), cexp (-(↑π : ℂ) / a * HPow.hPow (β := ℕ) ((↑n : ℂ) + I * b) 2)
have Ff_bd : IsBigO (F := ℝ) (cocompact ℝ) (𝓕 f) fun (x : ℝ) ↦ HPow.hPow (β := ℝ) |x| (-2)
Tactic: have Ff_bd : (𝓕 f) =O[cocompact ℝ] (fun x => |x| ^ (-2 : ℝ)) := by
    rw [hFf]
    have : ∀ (x : ℝ), -↑π / a * (↑x + I * b) ^ 2 =
        -↑π / a * x ^ 2 + (-2 * π * I * b) / a * x + π * b ^ 2 / a := by
      intro x; ring_nf; rw [I_sq]; ring
    simp_rw [this]
    conv => enter [2, x]; rw [Complex.exp_add, ← mul_assoc _ _ (Complex.exp _), mul_comm]
    refine ((cexp_neg_quadratic_isLittleO_abs_rpow_cocompact
      (?_) (-2 * ↑π * I * b / a) (-2)).isBigO.const_mul_left _).const_mul_left _
    rwa [neg_div, 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 : ℂ))
hCf : Continuous f
hFf : 𝓕 f = fun (x : ℝ) ↦ 1 / a ^ (1 / 2) * cexp (-(↑π : ℂ) / a * HPow.hPow (β := ℕ) ((↑x : ℂ) + I * b) 2)
h1 : 0 < ((↑π : ℂ) * a).re
h2 : 0 < ((↑π : ℂ) / a).re
f_bd : IsBigO (F := ℝ) (cocompact ℝ) f fun (x : ℝ) ↦ HPow.hPow (β := ℝ) |x| (-2)
Ff_bd : IsBigO (F := ℝ) (cocompact ℝ) (𝓕 f) fun (x : ℝ) ↦ HPow.hPow (β := ℝ) |x| (-2)
⊢ ∑' (n : ℤ), cexp (-(↑π : ℂ) * a * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 + 2 * (↑π : ℂ) * b * (↑n : ℂ)) =
    1 / a ^ (1 / 2) * ∑' (n : ℤ), cexp (-(↑π : ℂ) / a * HPow.hPow (β := ℕ) ((↑n : ℂ) + I * b) 2)
have h : Eq (α := ℂ) (∑' (n : ℤ), cexp (-(↑π : ℂ) * a * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 + 2 * (↑π : ℂ) * b * (↑n : ℂ)))
  (∑' (n : ℤ), f (HAdd.hAdd (α := ℝ) 0 (↑n : ℝ)))
Tactic: convert! Real.tsum_eq_tsum_fourier_of_rpow_decay hCf one_lt_two f_bd Ff_bd 0 using 1
-- 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 : ℂ))
hCf : Continuous f
hFf : 𝓕 f = fun (x : ℝ) ↦ 1 / a ^ (1 / 2) * cexp (-(↑π : ℂ) / a * HPow.hPow (β := ℕ) ((↑x : ℂ) + I * b) 2)
h1 : 0 < ((↑π : ℂ) * a).re
h2 : 0 < ((↑π : ℂ) / a).re
f_bd : IsBigO (F := ℝ) (cocompact ℝ) f fun (x : ℝ) ↦ HPow.hPow (β := ℝ) |x| (-2)
Ff_bd : IsBigO (F := ℝ) (cocompact ℝ) (𝓕 f) fun (x : ℝ) ↦ HPow.hPow (β := ℝ) |x| (-2)
h :
  Eq (α := ℂ) (∑' (n : ℤ), cexp (-(↑π : ℂ) * a * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 + 2 * (↑π : ℂ) * b * (↑n : ℂ)))
    (∑' (n : ℤ), f (HAdd.hAdd (α := ℝ) 0 (↑n : ℝ)))
⊢ ∑' (n : ℤ), cexp (-(↑π : ℂ) * a * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 + 2 * (↑π : ℂ) * b * (↑n : ℂ)) =
    1 / a ^ (1 / 2) * ∑' (n : ℤ), cexp (-(↑π : ℂ) / a * HPow.hPow (β := ℕ) ((↑n : ℂ) + I * b) 2)
have h₁ : 1 / a ^ (1 / 2) * ∑' (n : ℤ), cexp (-(↑π : ℂ) / a * HPow.hPow (β := ℕ) ((↑n : ℂ) + I * b) 2) =
  ∑' (n : ℤ),
    HMul.hMul (β := ℂ) (𝓕 f (↑n : ℝ)) ((fourier n : (a : AddCircle 1) → ℂ) (↑0 : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
Tactic: convert! Real.tsum_eq_tsum_fourier_of_rpow_decay hCf one_lt_two f_bd Ff_bd 0 using 1