awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ModularForms.Identities
Goal:
f : ℍ → ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
s : Set (GL (Fin 2) ℝ)
hΓ : Γ = Subgroup.closure s
k : ℤ
h : ∀ γ ∈ s, @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ f = f
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
mpr :
  ∀ (x y : GL (Fin 2) ℝ) (hx : Membership.mem (γ := Subgroup (GL (Fin 2) ℝ)) (Subgroup.closure s) x)
    (hy : Membership.mem (γ := Subgroup (GL (Fin 2) ℝ)) (Subgroup.closure s) y),
    @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k x f = f →
      @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k y f = f →
        @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k (x * y) f = f
mpr₁ :
  ∀ (x : GL (Fin 2) ℝ) (hx : Membership.mem (γ := Subgroup (GL (Fin 2) ℝ)) (Subgroup.closure s) x),
    @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k x f = f →
      @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k x⁻¹ f = f
mpr₂ : Membership.mem (γ := Subgroup (GL (Fin 2) ℝ)) (Subgroup.closure s) γ
⊢ @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ f = f

Tactic:
apply Subgroup.closure_induction (p := fun γ _ ↦ f ∣[k] γ = f) h (by simp)

Premises used: Subgroup.closure_induction
-- Module: Mathlib.NumberTheory.ModularForms.Identities
Goal:
f : ℍ → ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
s : Set (GL (Fin 2) ℝ)
hΓ : Γ = Subgroup.closure s
k : ℤ
h : ∀ γ ∈ s, @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ f = f
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
⊢ ∀ (x y : GL (Fin 2) ℝ) (hx : Membership.mem (γ := Subgroup (GL (Fin 2) ℝ)) (Subgroup.closure s) x)
    (hy : Membership.mem (γ := Subgroup (GL (Fin 2) ℝ)) (Subgroup.closure s) y),
    @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k x f = f →
      @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k y f = f →
        @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k (x * y) f = f

Tactic:
simp +contextual [SlashAction.slash_mul]

Premises used: SlashAction.slash_mul
-- Module: Mathlib.NumberTheory.ModularForms.Identities
Goal:
f : ℍ → ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
s : Set (GL (Fin 2) ℝ)
hΓ : Γ = Subgroup.closure s
k : ℤ
h : ∀ γ ∈ s, @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ f = f
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
x : GL (Fin 2) ℝ
hx : Membership.mem (γ := Subgroup (GL (Fin 2) ℝ)) (Subgroup.closure s) x
hf : @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k x f = f
mpr :
  @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k (x * x⁻¹) f =
    @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k x f
⊢ @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k x⁻¹ f = f

Tactic:
rw [← hf, ← SlashAction.slash_mul]

Premises used: SlashAction.slash_mul
-- Module: Mathlib.NumberTheory.ModularForms.Identities
Goal:
f : ℍ → ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
s : Set (GL (Fin 2) ℝ)
hΓ : Γ = Subgroup.closure s
k : ℤ
h : ∀ γ ∈ s, @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ f = f
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
x : GL (Fin 2) ℝ
hx : Membership.mem (γ := Subgroup (GL (Fin 2) ℝ)) (Subgroup.closure s) x
hf : @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k x f = f
⊢ @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k (x * x⁻¹) f =
    @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k x f

Tactic:
simp [hf]
-- Module: Mathlib.NumberTheory.ModularForms.Identities
Goal:
f : ℍ → ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
s : Set (GL (Fin 2) ℝ)
hΓ : Γ = Subgroup.closure s
k : ℤ
h : ∀ γ ∈ s, @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ f = f
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
⊢ Membership.mem (γ := Subgroup (GL (Fin 2) ℝ)) (Subgroup.closure s) γ

Tactic:
simpa [← hΓ]
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
c d : ℝ
hcd : c ≤ d
hfg : ∀ᶠ (x : ℝ) in atTop, ‖rexp (-d * x)‖ ≤ rexp (-c * x)
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ rexp (-d * t)) fun (t : ℝ) ↦ rexp (-c * t)

Tactic:
apply Eventually.isBigO

