awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Identities (goal)
Goal:
f : ℍ → ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
s : Set (GL (Fin 2) ℝ)
hΓ : Γ = Subgroup.closure s
k : ℤ
mp :
  (∀ γ ∈ Γ, @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ f = f) →
    ∀ γ ∈ s, @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ f = f
⊢ (∀ γ ∈ Γ, @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ f = f) ↔
    ∀ γ ∈ s, @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ f = f
have mpr : (∀ γ ∈ s, @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ f = f) →
  ∀ γ ∈ Γ, @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ f = f
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Identities (goal)
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γ : γ ∈ Γ
⊢ @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ f = f
have 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
Tactic: apply Subgroup.closure_induction (p := fun γ _ ↦ f ∣[k] γ = f) h (by simp)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Identities (goal)
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
⊢ @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ f = f
have 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
Tactic: apply Subgroup.closure_induction (p := fun γ _ ↦ f ∣[k] γ = f) h (by simp)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Identities (goal)
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
⊢ @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ f = f
have mpr₂ : Membership.mem (γ := Subgroup (GL (Fin 2) ℝ)) (Subgroup.closure s) γ
Tactic: apply Subgroup.closure_induction (p := fun γ _ ↦ f ∣[k] γ = f) h (by simp)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Identities (goal)
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⁻¹ f = f
have 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
Tactic: rw [← hf, ← SlashAction.slash_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
c d : ℝ
hcd : c ≤ d
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ rexp (-d * t)) fun (t : ℝ) ↦ rexp (-c * t)
have hfg : ∀ᶠ (x : ℝ) in atTop, ‖rexp (-d * x)‖ ≤ rexp (-c * x)
Tactic: apply Eventually.isBigO
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
c d : ℝ
hcd : c ≤ d
⊢ ∀ᶠ (x : ℝ) in atTop, ‖rexp (-d * x)‖ ≤ rexp (-c * x)
have h : ∀ (t : ℝ) (ht : 0 < t), ‖rexp (-d * t)‖ ≤ rexp (-c * t)
Tactic: filter_upwards [eventually_gt_atTop 0] with t ht
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
c d : ℝ
hcd : c ≤ d
t : ℝ
ht : 0 < t
⊢ ‖rexp (-d * t)‖ ≤ rexp (-c * t)
have h : rexp (-d * t) ≤ rexp (-c * t)
Tactic: rw [norm_of_nonneg (exp_pos _).le]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
c d : ℝ
hcd : c ≤ d
t : ℝ
ht : 0 < t
⊢ rexp (-d * t) ≤ rexp (-c * t)
have h : 0 ≤ t
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ (1 - rexp (-π * t))⁻¹) fun (x : ℝ) ↦ 1
have refine : Tendsto (β := ℝ) (fun (x : ℝ) ↦ rexp (-π * x)) atTop (𝓝 0)
Tactic: refine ((Tendsto.const_sub _ ?_).inv₀ (by simp)).isBigO_one ℝ (c := ((1 - 0)⁻¹ : ℝ))
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
k : ℕ
a t : ℝ
ha : 0 ≤ a
ht : 0 < t
n : ℕ
⊢ ‖f_nat k a t n‖ ≤ g_nat k a t n
have rw : ((↑n : ℝ) + a) ^ k * rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t) ≤
  ((↑n : ℝ) + a) ^ k * rexp (-π * ((↑n : ℝ) + HPow.hPow (β := ℕ) a 2) * t)
Tactic: rw [f_nat, norm_of_nonneg (by positivity), g_nat]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
k : ℕ
a t : ℝ
ha : 0 ≤ a
ht : 0 < t
n : ℕ
⊢ ((↑n : ℝ) + a) ^ k * rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t) ≤
    ((↑n : ℝ) + a) ^ k * rexp (-π * ((↑n : ℝ) + HPow.hPow (β := ℕ) a 2) * t)
