awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Ico 0 1) a
p : ℝ
hp : 0 < p
hp' : IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ F_nat 0 a t - if a = 0 then 1 else 0) fun (t : ℝ) ↦ rexp (-p * t)
⊢ ∃ (p : ℝ),
    0 < p ∧
      IsBigO (E := ℝ) (F := ℝ) atTop
        (fun (t : ℝ) ↦
          F_int 0 (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t -
            if Eq (α := UnitAddCircle) (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) 0 then 1 else 0)
        fun (t : ℝ) ↦ rexp (-p * t)
have obtain : ∀ (q : ℝ) (hq : 0 < q)
  (hq' :
    IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ F_nat 0 (1 - a) t - if 1 - a = 0 then 1 else 0) fun (t : ℝ) ↦
      rexp (-q * t)),
  ∃ (p : ℝ),
    0 < p ∧
      IsBigO (E := ℝ) (F := ℝ) atTop
        (fun (t : ℝ) ↦
          F_int 0 (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t -
            if Eq (α := UnitAddCircle) (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) 0 then 1 else 0)
        fun (t : ℝ) ↦ rexp (-p * t)
Tactic: obtain ⟨q, hq, hq'⟩ := isBigO_atTop_F_nat_zero_sub (sub_nonneg.mpr ha.2.le)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Ico 0 1) a
p : ℝ
hp : 0 < p
hp' : IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ F_nat 0 a t - if a = 0 then 1 else 0) fun (t : ℝ) ↦ rexp (-p * t)
q : ℝ
hq : 0 < q
hq' :
  IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ F_nat 0 (1 - a) t - if 1 - a = 0 then 1 else 0) fun (t : ℝ) ↦
    rexp (-q * t)
⊢ ∃ (p : ℝ),
    0 < p ∧
      IsBigO (E := ℝ) (F := ℝ) atTop
        (fun (t : ℝ) ↦
          F_int 0 (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t -
            if Eq (α := UnitAddCircle) (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) 0 then 1 else 0)
        fun (t : ℝ) ↦ rexp (-p * t)
have simp_rw : ∃ (p : ℝ),
  0 < p ∧
    IsBigO (E := ℝ) (F := ℝ) atTop
      (fun (t : ℝ) ↦ F_int 0 (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t - if a = 0 then 1 else 0) fun (t : ℝ) ↦ rexp (-p * t)
Tactic: simp_rw [AddCircle.coe_eq_zero_iff_of_mem_Ico ha]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Ico 0 1) a
p : ℝ
hp : 0 < p
hp' : IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ F_nat 0 a t - if a = 0 then 1 else 0) fun (t : ℝ) ↦ rexp (-p * t)
q : ℝ
hq : 0 < q
hq' :
  IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ F_nat 0 (1 - a) t - if 1 - a = 0 then 1 else 0) fun (t : ℝ) ↦
    rexp (-q * t)
⊢ 1 - a ≠ 0
have linarith : 1 - a = 0 → 1 - a - 0 + (a - 1) = 0
Tactic: linarith [ha.2]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (hypothesis)
Goal:
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Ico 0 1) a
p : ℝ
hp : 0 < p
hp' : IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ F_nat 0 a t - if a = 0 then 1 else 0) fun (t : ℝ) ↦ rexp (-p * t)
q : ℝ
hq : 0 < q
hq' :
  IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ F_nat 0 (1 - a) t - if 1 - a = 0 then 1 else 0) fun (t : ℝ) ↦
    rexp (-q * t)