Premises used: Filter.Eventually.isBigO
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
c d : ℝ
hcd : c ≤ d
h : ∀ (t : ℝ) (ht : 0 < t), ‖rexp (-d * t)‖ ≤ rexp (-c * t)
⊢ ∀ᶠ (x : ℝ) in atTop, ‖rexp (-d * x)‖ ≤ rexp (-c * x)

Tactic:
filter_upwards [eventually_gt_atTop 0] with t ht

Premises used: OfNat.ofNat, Filter.eventually_gt_atTop
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
c d : ℝ
hcd : c ≤ d
t : ℝ
ht : 0 < t
h : rexp (-d * t) ≤ rexp (-c * t)
⊢ ‖rexp (-d * t)‖ ≤ rexp (-c * t)

Tactic:
rw [norm_of_nonneg (exp_pos _).le]

Premises used: LT.lt.le, Real.norm_of_nonneg, Real.exp_pos
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
c d : ℝ
hcd : c ≤ d
t : ℝ
ht : 0 < t
h : 0 ≤ t
⊢ rexp (-d * t) ≤ rexp (-c * t)

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
t : ℝ
ht : 0 < t
⊢ rexp (-π * t) < 1

Tactic:
simpa only [exp_lt_one_iff, neg_mul, neg_lt_zero] using mul_pos pi_pos ht

Premises used: Real.pi_pos, neg_lt_zero, mul_pos, Real.exp_lt_one_iff, neg_mul
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
⊢ HSub.hSub (α := ℝ) 1 0 ≠ 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
refine : Tendsto (β := ℝ) (fun (x : ℝ) ↦ rexp (-π * x)) atTop (𝓝 0)
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ (1 - rexp (-π * t))⁻¹) fun (x : ℝ) ↦ 1

Tactic:
refine ((Tendsto.const_sub _ ?_).inv₀ (by simp)).isBigO_one ℝ (c := ((1 - 0)⁻¹ : ℝ))

Premises used: Filter.Tendsto.isBigO_one, Real, Filter.Tendsto.const_sub, Filter.Tendsto.inv₀
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ rexp (-π * x)) atTop (𝓝 0)

Tactic:
simpa only [neg_mul, tendsto_exp_comp_nhds_zero, tendsto_neg_atBot_iff]
    using tendsto_id.const_mul_atTop pi_pos

Premises used: Filter.Tendsto.const_mul_atTop, Filter.tendsto_id, Real.tendsto_exp_comp_nhds_zero, Real.pi_pos, Filter.tendsto_neg_atBot_iff, neg_mul
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
k : ℕ
a t : ℝ
ha : 0 ≤ a
ht : 0 < t
n : ℕ
⊢ 0 ≤ ((↑n : ℝ) + a) ^ k * rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t)

Tactic:
positivity
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
k : ℕ
a t : ℝ
ha : 0 ≤ a
ht : 0 < t
n : ℕ
rw :
  ((↑n : ℝ) + a) ^ k * rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t) ≤
    ((↑n : ℝ) + a) ^ k * rexp (-π * ((↑n : ℝ) + HPow.hPow (β := ℕ) a 2) * t)
⊢ ‖f_nat k a t n‖ ≤ g_nat k a t n

Tactic:
rw [f_nat, norm_of_nonneg (by positivity), g_nat]

Premises used: HurwitzKernelBounds.f_nat, HurwitzKernelBounds.g_nat, Real.norm_of_nonneg
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
k : ℕ
a t : ℝ
ha : 0 ≤ a
ht : 0 < t
n : ℕ
simp :
  ((↑n : ℝ) + a) ^ k *
      rexp
        (-(π * (HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 + HMul.hMul (α := ℝ) 2 (↑n : ℝ) * a + HPow.hPow (β := ℕ) a 2) *
            t)) ≤
    ((↑n : ℝ) + a) ^ k * rexp (-(π * ((↑n : ℝ) + HPow.hPow (β := ℕ) a 2) * t))
⊢ ((↑n : ℝ) + a) ^ k * rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t) ≤
    ((↑n : ℝ) + a) ^ k * rexp (-π * ((↑n : ℝ) + HPow.hPow (β := ℕ) a 2) * t)

Tactic:
simp only [neg_mul, add_sq]

