awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation
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

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]
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation
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 (E := ℂ) (F := ℝ) (cocompact ℝ)
    (fun (x : ℝ) ↦ cexp (-(↑π : ℂ) * a * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + 2 * (↑π : ℂ) * b * (↑x : ℂ))) fun (x : ℝ) ↦
    HPow.hPow (β := ℝ) |x| (-2)

Tactic:
(cexp_neg_quadratic_isLittleO_abs_rpow_cocompact ?_ _ (-2)).isBigO

Premises used: Asymptotics.IsLittleO.isBigO, cexp_neg_quadratic_isLittleO_abs_rpow_cocompact, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation
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
⊢ IsBigO (F := ℝ) (cocompact ℝ) f fun (x : ℝ) ↦ HPow.hPow (β := ℝ) |x| (-2)

Tactic:
convert! (cexp_neg_quadratic_isLittleO_abs_rpow_cocompact ?_ _ (-2)).isBigO

Premises used: Asymptotics.IsLittleO.isBigO, cexp_neg_quadratic_isLittleO_abs_rpow_cocompact, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation
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
convert_2₁ : -((↑π : ℂ) * a).re < 0
convert_2₂ convert_2₃ convert_2₄ convert_2₅ : 0 < ((↑π : ℂ) * a).re
⊢ (-(↑π : ℂ) * a).re < 0

Tactic:
rwa [neg_mul, neg_re, neg_lt_zero]

Premises used: neg_lt_zero, Complex.neg_re, neg_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation
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)

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]
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation
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)
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)
⊢ IsBigO (F := ℝ) (cocompact ℝ) (𝓕 f) fun (x : ℝ) ↦ HPow.hPow (β := ℝ) |x| (-2)

Tactic:
rw [hFf]
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation
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 : ℝ
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
⊢ -(↑π : ℂ) / a * HPow.hPow (β := ℕ) ((↑x : ℂ) + I * b) 2 =
    -(↑π : ℂ) / a * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + -2 * (↑π : ℂ) * I * b / a * (↑x : ℂ) +
      (↑π : ℂ) * HPow.hPow (β := ℕ) b 2 / a

Tactic:
ring_nf
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation
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 : ℝ
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
⊢ -((↑π : ℂ) * 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:
rw [I_sq]

Premises used: Complex.I_sq
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation
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⁻¹ * -1 * HPow.hPow (β := ℕ) b 2 =
    -((↑π : ℂ) * a⁻¹ * (↑x : ℂ) * I * b * 2) - (↑π : ℂ) * a⁻¹ * HPow.hPow (β := ℕ) (↑x : ℂ) 2 +
      (↑π : ℂ) * a⁻¹ * HPow.hPow (β := ℕ) b 2

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation
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

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
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation
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
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)
⊢ 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:
simp_rw [this]
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation
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
h :
  ∀ (x : ℝ),
    1 / a ^ (1 / 2) *
      cexp
        (-(↑π : ℂ) / 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)

Tactic:
enter [2, x]
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation
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 : ℝ
h :
  cexp ((↑π : ℂ) * HPow.hPow (β := ℕ) b 2 / a) *
    (1 / a ^ (1 / 2) * cexp (-(↑π : ℂ) / a * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + -2 * (↑π : ℂ) * I * b / a * (↑x : ℂ)))
| 1 / a ^ (1 / 2) *
    cexp
      (-(↑π : ℂ) / a * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + -2 * (↑π : ℂ) * I * b / a * (↑x : ℂ) +
        (↑π : ℂ) * HPow.hPow (β := ℕ) b 2 / a)

Tactic:
rw [Complex.exp_add, ← mul_assoc _ _ (Complex.exp _), mul_comm]

Premises used: Complex.exp_add, mul_assoc, mul_comm, Complex.exp
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation
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
h :
  ∀ (x : ℝ),
    cexp ((↑π : ℂ) * HPow.hPow (β := ℕ) b 2 / a) *
      (1 / a ^ (1 / 2) * cexp (-(↑π : ℂ) / a * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + -2 * (↑π : ℂ) * I * b / a * (↑x : ℂ)))
| 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:
enter [2, x]; rw [Complex.exp_add, ← mul_assoc _ _ (Complex.exp _), mul_comm]

Premises used: Complex.exp_add, mul_assoc, mul_comm, Complex.exp
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation
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
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)
⊢ 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:
conv => enter [2, x]; rw [Complex.exp_add, ← mul_assoc _ _ (Complex.exp _), mul_comm]

