awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation
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 (-x)) fun (x : ℝ) ↦ x ^ s

Tactic:
simpa only [neg_one_mul] using isLittleO_exp_neg_mul_rpow_atTop zero_lt_one s

Premises used: neg_one_mul, isLittleO_exp_neg_mul_rpow_atTop, zero_lt_one
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation
Goal:
a : ℝ
ha : a < 0
b s : ℝ
suffices :
  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

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
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation
Goal:
a : ℝ
ha : a < 0
b s : ℝ
rw : Tendsto (β := ℝ) (fun (x : ℝ) ↦ -x - (a * HPow.hPow (β := ℕ) x 2 + b * x)) atTop atTop
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ rexp (a * HPow.hPow (β := ℕ) x 2 + b * x)) fun (x : ℝ) ↦ rexp (-x)

Tactic:
rw [isLittleO_exp_comp_exp_comp]

Premises used: Real.isLittleO_exp_comp_exp_comp
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation
Goal:
a : ℝ
ha : a < 0
b s : ℝ
h : ∀ (x : ℝ), -x - (a * HPow.hPow (β := ℕ) x 2 + b * x) = x * (-a * x - (b + 1))
⊢ Eq (α := (x : ℝ) → ℝ) (fun (x : ℝ) ↦ -x - (a * HPow.hPow (β := ℕ) x 2 + b * x)) fun (x : ℝ) ↦ x * (-a * x - (b + 1))

Tactic:
ext1 x
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation
Goal:
a : ℝ
ha : a < 0
b s x : ℝ
⊢ -x - (a * HPow.hPow (β := ℕ) x 2 + b * x) = x * (-a * x - (b + 1))

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

Tactic:
have : (fun x ↦ -x - (a * x ^ 2 + b * x)) = fun x ↦ x * (-a * x - (b + 1)) := by
    ext1 x; ring_nf
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation
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))
rw : Tendsto (β := ℝ) (fun (x : ℝ) ↦ x * (-a * x - (b + 1))) atTop atTop
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ -x - (a * HPow.hPow (β := ℕ) x 2 + b * x)) atTop atTop

Tactic:
rw [this]
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation
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 * x - (b + 1))) atTop atTop

Tactic:
tendsto_id.atTop_mul_atTop₀ <| tendsto_atTop_add_const_right _ _ <|
    tendsto_id.const_mul_atTop (neg_pos.mpr ha)

Premises used: Filter.tendsto_atTop_add_const_right, Iff.mpr, Filter.Tendsto.const_mul_atTop, neg_pos, Filter.tendsto_id, Filter.Tendsto.atTop_mul_atTop₀
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation
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 * x - (b + 1))) atTop atTop

Tactic:
exact tendsto_id.atTop_mul_atTop₀ <| tendsto_atTop_add_const_right _ _ <|
    tendsto_id.const_mul_atTop (neg_pos.mpr ha)

Premises used: Filter.tendsto_atTop_add_const_right, Iff.mpr, Filter.Tendsto.const_mul_atTop, neg_pos, Filter.tendsto_id, Filter.Tendsto.atTop_mul_atTop₀
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation
Goal:
a : ℂ
ha : a.re < 0
b : ℂ
s : ℝ
a₁ :
  IsLittleO (E := ℝ) (F := ℝ) atTop (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:
apply Asymptotics.IsLittleO.of_norm_left

Premises used: Asymptotics.IsLittleO.of_norm_left
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation
Goal:
a : ℂ
ha : a.re < 0
b : ℂ
s : ℝ
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ rexp (a.re * HPow.hPow (β := ℕ) x 2 + b.re * x)) fun (x : ℝ) ↦ x ^ s

Tactic:
rexp_neg_quadratic_isLittleO_rpow_atTop ha b.re s

Premises used: Complex.re, rexp_neg_quadratic_isLittleO_rpow_atTop
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation
Goal:
a : ℂ
ha : a.re < 0
b : ℂ
s : ℝ
h :
  ∀ (x : ℝ), ‖cexp (a * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + b * (↑x : ℂ))‖ = rexp (a.re * HPow.hPow (β := ℕ) x 2 + b.re * x)
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ ‖cexp (a * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + b * (↑x : ℂ))‖)
    fun (x : ℝ) ↦ x ^ s