Premises used: add_sq, neg_mul
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
k : ℕ
a t : ℝ
ha : 0 ≤ a
ht : 0 < t
n : ℕ
hbc : (↑n : ℝ) ≤ HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 + HMul.hMul (α := ℝ) 2 (↑n : ℝ) * a
⊢ ((↑n : ℝ) + a) ^ k *
      rexp
        (-(π * (HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 + HMul.hMul (α := ℝ) 2 (↑n : ℝ) * a + HPow.hPow (β := ℕ) a 2) *
            t)) ≤
    ((↑n : ℝ) + a) ^ k * rexp (-(π * ((↑n : ℝ) + HPow.hPow (β := ℕ) a 2) * t))

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
k : ℕ
a t : ℝ
ha : 0 ≤ a
ht : 0 < t
n : ℕ
⊢ (↑n : ℝ) ≤ HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2

Tactic:
have H₁ : (n : ℝ) ≤ n ^ 2 := mod_cast Nat.le_self_pow two_ne_zero n
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
k : ℕ
a t : ℝ
ha : 0 ≤ a
ht : 0 < t
n : ℕ
H₁ : (↑n : ℝ) ≤ HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2
⊢ 0 ≤ HMul.hMul (α := ℝ) 2 (↑n : ℝ) * a

Tactic:
positivity
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
k : ℕ
a t : ℝ
ha : 0 ≤ a
ht : 0 < t
n : ℕ
H₁ : (↑n : ℝ) ≤ HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2
⊢ 0 ≤ HMul.hMul (α := ℝ) 2 (↑n : ℝ) * a

Tactic:
have H₂ : 0 ≤ 2 * n * a := by positivity
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
k : ℕ
a t : ℝ
ha : 0 ≤ a
ht : 0 < t
n : ℕ
H₁ : (↑n : ℝ) ≤ HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2
H₂ : 0 ≤ HMul.hMul (α := ℝ) 2 (↑n : ℝ) * a
⊢ (↑n : ℝ) ≤ HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 + HMul.hMul (α := ℝ) 2 (↑n : ℝ) * a

Tactic:
linear_combination H₁ + H₂
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
k : ℕ
a t : ℝ
ht : 0 < t
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) k * rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t)

Tactic:
(((summable_pow_mul_jacobiTheta₂_term_bound (|a| * t) ht k).mul_right
      (rexp (-π * a ^ 2 * t))).comp_injective Nat.cast_injective).of_norm_bounded (fun n ↦ ?_)

Premises used: Real.pi, HMul.hMul, abs, Summable.mul_right, Real.exp, HPow.hPow, Summable.comp_injective, Summable.of_norm_bounded, summable_pow_mul_jacobiTheta₂_term_bound, Nat.cast_injective, OfNat.ofNat, Neg.neg
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
k : ℕ
a t : ℝ
ht : 0 < t
refine :
  ∀ (n : ℕ),
    ‖HPow.hPow (α := ℝ) (↑n : ℝ) k * rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t)‖ ≤
      ((fun (i : ℤ) ↦
            HPow.hPow (α := ℝ) (↑|i| : ℝ) k *
                rexp (-π * (t * HPow.hPow (α := ℝ) (β := ℕ) (↑i : ℝ) 2 - 2 * (|a| * t) * (↑|i| : ℝ))) *
              rexp (-π * HPow.hPow (β := ℕ) a 2 * t)) ∘
          Nat.cast)
        n
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) k * rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t)

Tactic:
refine (((summable_pow_mul_jacobiTheta₂_term_bound (|a| * t) ht k).mul_right
      (rexp (-π * a ^ 2 * t))).comp_injective Nat.cast_injective).of_norm_bounded (fun n ↦ ?_)

Premises used: Real.pi, HMul.hMul, abs, Summable.mul_right, Real.exp, HPow.hPow, Summable.comp_injective, Summable.of_norm_bounded, summable_pow_mul_jacobiTheta₂_term_bound, Nat.cast_injective, OfNat.ofNat, Neg.neg
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
k : ℕ
a t : ℝ
ht : 0 < t
n : ℕ
simp_rw :
  HPow.hPow (α := ℝ) (↑n : ℝ) k * rexp (-π * (HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t)) ≤
    HPow.hPow (α := ℝ) (↑n : ℝ) k *
      rexp
        (-π * (t * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * (|a| * (t * (↑n : ℝ)))) +
          -π * (HPow.hPow (β := ℕ) a 2 * t))
