awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Ico 0 1) a
obtain :
  ∀ (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)
⊢ ∃ (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 ⟨p, hp, hp'⟩ := isBigO_atTop_F_nat_zero_sub ha.1

Premises used: HurwitzKernelBounds.isBigO_atTop_F_nat_zero_sub, And.left
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
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)
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)
⊢ ∃ (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)

Premises used: Iff.mpr, LT.lt.le, HurwitzKernelBounds.isBigO_atTop_F_nat_zero_sub, And.right, sub_nonneg
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
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)
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)
⊢ ∃ (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:
simp_rw [AddCircle.coe_eq_zero_iff_of_mem_Ico ha]

Premises used: AddCircle.coe_eq_zero_iff_of_mem_Ico
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
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)
linarith : 1 - a = 0 → 1 - a - 0 + (a - 1) = 0
⊢ 1 - a ≠ 0

Tactic:
linarith [ha.2]

Premises used: And.right
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
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)
⊢ 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'

Premises used: sub_zero, if_false, eq_false_intro
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
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)

Tactic:
⟨_, lt_min hp hq, ?_⟩

Premises used: lt_min, And.intro, Exists.intro
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
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)
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)
⊢ ∃ (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:
refine ⟨_, lt_min hp hq, ?_⟩
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
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)
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
⊢ 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:
filter_upwards [eventually_gt_atTop 0] with t ht

Premises used: OfNat.ofNat, Filter.eventually_gt_atTop
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
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
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
⊢ (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:
rw [F_int_eq_of_mem_Icc 0 (Ico_subset_Icc_self ha) ht]

Premises used: Set.Ico_subset_Icc_self, HurwitzKernelBounds.F_int_eq_of_mem_Icc, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
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_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:
ring
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
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

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
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
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)

Tactic:
this.isBigO.trans ((hp'.trans ?_).add (hq'.trans ?_))

Premises used: Filter.EventuallyEq.isBigO, Asymptotics.IsBigO.trans, Asymptotics.IsBigO.add
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
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)
refine_2 : IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ rexp (-q * 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)

Tactic:
refine this.isBigO.trans ((hp'.trans ?_).add (hq'.trans ?_))

Premises used: Filter.EventuallyEq.isBigO, Asymptotics.IsBigO.trans, Asymptotics.IsBigO.add
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
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 : min p q ≤ p
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ rexp (-p * t)) fun (t : ℝ) ↦ rexp (-min p q * t)

Tactic:
apply isBigO_exp_neg_mul_of_le

Premises used: HurwitzKernelBounds.isBigO_exp_neg_mul_of_le
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
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_2 : min p q ≤ q
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ rexp (-q * t)) fun (t : ℝ) ↦ rexp (-min p q * t)

Tactic:
apply isBigO_exp_neg_mul_of_le

Premises used: HurwitzKernelBounds.isBigO_exp_neg_mul_of_le
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
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
⊢ min p q ≤ p

Tactic:
min_le_left ..

Premises used: min_le_left
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
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
⊢ min p q ≤ q

Tactic:
min_le_right ..

Premises used: min_le_right
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
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
⊢ min p q ≤ p

Tactic:
exacts [min_le_left .., min_le_right ..]

Premises used: min_le_left, min_le_right
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
a : UnitAddCircle
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)
⊢ ∃ (p : ℝ), 0 < p ∧ IsBigO (F := ℝ) atTop (F_int 1 a) fun (t : ℝ) ↦ rexp (-p * t)

Tactic:
obtain ⟨a, ha, rfl⟩ := a.eq_coe_Ico

Premises used: AddCircle.eq_coe_Ico, rfl
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Ico 0 1) a
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)
⊢ ∃ (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

Premises used: HurwitzKernelBounds.isBigO_atTop_F_nat_one, And.left
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
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)
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)
⊢ ∃ (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)

Premises used: Iff.mpr, HurwitzKernelBounds.isBigO_atTop_F_nat_one, LT.lt.le, And.right, sub_nonneg
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
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)

Tactic:
⟨_, lt_min hp hq, ?_⟩