Tactic:
convert! rexp_neg_quadratic_isLittleO_rpow_atTop ha b.re s with x

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

Tactic:
simp_rw [Complex.norm_exp, add_re, ← ofReal_pow, mul_comm (_ : ℂ) ↑(_ : ℝ),
      re_ofReal_mul, mul_comm _ (re _)]

Premises used: Complex.add_re, Complex.ofReal, Complex.re, Complex.norm_exp, mul_comm, Complex.ofReal_pow, Complex.re_ofReal_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation
Goal:
a : ℂ
ha : a.re < 0
b : ℂ
s : ℝ
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
⊢ IsLittleO (E := ℂ) (F := ℝ) (cocompact ℝ) (fun (x : ℝ) ↦ cexp (a * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + b * (↑x : ℂ)))
    fun (x : ℝ) ↦ |x| ^ s

Tactic:
rw [cocompact_eq_atBot_atTop, isLittleO_sup]

Premises used: cocompact_eq_atBot_atTop, Asymptotics.isLittleO_sup
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation
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
right :
  IsLittleO (E := ℂ) (F := ℝ) atTop (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

Tactic:
constructor
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation
Goal:
a : ℂ
ha : a.re < 0
b : ℂ
s x : ℝ
⊢ Eq (α := ℂ) (((fun (x : ℝ) ↦ cexp (a * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + -b * (↑x : ℂ))) ∘ Neg.neg) x)
    ((fun (x : ℝ) ↦ cexp (a * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + b * (↑x : ℂ))) x)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation
Goal:
a : ℂ
ha : a.re < 0
b : ℂ
s : ℝ
left : EventuallyEq (β := ℝ) atBot ((fun (x : ℝ) ↦ x ^ s) ∘ Neg.neg) fun (x : ℝ) ↦ |x| ^ s
⊢ IsLittleO (E := ℂ) (F := ℝ) atBot (fun (x : ℝ) ↦ cexp (a * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + b * (↑x : ℂ)))
    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) ?_

Premises used: Filter.tendsto_neg_atBot_atTop, Filter.Eventually.of_forall, Asymptotics.IsLittleO.congr', cexp_neg_quadratic_isLittleO_rpow_atTop, Asymptotics.IsLittleO.comp_tendsto, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation
Goal:
a : ℂ
ha : a.re < 0
b : ℂ
s : ℝ
⊢ EventuallyEq (β := ℝ) atBot ((fun (x : ℝ) ↦ x ^ s) ∘ Neg.neg) fun (x : ℝ) ↦ |x| ^ s

Tactic:
(eventually_lt_atBot 0).mp (Eventually.of_forall fun x hx ↦ ?_)

Premises used: Filter.EventuallyEq, Filter.Eventually.of_forall, Filter.Eventually.mp, Filter.eventually_lt_atBot, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation
Goal:
a : ℂ
ha : a.re < 0
b : ℂ
s : ℝ
left : ∀ (x : ℝ) (hx : x < 0), Eq (α := ℝ) (((fun (x : ℝ) ↦ x ^ s) ∘ Neg.neg) x) ((fun (x : ℝ) ↦ |x| ^ s) x)
⊢ EventuallyEq (β := ℝ) atBot ((fun (x : ℝ) ↦ x ^ s) ∘ Neg.neg) fun (x : ℝ) ↦ |x| ^ s

Tactic:
refine (eventually_lt_atBot 0).mp (Eventually.of_forall fun x hx ↦ ?_)

Premises used: Filter.Eventually.of_forall, Filter.Eventually.mp, Filter.eventually_lt_atBot, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation
Goal:
a : ℂ
ha : a.re < 0
b : ℂ
s x : ℝ
hx : x < 0
⊢ Eq (α := ℝ) (((fun (x : ℝ) ↦ x ^ s) ∘ Neg.neg) x) ((fun (x : ℝ) ↦ |x| ^ s) x)

Tactic:
simp only [Function.comp_apply, abs_of_neg hx]

Premises used: abs_of_neg, Function.comp_apply
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation
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

Tactic:
(cexp_neg_quadratic_isLittleO_rpow_atTop ha b s).congr' EventuallyEq.rfl ?_