⊢ ‖HPow.hPow (α := ℝ) (↑n : ℝ) k * rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t)‖ ≤
    ((fun (i : ℤ) ↦
          HPow.hPow (α := ℝ) (↑|i| : ℝ) k *
              rexp (-π * (t * HPow.hPow (α := ℝ) (β := ℕ) (↑i : ℝ) 2 - 2 * (|a| * t) * (↑|i| : ℝ))) *
            rexp (-π * HPow.hPow (β := ℕ) a 2 * t)) ∘
        Nat.cast)
      n

Tactic:
simp_rw [mul_assoc, Function.comp_apply, ← Real.exp_add, norm_mul, norm_pow, Int.cast_abs,
      Int.cast_natCast, norm_eq_abs, Nat.abs_cast, abs_exp]

Premises used: Int.cast_natCast, Int.cast_abs, norm_pow, Nat.abs_cast, mul_assoc, norm_mul, Function.comp_apply, Real.exp_add, Real.norm_eq_abs, Real.abs_exp
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
k : ℕ
a t : ℝ
ht : 0 < t
n : ℕ
hbc :
  -π * (HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t) ≤
    -π * (t * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * (|a| * (t * (↑n : ℝ)))) + -π * (HPow.hPow (β := ℕ) a 2 * t)
⊢ HPow.hPow (α := ℝ) (↑n : ℝ) k * rexp (-π * (HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t)) ≤
    HPow.hPow (α := ℝ) (↑n : ℝ) k *
      rexp
        (-π * (t * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * (|a| * (t * (↑n : ℝ)))) +
          -π * (HPow.hPow (β := ℕ) a 2 * t))

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
k : ℕ
a t : ℝ
ht : 0 < t
n : ℕ
hbc :
  0 ≤
    -π * (t * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * (|a| * (t * (↑n : ℝ)))) + -π * (HPow.hPow (β := ℕ) a 2 * t) -
      -π * (HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t)
⊢ -π * (HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t) ≤
    -π * (t * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * (|a| * (t * (↑n : ℝ)))) + -π * (HPow.hPow (β := ℕ) a 2 * t)

Tactic:
rw [← sub_nonneg]

Premises used: sub_nonneg
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
k : ℕ
a t : ℝ
ht : 0 < t
n : ℕ
⊢ -π * (t * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * (|a| * (t * (↑n : ℝ)))) + -π * (HPow.hPow (β := ℕ) a 2 * t) -
      -π * (HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t) =
    π * t * (↑n : ℝ) * (|a| + a) * 2

Tactic:
ring
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
k : ℕ
a t : ℝ
ht : 0 < t
n : ℕ
hbc : 0 ≤ π * t * (↑n : ℝ) * (|a| + a) * 2
⊢ 0 ≤
    -π * (t * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * (|a| * (t * (↑n : ℝ)))) + -π * (HPow.hPow (β := ℕ) a 2 * t) -
      -π * (HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t)

Tactic:
rw [show -π * (t * n ^ 2 - 2 * (|a| * (t * n))) + -π * (a ^ 2 * t) - -π * ((n + a) ^ 2 * t)
         = π * t * n * (|a| + a) * 2 by ring]
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
k : ℕ
a t : ℝ
ht : 0 < t
n : ℕ
⊢ 0 ≤ π * t * (↑n : ℝ)

Tactic:
positivity
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
k : ℕ
a t : ℝ
ht : 0 < t
n : ℕ
hbc : 0 ≤ |a| + a
⊢ 0 ≤ π * t * (↑n : ℝ) * (|a| + a) * 2

Tactic:
refine mul_nonneg (mul_nonneg (by positivity) ?_) two_pos.le

Premises used: mul_nonneg
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
k : ℕ
a t : ℝ
ht : 0 < t
n : ℕ
hbc : -a ≤ |a|
⊢ 0 ≤ |a| + a

Tactic:
rw [← neg_le_iff_add_nonneg]

Premises used: neg_le_iff_add_nonneg
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
k : ℕ
a t : ℝ
ht : 0 < t
n : ℕ
⊢ -a ≤ |a|

Tactic:
apply neg_le_abs

