-- Mathlib/NumberTheory/ModularForms/JacobiTheta/Bounds.lean
lemma isBigO_atTop_F_int_one (a : UnitAddCircle) : ∃ p, 0 < p ∧
    F_int 1 a =O[atTop] fun t ↦ exp (-p * t)

Proof state:
case intro.intro.intro.intro.intro.intro
a : ℝ
ha : a ∈ Ico 0 1
p : ℝ
hp : 0 < p
hp' : F_nat 1 a =O[atTop] fun t => rexp (-p * t)
q : ℝ
hq : 0 < q
hq' : F_nat 1 (1 - a) =O[atTop] fun t => rexp (-q * t)
⊢ F_int 1 ↑a =O[atTop] fun t => rexp (-(p ⊓ q) * 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

Result:
case intro.intro.intro.intro.intro.intro
a : ℝ
ha : a ∈ Ico 0 1
p : ℝ
hp : 0 < p
hp' : F_nat 1 a =O[atTop] fun t => rexp (-p * t)
q : ℝ
hq : 0 < q
hq' : F_nat 1 (1 - a) =O[atTop] fun t => rexp (-q * t)
this : F_int 1 ↑a =ᶠ[atTop] fun t => F_nat 1 a t + F_nat 1 (1 - a) t
⊢ F_int 1 ↑a =O[atTop] fun t => rexp (-(p ⊓ q) * t)

Proof state:
case h
a : ℝ
ha : a ∈ Ico 0 1
p : ℝ
hp : 0 < p
hp' : F_nat 1 a =O[atTop] fun t => rexp (-p * t)
q : ℝ
hq : 0 < q
hq' : F_nat 1 (1 - a) =O[atTop] fun t => rexp (-q * t)
t : ℝ
ht : 0 < t
⊢ F_int 1 (↑a) 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

Result:
no goals

Proof state:
case intro.intro
a : ℝ
ha : a ∈ Ico 0 1
⊢ ∃ p, 0 < p ∧ F_int 1 ↑a =O[atTop] fun t => rexp (-p * t)

Tactic:
obtain ⟨p, hp, hp'⟩ := isBigO_atTop_F_nat_one ha.1

Result:
case intro.intro.intro.intro
a : ℝ
ha : a ∈ Ico 0 1
p : ℝ
hp : 0 < p
hp' : F_nat 1 a =O[atTop] fun t => rexp (-p * t)
⊢ ∃ p, 0 < p ∧ F_int 1 ↑a =O[atTop] fun t => rexp (-p * t)

Proof state:
case intro.intro.intro.intro.intro.intro
a : ℝ
ha : a ∈ Ico 0 1
p : ℝ
hp : 0 < p
hp' : F_nat 1 a =O[atTop] fun t => rexp (-p * t)
q : ℝ
hq : 0 < q
hq' : F_nat 1 (1 - a) =O[atTop] fun t => rexp (-q * t)
this : F_int 1 ↑a =ᶠ[atTop] fun t => F_nat 1 a t + F_nat 1 (1 - a) t
⊢ F_int 1 ↑a =O[atTop] fun t => rexp (-(p ⊓ q) * t)

Tactic:
refine this.isBigO.trans ((hp'.trans ?_).add (hq'.trans ?_)) <;>
apply isBigO_exp_neg_mul_of_le

Result:
case intro.intro.intro.intro.intro.intro.refine_1.hcd
a : ℝ
ha : a ∈ Ico 0 1
p : ℝ
hp : 0 < p
hp' : F_nat 1 a =O[atTop] fun t => rexp (-p * t)
q : ℝ
hq : 0 < q
hq' : F_nat 1 (1 - a) =O[atTop] fun t => rexp (-q * t)
this : F_int 1 ↑a =ᶠ[atTop] fun t => F_nat 1 a t + F_nat 1 (1 - a) t
⊢ p ⊓ q ≤ p

case intro.intro.intro.intro.intro.intro.refine_2.hcd
a : ℝ
ha : a ∈ Ico 0 1
p : ℝ
hp : 0 < p
hp' : F_nat 1 a =O[atTop] fun t => rexp (-p * t)
q : ℝ
hq : 0 < q
hq' : F_nat 1 (1 - a) =O[atTop] fun t => rexp (-q * t)
this : F_int 1 ↑a =ᶠ[atTop] fun t => F_nat 1 a t + F_nat 1 (1 - a) t
⊢ p ⊓ q ≤ q

Proof state:
a : ℝ
ha : a ∈ Ico 0 1
p : ℝ
hp : 0 < p
hp' : F_nat 1 a =O[atTop] fun t => rexp (-p * t)
q : ℝ
hq : 0 < q
hq' : F_nat 1 (1 - a) =O[atTop] fun t => rexp (-q * t)
⊢ F_int 1 ↑a =ᶠ[atTop] fun t => F_nat 1 a t + F_nat 1 (1 - a) t

Tactic:
filter_upwards [eventually_gt_atTop 0] with t ht

Result:
case h
a : ℝ
ha : a ∈ Ico 0 1
p : ℝ
hp : 0 < p
hp' : F_nat 1 a =O[atTop] fun t => rexp (-p * t)
q : ℝ
hq : 0 < q
hq' : F_nat 1 (1 - a) =O[atTop] fun t => rexp (-q * t)
t : ℝ
ht : 0 < t
⊢ F_int 1 (↑a) t = F_nat 1 a t + F_nat 1 (1 - a) t

Proof state:
case intro.intro.intro.intro
a : ℝ
ha : a ∈ Ico 0 1
p : ℝ
hp : 0 < p
hp' : F_nat 1 a =O[atTop] fun t => rexp (-p * t)
⊢ ∃ p, 0 < p ∧ F_int 1 ↑a =O[atTop] fun t => rexp (-p * t)

Tactic:
obtain ⟨q, hq, hq'⟩ := isBigO_atTop_F_nat_one (sub_nonneg.mpr ha.2.le)

Result:
case intro.intro.intro.intro.intro.intro
a : ℝ
ha : a ∈ Ico 0 1
p : ℝ
hp : 0 < p
hp' : F_nat 1 a =O[atTop] fun t => rexp (-p * t)
q : ℝ
hq : 0 < q
hq' : F_nat 1 (1 - a) =O[atTop] fun t => rexp (-q * t)
⊢ ∃ p, 0 < p ∧ F_int 1 ↑a =O[atTop] fun t => rexp (-p * t)

Proof state:
a : UnitAddCircle
⊢ ∃ p, 0 < p ∧ F_int 1 a =O[atTop] fun t => rexp (-p * t)

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

Result:
case intro.intro
a : ℝ
ha : a ∈ Ico 0 1
⊢ ∃ p, 0 < p ∧ F_int 1 ↑a =O[atTop] fun t => rexp (-p * t)

Proof state:
case intro.intro.intro.intro.intro.intro.refine_1.hcd
a : ℝ
ha : a ∈ Ico 0 1
p : ℝ
hp : 0 < p
hp' : F_nat 1 a =O[atTop] fun t => rexp (-p * t)
q : ℝ
hq : 0 < q
hq' : F_nat 1 (1 - a) =O[atTop] fun t => rexp (-q * t)
this : F_int 1 ↑a =ᶠ[atTop] fun t => F_nat 1 a t + F_nat 1 (1 - a) t
⊢ p ⊓ q ≤ p

case intro.intro.intro.intro.intro.intro.refine_2.hcd
a : ℝ
ha : a ∈ Ico 0 1
p : ℝ
hp : 0 < p
hp' : F_nat 1 a =O[atTop] fun t => rexp (-p * t)
q : ℝ
hq : 0 < q
hq' : F_nat 1 (1 - a) =O[atTop] fun t => rexp (-q * t)
this : F_int 1 ↑a =ᶠ[atTop] fun t => F_nat 1 a t + F_nat 1 (1 - a) t
⊢ p ⊓ q ≤ q

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

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro
a : ℝ
ha : a ∈ Ico 0 1
p : ℝ
hp : 0 < p
hp' : F_nat 1 a =O[atTop] fun t => rexp (-p * t)
q : ℝ
hq : 0 < q
hq' : F_nat 1 (1 - a) =O[atTop] fun t => rexp (-q * t)
⊢ ∃ p, 0 < p ∧ F_int 1 ↑a =O[atTop] fun t => rexp (-p * t)

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

Result:
case intro.intro.intro.intro.intro.intro
a : ℝ
ha : a ∈ Ico 0 1
p : ℝ
hp : 0 < p
hp' : F_nat 1 a =O[atTop] fun t => rexp (-p * t)
q : ℝ
hq : 0 < q
hq' : F_nat 1 (1 - a) =O[atTop] fun t => rexp (-q * t)
⊢ F_int 1 ↑a =O[atTop] fun t => rexp (-(p ⊓ q) * t)