have 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))
Tactic: simp only [neg_mul, add_sq]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
k : ℕ
a t : ℝ
ha : 0 ≤ a
ht : 0 < t
n : ℕ
⊢ ((↑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))
have hbc : (↑n : ℝ) ≤ HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 + HMul.hMul (α := ℝ) 2 (↑n : ℝ) * a
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (hypothesis)
Goal:
k : ℕ
a t : ℝ
ha : 0 ≤ a
ht : 0 < t
n : ℕ
⊢ (↑n : ℝ) ≤ HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 + HMul.hMul (α := ℝ) 2 (↑n : ℝ) * a
have H₁ : (↑n : ℝ) ≤ HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2
Tactic: have H₁ : (n : ℝ) ≤ n ^ 2 := mod_cast Nat.le_self_pow two_ne_zero n
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (hypothesis)
Goal:
k : ℕ
a t : ℝ
ha : 0 ≤ a
ht : 0 < t
n : ℕ
H₁ : (↑n : ℝ) ≤ HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2
⊢ (↑n : ℝ) ≤ HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 + HMul.hMul (α := ℝ) 2 (↑n : ℝ) * a
have H₂ : 0 ≤ HMul.hMul (α := ℝ) 2 (↑n : ℝ) * a
Tactic: have H₂ : 0 ≤ 2 * n * a := by positivity
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
k : ℕ
a t : ℝ
ht : 0 < t
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) k * rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t)
have 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
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 ↦ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
k : ℕ
a t : ℝ
ht : 0 < t
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
have 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))
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]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
k : ℕ
a t : ℝ
ht : 0 < t
n : ℕ
⊢ 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))
have hbc : -π * (HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t) ≤
  -π * (t * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * (|a| * (t * (↑n : ℝ)))) + -π * (HPow.hPow (β := ℕ) a 2 * t)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
k : ℕ
a t : ℝ
ht : 0 < t
n : ℕ
⊢ -π * (HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t) ≤
    -π * (t * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * (|a| * (t * (↑n : ℝ)))) + -π * (HPow.hPow (β := ℕ) a 2 * t)
have hbc : 0 ≤
  -π * (t * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * (|a| * (t * (↑n : ℝ)))) + -π * (HPow.hPow (β := ℕ) a 2 * t) -
    -π * (HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t)
Tactic: rw [← sub_nonneg]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
k : ℕ
a t : ℝ
ht : 0 < t
n : ℕ
⊢ 0 ≤
    -π * (t * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * (|a| * (t * (↑n : ℝ)))) + -π * (HPow.hPow (β := ℕ) a 2 * t) -
      -π * (HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t)
have hbc : 0 ≤ π * t * (↑n : ℝ) * (|a| + a) * 2
Tactic: rw [show -π * (t * n ^ 2 - 2 * (|a| * (t * n))) + -π * (a ^ 2 * t) - -π * ((n + a) ^ 2 * t)
         = π * t * n * (|a| + a) * 2 by ring]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
k : ℕ
a t : ℝ
ht : 0 < t
n : ℕ
⊢ 0 ≤ π * t * (↑n : ℝ) * (|a| + a) * 2
have hbc : 0 ≤ |a| + a
Tactic: refine mul_nonneg (mul_nonneg (by positivity) ?_) two_pos.le
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
k : ℕ
a t : ℝ
ht : 0 < t
n : ℕ
⊢ 0 ≤ |a| + a
have hbc : -a ≤ |a|
Tactic: rw [← neg_le_iff_add_nonneg]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (hypothesis)
Goal:
k : ℕ
a t : ℝ
ht : 0 < t
⊢ Summable (f_nat k a t)
have this : 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
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
k : ℕ
a t : ℝ
ht : 0 < t
this :
  Summable (α := ℝ) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) k * rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t)
⊢ Summable (f_nat k a t)
have 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))
Tactic: apply (this.mul_left (2 ^ k)).of_norm_bounded_eventually_nat
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
k : ℕ
a t : ℝ
ht : 0 < t
this :
  Summable (α := ℝ) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) k * rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t)