Premises used: neg_le_abs
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
k : ℕ
a t : ℝ
ht : 0 < t
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) k * rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t)

Tactic:
have : Summable fun n : ℕ ↦ n ^ k * exp (-π * (n + a) ^ 2 * t) := by
    refine (((summable_pow_mul_jacobiTheta₂_term_bound (|a| * t) ht k).mul_right
      (rexp (-π * a ^ 2 * t))).comp_injective Nat.cast_injective).of_norm_bounded (fun n ↦ ?_)
    simp_rw [mul_assoc, Function.comp_apply, ← Real.exp_add, norm_mul, norm_pow, Int.cast_abs,
      Int.cast_natCast, norm_eq_abs, Nat.abs_cast, abs_exp]
    gcongr
    rw [← sub_nonneg]
    rw [show -π * (t * n ^ 2 - 2 * (|a| * (t * n))) + -π * (a ^ 2 * t) - -π * ((n + a) ^ 2 * t)
         = π * t * n * (|a| + a) * 2 by ring]
    refine mul_nonneg (mul_nonneg (by positivity) ?_) two_pos.le
    rw [← neg_le_iff_add_nonneg]
    apply neg_le_abs
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
k : ℕ
a t : ℝ
ht : 0 < t
this :
  Summable (α := ℝ) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) k * rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t)
apply :
  ∀ᶠ (i : ℕ) in atTop,
    ‖f_nat k a t i‖ ≤
      HPow.hPow (α := ℝ) 2 k * (HPow.hPow (α := ℝ) (↑i : ℝ) k * rexp (-π * HPow.hPow (β := ℕ) ((↑i : ℝ) + a) 2 * t))
⊢ Summable (f_nat k a t)

Tactic:
apply (this.mul_left (2 ^ k)).of_norm_bounded_eventually_nat

Premises used: Summable.mul_left, HPow.hPow, OfNat.ofNat, Summable.of_norm_bounded_eventually_nat
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
k : ℕ
a t : ℝ
ht : 0 < t
this :
  Summable (α := ℝ) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) k * rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t)
simp_rw : ∀ᶠ (i : ℕ) in atTop, |(↑i : ℝ) + a| ^ k ≤ HAdd.hAdd (α := ℝ) (↑i : ℝ) (↑i : ℝ) ^ k
⊢ ∀ᶠ (i : ℕ) in atTop,
    ‖f_nat k a t i‖ ≤
      HPow.hPow (α := ℝ) 2 k * (HPow.hPow (α := ℝ) (↑i : ℝ) k * rexp (-π * HPow.hPow (β := ℕ) ((↑i : ℝ) + a) 2 * t))

Tactic:
simp_rw [← mul_assoc, f_nat, norm_mul, norm_eq_abs, abs_exp,
    mul_le_mul_iff_of_pos_right (exp_pos _), ← mul_pow, abs_pow, two_mul]

Premises used: mul_le_mul_iff_of_pos_right, mul_assoc, two_mul, norm_mul, HurwitzKernelBounds.f_nat, mul_pow, Real.norm_eq_abs, abs_pow, Real.exp_pos, Real.abs_exp
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
k : ℕ
a t : ℝ
ht : 0 < t
this :
  Summable (α := ℝ) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) k * rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t)
h : ∀ (n : ℕ) (hn : ⌈|a|⌉₊ ≤ n), |(↑n : ℝ) + a| ^ k ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) (↑n : ℝ) ^ k
⊢ ∀ᶠ (i : ℕ) in atTop, |(↑i : ℝ) + a| ^ k ≤ HAdd.hAdd (α := ℝ) (↑i : ℝ) (↑i : ℝ) ^ k

Tactic:
filter_upwards [eventually_ge_atTop (Nat.ceil |a|)] with n hn

Premises used: abs, Nat.ceil, Filter.eventually_ge_atTop
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
k : ℕ
a t : ℝ
ht : 0 < t
this :
  Summable (α := ℝ) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) k * rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t)
n : ℕ
hn : ⌈|a|⌉₊ ≤ n
h : |(↑n : ℝ) + a| ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) (↑n : ℝ)
⊢ |(↑n : ℝ) + a| ^ k ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) (↑n : ℝ) ^ k

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
k : ℕ
a t : ℝ
ht : 0 < t
this :
  Summable (α := ℝ) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) k * rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t)