⊢ ∃ (p : ℝ),
    0 < p ∧
      IsBigO (E := ℝ) (F := ℝ) atTop
        (fun (t : ℝ) ↦ F_int 0 (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t - if a = 0 then 1 else 0) fun (t : ℝ) ↦
        rexp (-p * t)
have hq'₁ : IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ F_nat 0 (1 - a) t) fun (t : ℝ) ↦ rexp (-q * t)
Tactic: simp_rw [eq_false_intro (by linarith [ha.2] : 1 - a ≠ 0), if_false, sub_zero] at hq'
Cleared hypotheses: hq'
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Ico 0 1) a
p : ℝ
hp : 0 < p
hp' : IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ F_nat 0 a t - if a = 0 then 1 else 0) fun (t : ℝ) ↦ rexp (-p * t)
q : ℝ
hq : 0 < q
hq' : IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ F_nat 0 (1 - a) t) fun (t : ℝ) ↦ rexp (-q * t)
⊢ ∃ (p : ℝ),
    0 < p ∧
      IsBigO (E := ℝ) (F := ℝ) atTop
        (fun (t : ℝ) ↦ F_int 0 (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t - if a = 0 then 1 else 0) fun (t : ℝ) ↦
        rexp (-p * t)
have refine : IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ F_int 0 (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t - if a = 0 then 1 else 0)
  fun (t : ℝ) ↦ rexp (-min p q * t)
Tactic: refine ⟨_, lt_min hp hq, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Ico 0 1) a
p : ℝ
hp : 0 < p
hp' : IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ F_nat 0 a t - if a = 0 then 1 else 0) fun (t : ℝ) ↦ rexp (-p * t)
q : ℝ
hq : 0 < q
hq' : IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ F_nat 0 (1 - a) t) fun (t : ℝ) ↦ rexp (-q * t)
⊢ EventuallyEq (β := ℝ) atTop (fun (t : ℝ) ↦ F_int 0 (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t - if a = 0 then 1 else 0)
    fun (t : ℝ) ↦ (F_nat 0 a t - if a = 0 then 1 else 0) + F_nat 0 (1 - a) t
have h : ∀ (t : ℝ) (ht : 0 < t),
  (F_int 0 (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t - if a = 0 then 1 else 0) =
    (F_nat 0 a t - if a = 0 then 1 else 0) + F_nat 0 (1 - a) t
Tactic: filter_upwards [eventually_gt_atTop 0] with t ht
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Ico 0 1) a
p : ℝ
hp : 0 < p
hp' : IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ F_nat 0 a t - if a = 0 then 1 else 0) fun (t : ℝ) ↦ rexp (-p * t)
q : ℝ
hq : 0 < q
hq' : IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ F_nat 0 (1 - a) t) fun (t : ℝ) ↦ rexp (-q * t)
t : ℝ
ht : 0 < t
⊢ (F_int 0 (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t - if a = 0 then 1 else 0) =
    (F_nat 0 a t - if a = 0 then 1 else 0) + F_nat 0 (1 - a) t
have h : (F_nat 0 a t + F_nat 0 (1 - a) t - if a = 0 then 1 else 0) = (F_nat 0 a t - if a = 0 then 1 else 0) + F_nat 0 (1 - a) t
Tactic: rw [F_int_eq_of_mem_Icc 0 (Ico_subset_Icc_self ha) ht]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (hypothesis)
Goal:
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Ico 0 1) a
p : ℝ
hp : 0 < p
hp' : IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ F_nat 0 a t - if a = 0 then 1 else 0) fun (t : ℝ) ↦ rexp (-p * t)
q : ℝ
hq : 0 < q
hq' : IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ F_nat 0 (1 - a) t) fun (t : ℝ) ↦ rexp (-q * t)
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ F_int 0 (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t - if a = 0 then 1 else 0)
    fun (t : ℝ) ↦ rexp (-min p q * t)
have this : EventuallyEq (β := ℝ) atTop (fun (t : ℝ) ↦ F_int 0 (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t - if a = 0 then 1 else 0)
  fun (t : ℝ) ↦ (F_nat 0 a t - if a = 0 then 1 else 0) + F_nat 0 (1 - a) t
Tactic: have : (fun t ↦ F_int 0 a t - (if a = 0 then 1 else 0)) =ᶠ[atTop]
      fun t ↦ (F_nat 0 a t - (if a = 0 then 1 else 0)) + F_nat 0 (1 - a) t := by
    filter_upwards [eventually_gt_atTop 0] with t ht
    rw [F_int_eq_of_mem_Icc 0 (Ico_subset_Icc_self ha) ht]
    ring
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Ico 0 1) a
p : ℝ
hp : 0 < p
hp' : IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ F_nat 0 a t - if a = 0 then 1 else 0) fun (t : ℝ) ↦ rexp (-p * t)
q : ℝ
hq : 0 < q
hq' : IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ F_nat 0 (1 - a) t) fun (t : ℝ) ↦ rexp (-q * t)
this :
  EventuallyEq (β := ℝ) atTop (fun (t : ℝ) ↦ F_int 0 (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t - if a = 0 then 1 else 0)
    fun (t : ℝ) ↦ (F_nat 0 a t - if a = 0 then 1 else 0) + F_nat 0 (1 - a) t
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ F_int 0 (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t - if a = 0 then 1 else 0)
    fun (t : ℝ) ↦ rexp (-min p q * t)
have refine_1 : IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ rexp (-p * t)) fun (t : ℝ) ↦ rexp (-min p q * t)
Tactic: refine this.isBigO.trans ((hp'.trans ?_).add (hq'.trans ?_))
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Ico 0 1) a
p : ℝ
hp : 0 < p
hp' : IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ F_nat 0 a t - if a = 0 then 1 else 0) fun (t : ℝ) ↦ rexp (-p * t)
q : ℝ
hq : 0 < q
hq' : IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ F_nat 0 (1 - a) t) fun (t : ℝ) ↦ rexp (-q * t)
this :
  EventuallyEq (β := ℝ) atTop (fun (t : ℝ) ↦ F_int 0 (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t - if a = 0 then 1 else 0)
    fun (t : ℝ) ↦ (F_nat 0 a t - if a = 0 then 1 else 0) + F_nat 0 (1 - a) t
refine_1 : IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ rexp (-p * t)) fun (t : ℝ) ↦ rexp (-min p q * t)
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ F_int 0 (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t - if a = 0 then 1 else 0)
    fun (t : ℝ) ↦ rexp (-min p q * t)