⊢ ∀ᶠ (i : ℕ) in atTop,
    ‖f_nat k a t i‖ ≤
      HPow.hPow (α := ℝ) 2 k * (HPow.hPow (α := ℝ) (↑i : ℝ) k * rexp (-π * HPow.hPow (β := ℕ) ((↑i : ℝ) + a) 2 * t))
have simp_rw : ∀ᶠ (i : ℕ) in atTop, |(↑i : ℝ) + a| ^ k ≤ HAdd.hAdd (α := ℝ) (↑i : ℝ) (↑i : ℝ) ^ k
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]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
k : ℕ
a t : ℝ
ht : 0 < t
this :
  Summable (α := ℝ) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) k * rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t)
⊢ ∀ᶠ (i : ℕ) in atTop, |(↑i : ℝ) + a| ^ k ≤ HAdd.hAdd (α := ℝ) (↑i : ℝ) (↑i : ℝ) ^ k
have h : ∀ (n : ℕ) (hn : ⌈|a|⌉₊ ≤ n), |(↑n : ℝ) + a| ^ k ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) (↑n : ℝ) ^ k
Tactic: filter_upwards [eventually_ge_atTop (Nat.ceil |a|)] with n hn
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
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| ^ k ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) (↑n : ℝ) ^ k
have h : |(↑n : ℝ) + a| ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) (↑n : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
⊢ ‖F_nat 0 a t‖ ≤ rexp (-π * HPow.hPow (β := ℕ) a 2 * t) / (1 - rexp (-π * t))
have refine : HasSum (g_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)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
⊢ HasSum (g_nat 0 a t) (rexp (-π * HPow.hPow (β := ℕ) a 2 * t) / (1 - rexp (-π * t)))
have h : g_nat 0 a t = fun (i : ℕ) ↦ rexp (-π * HPow.hPow (β := ℕ) a 2 * t) * rexp (-π * t) ^ i
Tactic: convert! (hasSum_geometric_of_lt_one (exp_pos _).le <| exp_lt_aux ht).mul_left _ using 1
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
⊢ g_nat 0 a t = fun (i : ℕ) ↦ rexp (-π * HPow.hPow (β := ℕ) a 2 * t) * rexp (-π * t) ^ i
have h : ∀ (n : ℕ), g_nat 0 a t n = rexp (-π * HPow.hPow (β := ℕ) a 2 * t) * rexp (-π * t) ^ n
Tactic: ext1 n
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
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) * rexp (-π * t) ^ n
have h : HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 0 * rexp (-π * ((↑n : ℝ) + HPow.hPow (β := ℕ) a 2) * t) =
  rexp (-π * HPow.hPow (β := ℕ) a 2 * t + (↑n : ℝ) * (-π * t))