Premises used: Asymptotics.IsLittleO.congr', cexp_neg_quadratic_isLittleO_rpow_atTop, Filter.EventuallyEq.rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation
Goal:
a : ℂ
ha : a.re < 0
b : ℂ
s : ℝ
right : EventuallyEq (β := ℝ) atTop (fun (x : ℝ) ↦ x ^ s) fun (x : ℝ) ↦ |x| ^ s
⊢ IsLittleO (E := ℂ) (F := ℝ) atTop (fun (x : ℝ) ↦ cexp (a * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + b * (↑x : ℂ)))
    fun (x : ℝ) ↦ |x| ^ s

Tactic:
refine (cexp_neg_quadratic_isLittleO_rpow_atTop ha b s).congr' EventuallyEq.rfl ?_

Premises used: Asymptotics.IsLittleO.congr', cexp_neg_quadratic_isLittleO_rpow_atTop, Filter.EventuallyEq.rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation
Goal:
a : ℂ
ha : a.re < 0
b : ℂ
s : ℝ
⊢ EventuallyEq (β := ℝ) atTop (fun (x : ℝ) ↦ x ^ s) fun (x : ℝ) ↦ |x| ^ s

Tactic:
(eventually_gt_atTop 0).mp (Eventually.of_forall fun x hx ↦ ?_)

Premises used: Filter.EventuallyEq, Filter.Eventually.of_forall, Filter.Eventually.mp, OfNat.ofNat, Filter.eventually_gt_atTop
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation
Goal:
a : ℂ
ha : a.re < 0
b : ℂ
s : ℝ
right : ∀ (x : ℝ) (hx : 0 < x), Eq (α := ℝ) ((fun (x : ℝ) ↦ x ^ s) x) ((fun (x : ℝ) ↦ |x| ^ s) x)
⊢ EventuallyEq (β := ℝ) atTop (fun (x : ℝ) ↦ x ^ s) fun (x : ℝ) ↦ |x| ^ s

Tactic:
refine (eventually_gt_atTop 0).mp (Eventually.of_forall fun x hx ↦ ?_)

Premises used: Filter.Eventually.of_forall, Filter.Eventually.mp, OfNat.ofNat, Filter.eventually_gt_atTop
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation
Goal:
a : ℂ
ha : a.re < 0
b : ℂ
s x : ℝ
hx : 0 < x
right right₁ : x ^ s = |x| ^ s
⊢ Eq (α := ℝ) ((fun (x : ℝ) ↦ x ^ s) x) ((fun (x : ℝ) ↦ |x| ^ s) x)

Tactic:
simp_rw [abs_of_pos hx]

Premises used: abs_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation
Goal:
a : ℝ
ha : 0 < a
s x : ℝ
rw : rexp (-a * HPow.hPow (β := ℕ) |x| 2)
| rexp (-a * HPow.hPow (β := ℕ) x 2)

Tactic:
rw [← sq_abs]

Premises used: sq_abs
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation
Goal:
a : ℝ
ha : 0 < a
s : ℝ
conv : Tendsto (β := ℝ) (fun (x : ℝ) ↦ |x| ^ s * rexp (-a * HPow.hPow (β := ℕ) |x| 2)) (cocompact ℝ) (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ |x| ^ s * rexp (-a * HPow.hPow (β := ℕ) x 2)) (cocompact ℝ) (𝓝 0)

Tactic:
conv in rexp _ => rw [← sq_abs]

Premises used: Real.exp, sq_abs
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation
Goal:
a : ℝ
ha : 0 < a
s : ℝ
rw : Tendsto (β := ℝ) (fun (x : ℝ) ↦ |x| ^ s * rexp (-a * HPow.hPow (β := ℕ) |x| 2)) (comap abs atTop) (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ |x| ^ s * rexp (-a * HPow.hPow (β := ℕ) |x| 2)) (cocompact ℝ) (𝓝 0)

Tactic:
rw [cocompact_eq_atBot_atTop, ← comap_abs_atTop]

Premises used: Filter.comap_abs_atTop, cocompact_eq_atBot_atTop
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation
Goal:
a : ℝ
ha : 0 < a
s : ℝ
erw : Tendsto (β := ℝ) (fun (y : ℝ) ↦ y ^ s * rexp (-a * HPow.hPow (β := ℕ) y 2)) atTop (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ |x| ^ s * rexp (-a * HPow.hPow (β := ℕ) |x| 2)) (comap abs 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⟩⟩)]