have refine_2 : IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ rexp (-q * t)) fun (t : ℝ) ↦ rexp (-min p q * t)
Tactic: refine this.isBigO.trans ((hp'.trans ?_).add (hq'.trans ?_))
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Ico 0 1) a
p : ℝ
hp : 0 < p
hp' : IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ F_nat 0 a t - if a = 0 then 1 else 0) fun (t : ℝ) ↦ rexp (-p * t)
q : ℝ
hq : 0 < q
hq' : IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ F_nat 0 (1 - a) t) fun (t : ℝ) ↦ rexp (-q * t)
this :
  EventuallyEq (β := ℝ) atTop (fun (t : ℝ) ↦ F_int 0 (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t - if a = 0 then 1 else 0)
    fun (t : ℝ) ↦ (F_nat 0 a t - if a = 0 then 1 else 0) + F_nat 0 (1 - a) t
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ rexp (-p * t)) fun (t : ℝ) ↦ rexp (-min p q * t)
have refine_1 : min p q ≤ p
Tactic: apply isBigO_exp_neg_mul_of_le
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Ico 0 1) a
p : ℝ
hp : 0 < p
hp' : IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ F_nat 0 a t - if a = 0 then 1 else 0) fun (t : ℝ) ↦ rexp (-p * t)
q : ℝ
hq : 0 < q
hq' : IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ F_nat 0 (1 - a) t) fun (t : ℝ) ↦ rexp (-q * t)
this :
  EventuallyEq (β := ℝ) atTop (fun (t : ℝ) ↦ F_int 0 (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t - if a = 0 then 1 else 0)
    fun (t : ℝ) ↦ (F_nat 0 a t - if a = 0 then 1 else 0) + F_nat 0 (1 - a) t
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ rexp (-q * t)) fun (t : ℝ) ↦ rexp (-min p q * t)
have refine_2 : min p q ≤ q
Tactic: apply isBigO_exp_neg_mul_of_le
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
a : UnitAddCircle
⊢ ∃ (p : ℝ), 0 < p ∧ IsBigO (F := ℝ) atTop (F_int 1 a) fun (t : ℝ) ↦ rexp (-p * t)
have obtain : ∀ (a : ℝ) (ha : Membership.mem (γ := Set ℝ) (Ico 0 1) a),
  ∃ (p : ℝ), 0 < p ∧ IsBigO (F := ℝ) atTop (F_int 1 (↑a : ℝ ⧸ AddSubgroup.zmultiples 1)) fun (t : ℝ) ↦ rexp (-p * t)