Tactic: rw [← Real.exp_nat_mul, ← Real.exp_add]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
t : ℝ
ht : 0 < t
⊢ ‖F_nat 0 0 t - 1‖ ≤ rexp (-π * t) / (1 - rexp (-π * t))
have h : F_nat 0 0 t - 1 = F_nat 0 1 t
Tactic: convert! F_nat_zero_le zero_le_one ht using 2
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
t : ℝ
ht : 0 < t
h : F_nat 0 0 t - 1 = F_nat 0 1 t
⊢ ‖F_nat 0 0 t - 1‖ ≤ rexp (-π * t) / (1 - rexp (-π * t))
have h₁ : rexp (-π * t) = rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) 1 2 * t)
Tactic: convert! F_nat_zero_le zero_le_one ht using 2
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
t : ℝ
ht : 0 < t
⊢ F_nat 0 0 t - 1 = F_nat 0 1 t
have h : ∑' (b : ℕ), f_nat 0 0 t (b + 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]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
t : ℝ
ht : 0 < t
⊢ ∑' (b : ℕ), f_nat 0 0 t (b + 1) = F_nat 0 1 t
have h : Eq (α := ℝ) (∑' (b : ℕ), f_nat 0 0 t (b + 1)) (∑' (n : ℕ), f_nat 0 1 t n)
Tactic: simp_rw [F_nat, f_nat, Nat.cast_add, Nat.cast_one, add_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
t : ℝ
ht : 0 < t
h : Eq (α := ℝ) (∑' (b : ℕ), f_nat 0 0 t (b + 1)) (∑' (n : ℕ), f_nat 0 1 t n)
⊢ ∑' (b : ℕ), f_nat 0 0 t (b + 1) = F_nat 0 1 t
have 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))
Tactic: simp_rw [F_nat, f_nat, Nat.cast_add, Nat.cast_one, add_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
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))
⊢ ∑' (b : ℕ), f_nat 0 0 t (b + 1) = F_nat 0 1 t
have 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))
Tactic: simp_rw [F_nat, f_nat, Nat.cast_add, Nat.cast_one, add_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
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))
⊢ ∑' (b : ℕ), f_nat 0 0 t (b + 1) = F_nat 0 1 t
have 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))
Tactic: simp_rw [F_nat, f_nat, Nat.cast_add, Nat.cast_one, add_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
t : ℝ
ht : 0 < t
⊢ rexp (-π * t) = rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) 1 2 * t)
have h : rexp (-π * t) = rexp (-π * 1 * t)
Tactic: rw [one_pow, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
t : ℝ
ht : 0 < t
h : rexp (-π * t) = rexp (-π * 1 * t)
⊢ rexp (-π * t) = rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) 1 2 * t)
have h₁ : rexp (-π * t) = rexp (-π * t)
Tactic: rw [one_pow, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
a : ℝ
ha : 0 ≤ a
⊢ ∃ (p : ℝ),
    0 < p ∧
      IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ F_nat 0 a t - if a = 0 then 1 else 0) fun (t : ℝ) ↦ rexp (-p * t)
have pos : ∀ (h : a = 0),
  ∃ (p : ℝ), 0 < p ∧ IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ F_nat 0 a t - 1) fun (t : ℝ) ↦ rexp (-p * t)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
a : ℝ
ha : 0 ≤ a
pos :
  ∀ (h : a = 0),
    ∃ (p : ℝ), 0 < p ∧ IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ F_nat 0 a t - 1) fun (t : ℝ) ↦ rexp (-p * t)
⊢ ∃ (p : ℝ),
    0 < p ∧
      IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ F_nat 0 a t - if a = 0 then 1 else 0) fun (t : ℝ) ↦ rexp (-p * t)
have neg : ∀ (h : ¬a = 0),
  ∃ (p : ℝ), 0 < p ∧ IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ F_nat 0 a t - 0) fun (t : ℝ) ↦ rexp (-p * t)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
a : ℝ
ha : 0 ≤ a
h : a = 0
⊢ ∃ (p : ℝ), 0 < p ∧ IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ F_nat 0 a t - 1) fun (t : ℝ) ↦ rexp (-p * t)
have pos : ∃ (p : ℝ), 0 < p ∧ IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ F_nat 0 0 t - 1) fun (t : ℝ) ↦ rexp (-p * t)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
a : ℝ
ha : 0 ≤ a
h : a = 0
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ F_nat 0 0 t - 1) fun (t : ℝ) ↦ rexp (-π * t) / (1 - rexp (-π * t))
have hfg : ∀ᶠ (x : ℝ) in atTop, ‖F_nat 0 0 x - 1‖ ≤ rexp (-π * x) / (1 - rexp (-π * x))
Tactic: apply Eventually.isBigO
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
a : ℝ
ha : 0 ≤ a
h : a = 0
⊢ ∀ᶠ (x : ℝ) in atTop, ‖F_nat 0 0 x - 1‖ ≤ rexp (-π * x) / (1 - rexp (-π * x))
have h₁ : ∀ (t : ℝ) (ht : 0 < t), ‖F_nat 0 0 t - 1‖ ≤ rexp (-π * t) / (1 - rexp (-π * t))
Tactic: filter_upwards [eventually_gt_atTop 0] with t ht