Premises used: Iff.mpr, Filter.tendsto_comap'_iff, Filter.mem_atTop_sets, Exists.intro, abs_of_nonneg, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation
Goal:
a : ℝ
ha : 0 < a
s : ℝ
⊢ Tendsto (β := ℝ) (fun (y : ℝ) ↦ y ^ s * rexp (-a * HPow.hPow (β := ℕ) y 2)) atTop (𝓝 0)

Tactic:
(rpow_mul_exp_neg_mul_sq_isLittleO_exp_neg ha s).tendsto_zero_of_tendsto
      (tendsto_exp_atBot.comp <| tendsto_id.const_mul_atTop_of_neg (neg_lt_zero.mpr one_half_pos))

Premises used: Iff.mpr, Asymptotics.IsLittleO.tendsto_zero_of_tendsto, Filter.tendsto_id, neg_lt_zero, rpow_mul_exp_neg_mul_sq_isLittleO_exp_neg, Real.tendsto_exp_atBot, one_half_pos, Filter.Tendsto.const_mul_atTop_of_neg, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation
Goal:
a : ℝ
ha : 0 < a
s : ℝ
⊢ Tendsto (β := ℝ) (fun (y : ℝ) ↦ y ^ s * rexp (-a * HPow.hPow (β := ℕ) y 2)) atTop (𝓝 0)

Tactic:
exact
    (rpow_mul_exp_neg_mul_sq_isLittleO_exp_neg ha s).tendsto_zero_of_tendsto
      (tendsto_exp_atBot.comp <| tendsto_id.const_mul_atTop_of_neg (neg_lt_zero.mpr one_half_pos))

Premises used: Iff.mpr, Asymptotics.IsLittleO.tendsto_zero_of_tendsto, Filter.tendsto_id, neg_lt_zero, rpow_mul_exp_neg_mul_sq_isLittleO_exp_neg, Real.tendsto_exp_atBot, one_half_pos, Filter.Tendsto.const_mul_atTop_of_neg, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation
Goal:
a : ℂ
ha : 0 < a.re
s : ℝ
⊢ IsLittleO (E := ℂ) (F := ℝ) (cocompact ℝ) (fun (x : ℝ) ↦ cexp (-a * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + 0 * (↑x : ℂ)))
    fun (x : ℝ) ↦ |x| ^ s

Tactic:
cexp_neg_quadratic_isLittleO_abs_rpow_cocompact (?_ : (-a).re < 0) 0 s

Premises used: cexp_neg_quadratic_isLittleO_abs_rpow_cocompact, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation
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 : ℂ))
convert! : (-a).re < 0
⊢ IsLittleO (E := ℂ) (F := ℝ) (cocompact ℝ) (fun (x : ℝ) ↦ cexp (-a * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) fun (x : ℝ) ↦
    |x| ^ s

Tactic:
convert! cexp_neg_quadratic_isLittleO_abs_rpow_cocompact (?_ : (-a).re < 0) 0 s using 1

Premises used: cexp_neg_quadratic_isLittleO_abs_rpow_cocompact, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation
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)
⊢ Eq (α := ℝ → ℂ) (fun (x : ℝ) ↦ cexp (-a * HPow.hPow (β := ℕ) (↑x : ℂ) 2)) fun (x : ℝ) ↦
    cexp (-a * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + 0 * (↑x : ℂ))

Tactic:
simp_rw [zero_mul, add_zero]

Premises used: MulZeroClass.zero_mul, add_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation
Goal:
a : ℂ
ha : 0 < a.re
s : ℝ
rwa : -a.re < 0
rwa₁ rwa₂ rwa₃ rwa₄ : 0 < a.re
⊢ (-a).re < 0

Tactic:
rwa [neg_re, neg_lt_zero]

Premises used: 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 : ℂ))
⊢ Continuous f

Tactic:
Complex.continuous_exp.comp (Continuous.add ?_ ?_)