n : ℕ
hn : ⌈|a|⌉₊ ≤ n
⊢ |(↑n : ℝ) + a| ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) (↑n : ℝ)

Tactic:
(abs_add_le ..).trans (add_le_add (Nat.abs_cast _).le (Nat.ceil_le.mp hn))

Premises used: Nat.abs_cast, add_le_add, Eq.le, Iff.mp, LE.le.trans, abs_add_le, Nat.ceil_le
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
k : ℕ
a t : ℝ
ht : 0 < t
this :
  Summable (α := ℝ) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) k * rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t)
n : ℕ
hn : ⌈|a|⌉₊ ≤ n
⊢ |(↑n : ℝ) + a| ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) (↑n : ℝ)

Tactic:
exact (abs_add_le ..).trans (add_le_add (Nat.abs_cast _).le (Nat.ceil_le.mp hn))

Premises used: add_le_add, Iff.mp, LE.le.trans, abs_add_le, Nat.ceil_le
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
⊢ ‖F_nat 0 a t‖ ≤ rexp (-π * HPow.hPow (β := ℕ) a 2 * t) / (1 - rexp (-π * t))

Tactic:
tsum_of_norm_bounded ?_ (f_le_g_nat 0 ha ht)

Premises used: HurwitzKernelBounds.f_le_g_nat, OfNat.ofNat, tsum_of_norm_bounded, HurwitzKernelBounds.F_nat
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
refine : HasSum (g_nat 0 a t) (rexp (-π * HPow.hPow (β := ℕ) a 2 * t) / (1 - rexp (-π * t)))
⊢ ‖F_nat 0 a t‖ ≤ rexp (-π * HPow.hPow (β := ℕ) a 2 * t) / (1 - rexp (-π * t))

Tactic:
refine tsum_of_norm_bounded ?_ (f_le_g_nat 0 ha ht)

Premises used: HurwitzKernelBounds.f_le_g_nat, OfNat.ofNat, tsum_of_norm_bounded
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
⊢ HasSum (fun (i : ℕ) ↦ rexp (-π * HPow.hPow (β := ℕ) a 2 * t) * rexp (-π * t) ^ i)
    (rexp (-π * HPow.hPow (β := ℕ) a 2 * t) * (1 - rexp (-π * t))⁻¹)

Tactic:
(hasSum_geometric_of_lt_one (exp_pos _).le <| exp_lt_aux ht).mul_left _

Premises used: _private.0.HurwitzKernelBounds.exp_lt_aux, LT.lt.le, HasSum.mul_left, hasSum_geometric_of_lt_one, Real.exp_pos
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
h : g_nat 0 a t = fun (i : ℕ) ↦ rexp (-π * HPow.hPow (β := ℕ) a 2 * t) * rexp (-π * t) ^ i
⊢ HasSum (g_nat 0 a t) (rexp (-π * HPow.hPow (β := ℕ) a 2 * t) / (1 - rexp (-π * t)))

Tactic:
convert! (hasSum_geometric_of_lt_one (exp_pos _).le <| exp_lt_aux ht).mul_left _ using 1

Premises used: _private.0.HurwitzKernelBounds.exp_lt_aux, LT.lt.le, HasSum.mul_left, hasSum_geometric_of_lt_one, Real.exp_pos
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
h : ∀ (n : ℕ), g_nat 0 a t n = rexp (-π * HPow.hPow (β := ℕ) a 2 * t) * rexp (-π * t) ^ n
⊢ g_nat 0 a t = fun (i : ℕ) ↦ rexp (-π * HPow.hPow (β := ℕ) a 2 * t) * rexp (-π * t) ^ i

Tactic:
ext1 n
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
n : ℕ
h :
  HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 0 * rexp (-π * ((↑n : ℝ) + HPow.hPow (β := ℕ) a 2) * t) =
    rexp (-π * HPow.hPow (β := ℕ) a 2 * t + (↑n : ℝ) * (-π * t))
⊢ HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 0 * rexp (-π * ((↑n : ℝ) + HPow.hPow (β := ℕ) a 2) * t) =
    rexp (-π * HPow.hPow (β := ℕ) a 2 * t) * rexp (-π * t) ^ n