Premises used: Complex.exp_add, mul_assoc, mul_comm, Complex.exp
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation
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)

Tactic:
((cexp_neg_quadratic_isLittleO_abs_rpow_cocompact
      (?_) (-2 * ↑π * I * b / a) (-2)).isBigO.const_mul_left _).const_mul_left _

Premises used: Asymptotics.IsBigO.const_mul_left, HMul.hMul, HDiv.hDiv, Asymptotics.IsLittleO.isBigO, cexp_neg_quadratic_isLittleO_abs_rpow_cocompact, OfNat.ofNat, Neg.neg, Complex.I
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation
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
refine : (-(↑π : ℂ) / a).re < 0
⊢ 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:
refine ((cexp_neg_quadratic_isLittleO_abs_rpow_cocompact
      (?_) (-2 * ↑π * I * b / a) (-2)).isBigO.const_mul_left _).const_mul_left _

Premises used: Asymptotics.IsBigO.const_mul_left, HMul.hMul, HDiv.hDiv, Asymptotics.IsLittleO.isBigO, cexp_neg_quadratic_isLittleO_abs_rpow_cocompact, OfNat.ofNat, Neg.neg, Complex.I
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation
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
rwa₁ : -((↑π : ℂ) / a).re < 0
rwa₂ rwa₃ rwa₄ rwa₅ : 0 < ((↑π : ℂ) / a).re
⊢ (-(↑π : ℂ) / a).re < 0

Tactic:
rwa [neg_div, neg_re, neg_lt_zero]

Premises used: neg_div, neg_lt_zero, Complex.neg_re
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation
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)

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]
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation
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)
⊢ Eq (α := ℂ) (∑' (n : ℤ), f (HAdd.hAdd (α := ℝ) 0 (↑n : ℝ)))
    (∑' (n : ℤ),
      HMul.hMul (β := ℂ) (𝓕 f (↑n : ℝ)) ((fourier n : (a : AddCircle 1) → ℂ) (↑0 : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))

Tactic:
Real.tsum_eq_tsum_fourier_of_rpow_decay hCf one_lt_two f_bd Ff_bd 0

Premises used: Real.tsum_eq_tsum_fourier_of_rpow_decay, one_lt_two, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation
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 : ℝ)))
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) : ℂ)
⊢ ∑' (n : ℤ), cexp (-(↑π : ℂ) * a * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 + 2 * (↑π : ℂ) * b * (↑n : ℂ)) =
    1 / a ^ (1 / 2) * ∑' (n : ℤ), cexp (-(↑π : ℂ) / a * HPow.hPow (β := ℕ) ((↑n : ℂ) + I * b) 2)

Tactic:
convert! Real.tsum_eq_tsum_fourier_of_rpow_decay hCf one_lt_two f_bd Ff_bd 0 using 1

Premises used: Real.tsum_eq_tsum_fourier_of_rpow_decay, one_lt_two, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation
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)
⊢ Eq (α := ℂ) (∑' (n : ℤ), cexp (-(↑π : ℂ) * a * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 + 2 * (↑π : ℂ) * b * (↑n : ℂ)))
    (∑' (n : ℤ), f (HAdd.hAdd (α := ℝ) 0 (↑n : ℝ)))

Tactic:
simp only [f, zero_add, ofReal_intCast]

Premises used: Complex.ofReal_intCast, zero_add
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation
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 (α := ℂ) (∑' (x : ℤ), 1 / a ^ (1 / 2) * cexp (-(↑π : ℂ) / a * HPow.hPow (β := ℕ) ((↑x : ℂ) + I * b) 2))
    (∑' (n : ℤ),
      HMul.hMul (β := ℂ) (𝓕 f (↑n : ℝ)) ((fourier n : (a : AddCircle 1) → ℂ) (↑0 : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
⊢ 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:
rw [← tsum_mul_left]

Premises used: tsum_mul_left
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation
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)
⊢ Eq (α := ℂ) (∑' (x : ℤ), 1 / a ^ (1 / 2) * cexp (-(↑π : ℂ) / a * HPow.hPow (β := ℕ) ((↑x : ℂ) + I * b) 2))
    (∑' (n : ℤ),
      HMul.hMul (β := ℂ) (𝓕 f (↑n : ℝ)) ((fourier n : (a : AddCircle 1) → ℂ) (↑0 : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))

Tactic:
simp only [QuotientAddGroup.mk_zero, fourier_eval_zero, mul_one, hFf, ofReal_intCast]

Premises used: Complex.ofReal_intCast, fourier_eval_zero, QuotientAddGroup.mk_zero, mul_one