Tactic: obtain ⟨a, ha, rfl⟩ := a.eq_coe_Ico
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Ico 0 1) a
⊢ ∃ (p : ℝ), 0 < p ∧ IsBigO (F := ℝ) atTop (F_int 1 (↑a : ℝ ⧸ AddSubgroup.zmultiples 1)) fun (t : ℝ) ↦ rexp (-p * t)
have obtain : ∀ (p : ℝ) (hp : 0 < p) (hp' : IsBigO (F := ℝ) atTop (F_nat 1 a) fun (t : ℝ) ↦ rexp (-p * t)),
  ∃ (p : ℝ), 0 < p ∧ IsBigO (F := ℝ) atTop (F_int 1 (↑a : ℝ ⧸ AddSubgroup.zmultiples 1)) fun (t : ℝ) ↦ rexp (-p * t)
Tactic: obtain ⟨p, hp, hp'⟩ := isBigO_atTop_F_nat_one ha.1
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Ico 0 1) a
p : ℝ
hp : 0 < p
hp' : IsBigO (F := ℝ) atTop (F_nat 1 a) fun (t : ℝ) ↦ rexp (-p * t)
⊢ ∃ (p : ℝ), 0 < p ∧ IsBigO (F := ℝ) atTop (F_int 1 (↑a : ℝ ⧸ AddSubgroup.zmultiples 1)) fun (t : ℝ) ↦ rexp (-p * t)
have obtain : ∀ (q : ℝ) (hq : 0 < q) (hq' : IsBigO (F := ℝ) atTop (F_nat 1 (1 - a)) fun (t : ℝ) ↦ rexp (-q * t)),
  ∃ (p : ℝ), 0 < p ∧ IsBigO (F := ℝ) atTop (F_int 1 (↑a : ℝ ⧸ AddSubgroup.zmultiples 1)) fun (t : ℝ) ↦ rexp (-p * t)
Tactic: obtain ⟨q, hq, hq'⟩ := isBigO_atTop_F_nat_one (sub_nonneg.mpr ha.2.le)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Ico 0 1) a
p : ℝ
hp : 0 < p
hp' : IsBigO (F := ℝ) atTop (F_nat 1 a) fun (t : ℝ) ↦ rexp (-p * t)
q : ℝ
hq : 0 < q
hq' : IsBigO (F := ℝ) atTop (F_nat 1 (1 - a)) fun (t : ℝ) ↦ rexp (-q * t)
⊢ ∃ (p : ℝ), 0 < p ∧ IsBigO (F := ℝ) atTop (F_int 1 (↑a : ℝ ⧸ AddSubgroup.zmultiples 1)) fun (t : ℝ) ↦ rexp (-p * t)
have refine : IsBigO (F := ℝ) atTop (F_int 1 (↑a : ℝ ⧸ AddSubgroup.zmultiples 1)) fun (t : ℝ) ↦ rexp (-min p q * t)
Tactic: refine ⟨_, lt_min hp hq, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Ico 0 1) a
p : ℝ
hp : 0 < p
hp' : IsBigO (F := ℝ) atTop (F_nat 1 a) fun (t : ℝ) ↦ rexp (-p * t)
q : ℝ
hq : 0 < q
hq' : IsBigO (F := ℝ) atTop (F_nat 1 (1 - a)) fun (t : ℝ) ↦ rexp (-q * t)
⊢ F_int 1 (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) =ᶠ[atTop] fun (t : ℝ) ↦ F_nat 1 a t + F_nat 1 (1 - a) t
have h : ∀ (t : ℝ) (ht : 0 < t), F_int 1 (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t = F_nat 1 a t + F_nat 1 (1 - a) t
Tactic: filter_upwards [eventually_gt_atTop 0] with t ht
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (hypothesis)
Goal:
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Ico 0 1) a
p : ℝ
hp : 0 < p
hp' : IsBigO (F := ℝ) atTop (F_nat 1 a) fun (t : ℝ) ↦ rexp (-p * t)
q : ℝ
hq : 0 < q
hq' : IsBigO (F := ℝ) atTop (F_nat 1 (1 - a)) fun (t : ℝ) ↦ rexp (-q * t)
⊢ IsBigO (F := ℝ) atTop (F_int 1 (↑a : ℝ ⧸ AddSubgroup.zmultiples 1)) fun (t : ℝ) ↦ rexp (-min p q * t)
have this : F_int 1 (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) =ᶠ[atTop] fun (t : ℝ) ↦ F_nat 1 a t + F_nat 1 (1 - a) t
Tactic: have : F_int 1 a =ᶠ[atTop] fun t ↦ F_nat 1 a t + F_nat 1 (1 - a) t := by
    filter_upwards [eventually_gt_atTop 0] with t ht
    exact F_int_eq_of_mem_Icc 1 (Ico_subset_Icc_self ha) ht
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Ico 0 1) a
p : ℝ
hp : 0 < p
hp' : IsBigO (F := ℝ) atTop (F_nat 1 a) fun (t : ℝ) ↦ rexp (-p * t)
q : ℝ
hq : 0 < q
hq' : IsBigO (F := ℝ) atTop (F_nat 1 (1 - a)) fun (t : ℝ) ↦ rexp (-q * t)
this : F_int 1 (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) =ᶠ[atTop] fun (t : ℝ) ↦ F_nat 1 a t + F_nat 1 (1 - a) t
⊢ IsBigO (F := ℝ) atTop (F_int 1 (↑a : ℝ ⧸ AddSubgroup.zmultiples 1)) fun (t : ℝ) ↦ rexp (-min p q * t)
have refine_1 : IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ rexp (-p * t)) fun (t : ℝ) ↦ rexp (-min p q * t)
Tactic: refine this.isBigO.trans ((hp'.trans ?_).add (hq'.trans ?_))
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Ico 0 1) a
p : ℝ
hp : 0 < p
hp' : IsBigO (F := ℝ) atTop (F_nat 1 a) fun (t : ℝ) ↦ rexp (-p * t)
q : ℝ
hq : 0 < q
hq' : IsBigO (F := ℝ) atTop (F_nat 1 (1 - a)) fun (t : ℝ) ↦ rexp (-q * t)
this : F_int 1 (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) =ᶠ[atTop] fun (t : ℝ) ↦ F_nat 1 a t + F_nat 1 (1 - a) t
refine_1 : IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ rexp (-p * t)) fun (t : ℝ) ↦ rexp (-min p q * t)
⊢ IsBigO (F := ℝ) atTop (F_int 1 (↑a : ℝ ⧸ AddSubgroup.zmultiples 1)) fun (t : ℝ) ↦ rexp (-min p q * t)
have refine_2 : IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ rexp (-q * t)) fun (t : ℝ) ↦ rexp (-min p q * t)
Tactic: refine this.isBigO.trans ((hp'.trans ?_).add (hq'.trans ?_))
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Ico 0 1) a
p : ℝ
hp : 0 < p
hp' : IsBigO (F := ℝ) atTop (F_nat 1 a) fun (t : ℝ) ↦ rexp (-p * t)
q : ℝ
hq : 0 < q
hq' : IsBigO (F := ℝ) atTop (F_nat 1 (1 - a)) fun (t : ℝ) ↦ rexp (-q * t)
this : F_int 1 (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) =ᶠ[atTop] fun (t : ℝ) ↦ F_nat 1 a t + F_nat 1 (1 - a) t
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ rexp (-p * t)) fun (t : ℝ) ↦ rexp (-min p q * t)
have refine_1 : min p q ≤ p
Tactic: apply isBigO_exp_neg_mul_of_le
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Ico 0 1) a
p : ℝ
hp : 0 < p
hp' : IsBigO (F := ℝ) atTop (F_nat 1 a) fun (t : ℝ) ↦ rexp (-p * t)
q : ℝ
hq : 0 < q
hq' : IsBigO (F := ℝ) atTop (F_nat 1 (1 - a)) fun (t : ℝ) ↦ rexp (-q * t)
this : F_int 1 (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) =ᶠ[atTop] fun (t : ℝ) ↦ F_nat 1 a t + F_nat 1 (1 - a) t
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ rexp (-q * t)) fun (t : ℝ) ↦ rexp (-min p q * t)
have refine_2 : min p q ≤ q
Tactic: apply isBigO_exp_neg_mul_of_le
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable (goal)
Goal:
τ : ℂ
⊢ jacobiTheta (2 + τ) = jacobiTheta τ
have simp_rw : jacobiTheta₂ 0 (2 + τ) = jacobiTheta₂ 0 τ
Tactic: simp_rw [jacobiTheta_eq_jacobiTheta₂, add_comm, jacobiTheta₂_add_right]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable (goal)
Goal:
τ : ℂ
simp_rw : jacobiTheta₂ 0 (2 + τ) = jacobiTheta₂ 0 τ
⊢ jacobiTheta (2 + τ) = jacobiTheta τ
have simp_rw₁ : jacobiTheta₂ 0 (τ + 2) = jacobiTheta₂ 0 τ
Tactic: simp_rw [jacobiTheta_eq_jacobiTheta₂, add_comm, jacobiTheta₂_add_right]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable (goal)
Goal:
τ : ℍ
this : (↑(HPow.hPow (β := ℕ) ModularGroup.T 2 • τ) : ℂ) = 2 + (↑τ : ℂ)
⊢ jacobiTheta (↑(HPow.hPow (β := ℕ) ModularGroup.T 2 • τ) : ℂ) = jacobiTheta (↑τ : ℂ)
have simp_rw : jacobiTheta (2 + (↑τ : ℂ)) = jacobiTheta (↑τ : ℂ)
Tactic: simp_rw [this, jacobiTheta_two_add]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable (goal)
Goal:
τ : ℍ
⊢ jacobiTheta (↑(HPow.hPow (β := ℕ) ModularGroup.T 2 • τ) : ℂ) = jacobiTheta (↑τ : ℂ)
have suffices : (↑(HPow.hPow (β := ℕ) ModularGroup.T 2 • τ) : ℂ) = 2 + (↑τ : ℂ)
Tactic: suffices (ModularGroup.T ^ 2 • τ :) = (2 : ℂ) + ↑τ by simp_rw [this, jacobiTheta_two_add]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable (hypothesis)
Goal:
τ : ℍ
⊢ (↑(HPow.hPow (β := ℕ) ModularGroup.T 2 • τ) : ℂ) = 2 + (↑τ : ℂ)
have this : HPow.hPow (β := ℕ) ModularGroup.T 2 = HPow.hPow (β := ℤ) ModularGroup.T 2
Tactic: have : ModularGroup.T ^ (2 : ℕ) = ModularGroup.T ^ (2 : ℤ) := rfl
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable (goal)
Goal:
τ : ℍ
this : HPow.hPow (β := ℕ) ModularGroup.T 2 = HPow.hPow (β := ℤ) ModularGroup.T 2
⊢ (↑(HPow.hPow (β := ℕ) ModularGroup.T 2 • τ) : ℂ) = 2 + (↑τ : ℂ)
have simp_rw : (↑(↑2 : ℝ) : ℂ) + (↑τ : ℂ) = 2 + (↑τ : ℂ)
Tactic: simp_rw [this, UpperHalfPlane.modular_T_zpow_smul, UpperHalfPlane.coe_vadd]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable (goal)
Goal:
τ : ℍ
this : HPow.hPow (β := ℕ) ModularGroup.T 2 = HPow.hPow (β := ℤ) ModularGroup.T 2
⊢ (↑(↑2 : ℝ) : ℂ) + (↑τ : ℂ) = 2 + (↑τ : ℂ)
have norm_cast : 2 + (↑τ : ℂ) = 2 + (↑τ : ℂ)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable (hypothesis)
Goal:
τ : ℍ
⊢ jacobiTheta (↑(ModularGroup.S • τ) : ℂ) = (-I * (↑τ : ℂ)) ^ (1 / 2) * jacobiTheta (↑τ : ℂ)
have h0 : (↑τ : ℂ) ≠ 0
Tactic: have h0 : (τ : ℂ) ≠ 0 := ne_of_apply_ne im (zero_im.symm ▸ ne_of_gt τ.2)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable (goal)
Goal:
τ : ℍ
h0 : (↑τ : ℂ) ≠ 0
⊢ (-I * (↑τ : ℂ)) ^ (1 / 2) ≠ 0
have rw : ¬-I * (↑τ : ℂ) = 0 ∨ ¬1 / 2 ≠ 0
Tactic: rw [Ne, cpow_eq_zero_iff, not_and_or]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable (hypothesis)
Goal:
τ : ℍ
h0 : (↑τ : ℂ) ≠ 0
⊢ jacobiTheta (↑(ModularGroup.S • τ) : ℂ) = (-I * (↑τ : ℂ)) ^ (1 / 2) * jacobiTheta (↑τ : ℂ)
have h1 : (-I * (↑τ : ℂ)) ^ (1 / 2) ≠ 0
Tactic: have h1 : (-I * τ) ^ (1 / 2 : ℂ) ≠ 0 := by
    rw [Ne, cpow_eq_zero_iff, not_and_or]
    exact Or.inl <| mul_ne_zero (neg_ne_zero.mpr I_ne_zero) h0
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable (goal)
Goal:
τ : ℍ
h0 : (↑τ : ℂ) ≠ 0
h1 : (-I * (↑τ : ℂ)) ^ (1 / 2) ≠ 0
⊢ jacobiTheta (↑(ModularGroup.S • τ) : ℂ) = (-I * (↑τ : ℂ)) ^ (1 / 2) * jacobiTheta (↑τ : ℂ)
have simp_rw : jacobiTheta₂ (↑0 : ℂ) (-(↑τ : ℂ))⁻¹ = (-I * (↑τ : ℂ)) ^ (1 / 2) * jacobiTheta₂ (↑0 : ℂ) (↑τ : ℂ)
Tactic: simp_rw [UpperHalfPlane.modular_S_smul, jacobiTheta_eq_jacobiTheta₂, ← ofReal_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable (goal)
Goal:
τ : ℍ
h0 : (↑τ : ℂ) ≠ 0
h1 : (-I * (↑τ : ℂ)) ^ (1 / 2) ≠ 0
⊢ jacobiTheta₂ 0 (-(↑τ : ℂ))⁻¹ = (-I * (↑τ : ℂ)) ^ HDiv.hDiv (α := ℂ) 1 2 * jacobiTheta₂ 0 (↑τ : ℂ)
have simp_rw : jacobiTheta₂ 0 (-(↑τ : ℂ))⁻¹ =
  (-I * (↑τ : ℂ)) ^ HDiv.hDiv (α := ℂ) 1 2 *
    (1 / (-I * (↑τ : ℂ)) ^ (1 / 2) * cexp (-(↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) 0 2 / (↑τ : ℂ)) *
      jacobiTheta₂ (0 / (↑τ : ℂ)) (-1 / (↑τ : ℂ)))
Tactic: simp_rw [jacobiTheta₂_functional_equation 0 τ, zero_pow two_ne_zero, mul_zero, zero_div,
    Complex.exp_zero, mul_one, ← mul_assoc, mul_one_div, div_self h1, one_mul,
    inv_neg, neg_div, one_div]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable (goal)
Goal:
τ : ℍ
h0 : (↑τ : ℂ) ≠ 0
h1 : (-I * (↑τ : ℂ)) ^ (1 / 2) ≠ 0
simp_rw :
  jacobiTheta₂ 0 (-(↑τ : ℂ))⁻¹ =
    (-I * (↑τ : ℂ)) ^ HDiv.hDiv (α := ℂ) 1 2 *
      (1 / (-I * (↑τ : ℂ)) ^ (1 / 2) * cexp (-(↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) 0 2 / (↑τ : ℂ)) *
        jacobiTheta₂ (0 / (↑τ : ℂ)) (-1 / (↑τ : ℂ)))
⊢ jacobiTheta₂ 0 (-(↑τ : ℂ))⁻¹ = (-I * (↑τ : ℂ)) ^ HDiv.hDiv (α := ℂ) 1 2 * jacobiTheta₂ 0 (↑τ : ℂ)
have simp_rw₁ : jacobiTheta₂ 0 (-(↑τ : ℂ))⁻¹ =
  (-I * (↑τ : ℂ)) ^ HDiv.hDiv (α := ℂ) 1 2 *
    (1 / (-I * (↑τ : ℂ)) ^ (1 / 2) * cexp (-(↑π : ℂ) * I * 0 / (↑τ : ℂ)) * jacobiTheta₂ (0 / (↑τ : ℂ)) (-1 / (↑τ : ℂ)))
Tactic: simp_rw [jacobiTheta₂_functional_equation 0 τ, zero_pow two_ne_zero, mul_zero, zero_div,
    Complex.exp_zero, mul_one, ← mul_assoc, mul_one_div, div_self h1, one_mul,
    inv_neg, neg_div, one_div]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable (goal)
Goal:
τ : ℍ
h0 : (↑τ : ℂ) ≠ 0
h1 : (-I * (↑τ : ℂ)) ^ (1 / 2) ≠ 0
simp_rw :
  jacobiTheta₂ 0 (-(↑τ : ℂ))⁻¹ =
    (-I * (↑τ : ℂ)) ^ HDiv.hDiv (α := ℂ) 1 2 *
      (1 / (-I * (↑τ : ℂ)) ^ (1 / 2) * cexp (-(↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) 0 2 / (↑τ : ℂ)) *
        jacobiTheta₂ (0 / (↑τ : ℂ)) (-1 / (↑τ : ℂ)))
simp_rw₁ :
  jacobiTheta₂ 0 (-(↑τ : ℂ))⁻¹ =
    (-I * (↑τ : ℂ)) ^ HDiv.hDiv (α := ℂ) 1 2 *
      (1 / (-I * (↑τ : ℂ)) ^ (1 / 2) * cexp (-(↑π : ℂ) * I * 0 / (↑τ : ℂ)) *
        jacobiTheta₂ (0 / (↑τ : ℂ)) (-1 / (↑τ : ℂ)))
⊢ jacobiTheta₂ 0 (-(↑τ : ℂ))⁻¹ = (-I * (↑τ : ℂ)) ^ HDiv.hDiv (α := ℂ) 1 2 * jacobiTheta₂ 0 (↑τ : ℂ)
have simp_rw₂ : jacobiTheta₂ 0 (-(↑τ : ℂ))⁻¹ =
  (-I * (↑τ : ℂ)) ^ HDiv.hDiv (α := ℂ) 1 2 *
    (1 / (-I * (↑τ : ℂ)) ^ (1 / 2) * cexp (0 / (↑τ : ℂ)) * jacobiTheta₂ (0 / (↑τ : ℂ)) (-1 / (↑τ : ℂ)))
Tactic: simp_rw [jacobiTheta₂_functional_equation 0 τ, zero_pow two_ne_zero, mul_zero, zero_div,
    Complex.exp_zero, mul_one, ← mul_assoc, mul_one_div, div_self h1, one_mul,
    inv_neg, neg_div, one_div]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable (goal)
Goal:
τ : ℍ
h0 : (↑τ : ℂ) ≠ 0
h1 : (-I * (↑τ : ℂ)) ^ (1 / 2) ≠ 0
simp_rw :
  jacobiTheta₂ 0 (-(↑τ : ℂ))⁻¹ =
    (-I * (↑τ : ℂ)) ^ HDiv.hDiv (α := ℂ) 1 2 *
      (1 / (-I * (↑τ : ℂ)) ^ (1 / 2) * cexp (-(↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) 0 2 / (↑τ : ℂ)) *
        jacobiTheta₂ (0 / (↑τ : ℂ)) (-1 / (↑τ : ℂ)))
simp_rw₁ :
  jacobiTheta₂ 0 (-(↑τ : ℂ))⁻¹ =
    (-I * (↑τ : ℂ)) ^ HDiv.hDiv (α := ℂ) 1 2 *
      (1 / (-I * (↑τ : ℂ)) ^ (1 / 2) * cexp (-(↑π : ℂ) * I * 0 / (↑τ : ℂ)) *
        jacobiTheta₂ (0 / (↑τ : ℂ)) (-1 / (↑τ : ℂ)))
simp_rw₂ :
  jacobiTheta₂ 0 (-(↑τ : ℂ))⁻¹ =
    (-I * (↑τ : ℂ)) ^ HDiv.hDiv (α := ℂ) 1 2 *
      (1 / (-I * (↑τ : ℂ)) ^ (1 / 2) * cexp (0 / (↑τ : ℂ)) * jacobiTheta₂ (0 / (↑τ : ℂ)) (-1 / (↑τ : ℂ)))
⊢ jacobiTheta₂ 0 (-(↑τ : ℂ))⁻¹ = (-I * (↑τ : ℂ)) ^ HDiv.hDiv (α := ℂ) 1 2 * jacobiTheta₂ 0 (↑τ : ℂ)
have simp_rw₃ : jacobiTheta₂ 0 (-(↑τ : ℂ))⁻¹ =
  (-I * (↑τ : ℂ)) ^ HDiv.hDiv (α := ℂ) 1 2 * (1 / (-I * (↑τ : ℂ)) ^ (1 / 2) * cexp 0 * jacobiTheta₂ 0 (-1 / (↑τ : ℂ)))
Tactic: simp_rw [jacobiTheta₂_functional_equation 0 τ, zero_pow two_ne_zero, mul_zero, zero_div,
    Complex.exp_zero, mul_one, ← mul_assoc, mul_one_div, div_self h1, one_mul,
    inv_neg, neg_div, one_div]