Tactic:
rw [← Real.exp_nat_mul, ← Real.exp_add]

Premises used: Real.exp_nat_mul, Real.exp_add
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
n : ℕ
⊢ HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 0 * rexp (-π * ((↑n : ℝ) + HPow.hPow (β := ℕ) a 2) * t) =
    rexp (-π * HPow.hPow (β := ℕ) a 2 * t + (↑n : ℝ) * (-π * t))

Tactic:
ring_nf
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
t : ℝ
ht : 0 < t
⊢ ‖F_nat 0 1 t‖ ≤ rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) 1 2 * t) / (1 - rexp (-π * t))

Tactic:
F_nat_zero_le zero_le_one ht

Premises used: zero_le_one, HurwitzKernelBounds.F_nat_zero_le
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
t : ℝ
ht : 0 < t
h : F_nat 0 0 t - 1 = F_nat 0 1 t
h₁ : rexp (-π * t) = rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) 1 2 * t)
⊢ ‖F_nat 0 0 t - 1‖ ≤ rexp (-π * t) / (1 - rexp (-π * t))

Tactic:
convert! F_nat_zero_le zero_le_one ht using 2

Premises used: zero_le_one, HurwitzKernelBounds.F_nat_zero_le
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
t : ℝ
ht : 0 < t
h : ∑' (b : ℕ), f_nat 0 0 t (b + 1) = F_nat 0 1 t
⊢ F_nat 0 0 t - 1 = F_nat 0 1 t

Tactic:
rw [F_nat, (summable_f_nat 0 0 ht).tsum_eq_zero_add, f_nat, Nat.cast_zero, add_zero, pow_zero,
      one_mul, pow_two, mul_zero, mul_zero, zero_mul, exp_zero, add_comm, add_sub_cancel_right]

Premises used: pow_two, MulZeroClass.zero_mul, Summable.tsum_eq_zero_add, add_comm, pow_zero, MulZeroClass.mul_zero, HurwitzKernelBounds.summable_f_nat, HurwitzKernelBounds.f_nat, Real.exp_zero, Nat.cast_zero, add_sub_cancel_right, add_zero, OfNat.ofNat, HurwitzKernelBounds.F_nat, one_mul
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
t : ℝ
ht : 0 < t
h : Eq (α := ℝ) (∑' (b : ℕ), f_nat 0 0 t (b + 1)) (∑' (n : ℕ), f_nat 0 1 t n)
h₁ :
  Eq (α := ℝ)
    (∑' (b : ℕ),
      HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℝ) (↑(b + 1) : ℝ) 0) 0 *
        rexp (-π * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℝ) (↑(b + 1) : ℝ) 0) 2 * t))
    (∑' (n : ℕ),
      HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) 0 *
        rexp (-π * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) 2 * t))
h₂ :
  Eq (α := ℝ)
    (∑' (b : ℕ),
      HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℝ) (↑b : ℝ) (↑1 : ℝ) + 0) 0 *
        rexp (-π * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℝ) (↑b : ℝ) (↑1 : ℝ) + 0) 2 * t))
    (∑' (n : ℕ),
      HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) 0 *
        rexp (-π * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) 2 * t))
h₃ :
  Eq (α := ℝ)
    (∑' (b : ℕ),
      HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℝ) (↑b : ℝ) 1 + 0) 0 *
        rexp (-π * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℝ) (↑b : ℝ) 1 + 0) 2 * t))
    (∑' (n : ℕ),
      HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) 0 *
        rexp (-π * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) 2 * t))
⊢ ∑' (b : ℕ), f_nat 0 0 t (b + 1) = F_nat 0 1 t

Tactic:
simp_rw [F_nat, f_nat, Nat.cast_add, Nat.cast_one, add_zero]

Premises used: Nat.cast_add, HurwitzKernelBounds.f_nat, add_zero, Nat.cast_one, HurwitzKernelBounds.F_nat
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
t : ℝ
ht : 0 < t
h : rexp (-π * t) = rexp (-π * 1 * t)
h₁ h₂ : rexp (-π * t) = rexp (-π * t)
⊢ rexp (-π * t) = rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) 1 2 * t)

Tactic:
rw [one_pow, mul_one]

Premises used: one_pow, mul_one