Premises used: lt_min, And.intro, Exists.intro
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
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)
refine : IsBigO (F := ℝ) atTop (F_int 1 (↑a : ℝ ⧸ AddSubgroup.zmultiples 1)) fun (t : ℝ) ↦ rexp (-min p q * t)
⊢ ∃ (p : ℝ), 0 < p ∧ IsBigO (F := ℝ) atTop (F_int 1 (↑a : ℝ ⧸ AddSubgroup.zmultiples 1)) fun (t : ℝ) ↦ rexp (-p * t)

Tactic:
refine ⟨_, lt_min hp hq, ?_⟩
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
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)
h : ∀ (t : ℝ) (ht : 0 < t), F_int 1 (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t = F_nat 1 a t + F_nat 1 (1 - a) t
⊢ F_int 1 (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) =ᶠ[atTop] fun (t : ℝ) ↦ F_nat 1 a t + F_nat 1 (1 - a) t

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:
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)
t : ℝ
ht : 0 < t
⊢ F_int 1 (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t = F_nat 1 a t + F_nat 1 (1 - a) t

Tactic:
F_int_eq_of_mem_Icc 1 (Ico_subset_Icc_self ha) ht

Premises used: Set.Ico_subset_Icc_self, HurwitzKernelBounds.F_int_eq_of_mem_Icc, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
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)
t : ℝ
ht : 0 < t
⊢ F_int 1 (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t = F_nat 1 a t + F_nat 1 (1 - a) t

Tactic:
exact F_int_eq_of_mem_Icc 1 (Ico_subset_Icc_self ha) ht

Premises used: Set.Ico_subset_Icc_self, HurwitzKernelBounds.F_int_eq_of_mem_Icc, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
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

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
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
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)

Tactic:
this.isBigO.trans ((hp'.trans ?_).add (hq'.trans ?_))

Premises used: Filter.EventuallyEq.isBigO, Asymptotics.IsBigO.trans, Asymptotics.IsBigO.add
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
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)
refine_2 : IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ rexp (-q * 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)

Tactic:
refine this.isBigO.trans ((hp'.trans ?_).add (hq'.trans ?_))

Premises used: Filter.EventuallyEq.isBigO, Asymptotics.IsBigO.trans, Asymptotics.IsBigO.add
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
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 : min p q ≤ p
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ rexp (-p * t)) fun (t : ℝ) ↦ rexp (-min p q * t)

Tactic:
apply isBigO_exp_neg_mul_of_le

Premises used: HurwitzKernelBounds.isBigO_exp_neg_mul_of_le
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
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_2 : min p q ≤ q
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ rexp (-q * t)) fun (t : ℝ) ↦ rexp (-min p q * t)

Tactic:
apply isBigO_exp_neg_mul_of_le

Premises used: HurwitzKernelBounds.isBigO_exp_neg_mul_of_le
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
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
⊢ min p q ≤ p

Tactic:
min_le_left ..

Premises used: min_le_left
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
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
⊢ min p q ≤ q

Tactic:
min_le_right ..

Premises used: min_le_right
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
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
⊢ min p q ≤ p

Tactic:
exacts [min_le_left .., min_le_right ..]

Premises used: min_le_left, min_le_right
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
Goal:
τ : ℂ
⊢ ∀ (b : ℤ), cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑b : ℂ) 2 * τ) = jacobiTheta₂_term b 0 τ

Tactic:
simp [jacobiTheta₂_term]

Premises used: jacobiTheta₂_term
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
Goal:
τ : ℂ
simp_rw : jacobiTheta₂ 0 (2 + τ) = jacobiTheta₂ 0 τ
simp_rw₁ : jacobiTheta₂ 0 (τ + 2) = jacobiTheta₂ 0 τ
⊢ jacobiTheta (2 + τ) = jacobiTheta τ

Tactic:
simp_rw [jacobiTheta_eq_jacobiTheta₂, add_comm, jacobiTheta₂_add_right]

Premises used: add_comm, jacobiTheta_eq_jacobiTheta₂, jacobiTheta₂_add_right