Premises used: Continuous.comp, Complex.continuous_exp, Continuous.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 : ℂ))
refine_1 : Continuous (Y := ℂ) fun (x : ℝ) ↦ -(↑π : ℂ) * a * HPow.hPow (β := ℕ) (↑x : ℂ) 2
refine_2 : Continuous (Y := ℂ) fun (x : ℝ) ↦ 2 * (↑π : ℂ) * b * (↑x : ℂ)
⊢ Continuous f

Tactic:
refine Complex.continuous_exp.comp (Continuous.add ?_ ?_)

Premises used: Continuous.comp, Complex.continuous_exp, Continuous.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 : ℂ))
⊢ Continuous (Y := ℂ) fun (x : ℝ) ↦ -(↑π : ℂ) * a * HPow.hPow (β := ℕ) (↑x : ℂ) 2

Tactic:
continuous_const.mul (Complex.continuous_ofReal.pow 2)

Premises used: continuous_const, Continuous.pow, Continuous.mul, Complex.continuous_ofReal, 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 : ℂ))
⊢ Continuous (Y := ℂ) fun (x : ℝ) ↦ -(↑π : ℂ) * a * HPow.hPow (β := ℕ) (↑x : ℂ) 2

Tactic:
exact continuous_const.mul (Complex.continuous_ofReal.pow 2)

Premises used: continuous_const, Continuous.pow, Continuous.mul, Complex.continuous_ofReal, 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 : ℂ))
⊢ Continuous (Y := ℂ) fun (x : ℝ) ↦ 2 * (↑π : ℂ) * b * (↑x : ℂ)

Tactic:
continuous_const.mul Complex.continuous_ofReal

Premises used: continuous_const, Continuous.mul, Complex.continuous_ofReal
-- 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 : ℂ))
⊢ Continuous (Y := ℂ) fun (x : ℝ) ↦ 2 * (↑π : ℂ) * b * (↑x : ℂ)

Tactic:
exact continuous_const.mul Complex.continuous_ofReal

Premises used: continuous_const, Continuous.mul, Complex.continuous_ofReal
-- 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 : ℂ))
⊢ 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
-- 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
⊢ 𝓕 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
-- 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)
rw : 0 < π * a.re
⊢ 0 < ((↑π : ℂ) * a).re

Tactic:
rw [re_ofReal_mul]

Premises used: Complex.re_ofReal_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)
⊢ 0 < π * a.re

Tactic:
mul_pos pi_pos ha

Premises used: Real.pi_pos, mul_pos
-- 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)
⊢ 0 < π * a.re

Tactic:
exact mul_pos pi_pos ha

Premises used: Real.pi_pos, mul_pos
-- 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)
⊢ 0 < ((↑π : ℂ) * a).re

Tactic:
have h1 : 0 < (↑π * a).re := by
    rw [re_ofReal_mul]
    exact mul_pos pi_pos ha
-- 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
rw : 0 < π * HDiv.hDiv (β := ℝ) a.re ((normSq : (a : ℂ) → ℝ) a : ℝ)
⊢ 0 < ((↑π : ℂ) / a).re

Tactic:
rw [div_eq_mul_inv, re_ofReal_mul, inv_re]

Premises used: Complex.inv_re, div_eq_mul_inv, Complex.re_ofReal_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
⊢ 0 < π * HDiv.hDiv (β := ℝ) a.re ((normSq : (a : ℂ) → ℝ) a : ℝ)

Tactic:
mul_pos pi_pos (div_pos ha <| normSq_pos.mpr ?_)

Premises used: Iff.mpr, Complex.normSq_pos, Real.pi_pos, mul_pos, div_pos
-- 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
refine : a ≠ 0
⊢ 0 < π * HDiv.hDiv (β := ℝ) a.re ((normSq : (a : ℂ) → ℝ) a : ℝ)

Tactic:
refine mul_pos pi_pos (div_pos ha <| normSq_pos.mpr ?_)

Premises used: Iff.mpr, Complex.normSq_pos, Real.pi_pos, mul_pos, div_pos
-- 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
contrapose! : ∀ (ha : a = 0), a.re ≤ 0
⊢ a ≠ 0

Tactic:
contrapose! ha
-- Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation
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
rw₁ rw₂ : LE.le (α := ℝ) 0 0
⊢ a.re ≤ 0

Tactic:
rw [ha, zero_re]

Premises used: Complex.zero_re