-- Mathlib/NumberTheory/ModularForms/JacobiTheta/Bounds.lean
lemma isBigO_atTop_F_nat_zero_sub {a : ℝ} (ha : 0 ≤ a) : ∃ p, 0 < p ∧
    (fun t ↦ F_nat 0 a t - (if a = 0 then 1 else 0)) =O[atTop] fun t ↦ exp (-p * t)

Proof state:
a : ℝ
ha : 0 ≤ a
h : ¬a = 0
⊢ (fun t => F_nat 0 a t) =O[atTop] fun t => rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t))

Tactic:
apply Eventually.isBigO

Result:
case hfg
a : ℝ
ha : 0 ≤ a
h : ¬a = 0
⊢ ∀ᶠ (x : ℝ) in atTop, ‖F_nat 0 a x‖ ≤ rexp (-π * a ^ 2 * x) / (1 - rexp (-π * x))

Proof state:
case neg
a : ℝ
ha : 0 ≤ a
h : ¬a = 0
this : (fun t => F_nat 0 a t) =O[atTop] fun t => rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t))
⊢ (fun t => rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t))) =O[atTop] fun t => rexp (-(π * a ^ 2) * t)

Tactic:
simpa only [neg_mul π (a ^ 2), mul_one] using (isBigO_refl _ _).mul isBigO_one_aux

Result:
no goals

Proof state:
case neg
a : ℝ
ha : 0 ≤ a
h : ¬a = 0
⊢ ∃ p, 0 < p ∧ (fun t => F_nat 0 a t - 0) =O[atTop] fun t => rexp (-p * t)

Tactic:
simp_rw [sub_zero]

Result:
case neg
a : ℝ
ha : 0 ≤ a
h : ¬a = 0
⊢ ∃ p, 0 < p ∧ (fun t => F_nat 0 a t) =O[atTop] fun t => rexp (-p * t)

Proof state:
case neg
a : ℝ
ha : 0 ≤ a
h : ¬a = 0
⊢ ∃ p, 0 < p ∧ (fun t => F_nat 0 a t) =O[atTop] fun t => rexp (-p * t)

Tactic:
have : (fun t ↦ F_nat 0 a t) =O[atTop] fun t ↦ rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t)) := by
  apply Eventually.isBigO
  filter_upwards [eventually_gt_atTop 0] with t ht
  exact F_nat_zero_le ha ht

Result:
case neg
a : ℝ
ha : 0 ≤ a
h : ¬a = 0
this : (fun t => F_nat 0 a t) =O[atTop] fun t => rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t))
⊢ ∃ p, 0 < p ∧ (fun t => F_nat 0 a t) =O[atTop] fun t => rexp (-p * t)

Proof state:
case hfg
a : ℝ
ha : 0 ≤ a
h : ¬a = 0
⊢ ∀ᶠ (x : ℝ) in atTop, ‖F_nat 0 a x‖ ≤ rexp (-π * a ^ 2 * x) / (1 - rexp (-π * x))

Tactic:
filter_upwards [eventually_gt_atTop 0] with t ht

Result:
case h
a : ℝ
ha : 0 ≤ a
h : ¬a = 0
t : ℝ
ht : 0 < t
⊢ ‖F_nat 0 a t‖ ≤ rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t))

Proof state:
case hfg
a : ℝ
ha : 0 ≤ a
h : a = 0
⊢ ∀ᶠ (x : ℝ) in atTop, ‖F_nat 0 0 x - 1‖ ≤ rexp (-π * x) / (1 - rexp (-π * x))

Tactic:
filter_upwards [eventually_gt_atTop 0] with t ht

Result:
case h
a : ℝ
ha : 0 ≤ a
h : a = 0
t : ℝ
ht : 0 < t
⊢ ‖F_nat 0 0 t - 1‖ ≤ rexp (-π * t) / (1 - rexp (-π * t))

Proof state:
case h
a : ℝ
ha : 0 ≤ a
h : a = 0
t : ℝ
ht : 0 < t
⊢ ‖F_nat 0 0 t - 1‖ ≤ rexp (-π * t) / (1 - rexp (-π * t))

Tactic:
exact F_nat_zero_zero_sub_le ht

Result:
no goals

Proof state:
case pos
a : ℝ
ha : 0 ≤ a
h : a = 0
⊢ ∃ p, 0 < p ∧ (fun t => F_nat 0 0 t - 1) =O[atTop] fun t => rexp (-p * t)

Tactic:
have : (fun t ↦ F_nat 0 0 t - 1) =O[atTop] fun t ↦ rexp (-π * t) / (1 - rexp (-π * t)) := by
  apply Eventually.isBigO
  filter_upwards [eventually_gt_atTop 0] with t ht
  exact F_nat_zero_zero_sub_le ht

Result:
case pos
a : ℝ
ha : 0 ≤ a
h : a = 0
this : (fun t => F_nat 0 0 t - 1) =O[atTop] fun t => rexp (-π * t) / (1 - rexp (-π * t))
⊢ ∃ p, 0 < p ∧ (fun t => F_nat 0 0 t - 1) =O[atTop] fun t => rexp (-p * t)

Proof state:
a : ℝ
ha : 0 ≤ a
⊢ ∃ p, 0 < p ∧ (fun t => F_nat 0 a t - if a = 0 then 1 else 0) =O[atTop] fun t => rexp (-p * t)

Tactic:
split_ifs with h

Result:
case pos
a : ℝ
ha : 0 ≤ a
h : a = 0
⊢ ∃ p, 0 < p ∧ (fun t => F_nat 0 a t - 1) =O[atTop] fun t => rexp (-p * t)

case neg
a : ℝ
ha : 0 ≤ a
h : ¬a = 0
⊢ ∃ p, 0 < p ∧ (fun t => F_nat 0 a t - 0) =O[atTop] fun t => rexp (-p * t)

Proof state:
case pos
a : ℝ
ha : 0 ≤ a
h : a = 0
⊢ ∃ p, 0 < p ∧ (fun t => F_nat 0 a t - 1) =O[atTop] fun t => rexp (-p * t)

Tactic:
rw [h]

Result:
case pos
a : ℝ
ha : 0 ≤ a
h : a = 0
⊢ ∃ p, 0 < p ∧ (fun t => F_nat 0 0 t - 1) =O[atTop] fun t => rexp (-p * t)

Proof state:
a : ℝ
ha : 0 ≤ a
h : a = 0
⊢ (fun t => F_nat 0 0 t - 1) =O[atTop] fun t => rexp (-π * t) / (1 - rexp (-π * t))

Tactic:
apply Eventually.isBigO

Result:
case hfg
a : ℝ
ha : 0 ≤ a
h : a = 0
⊢ ∀ᶠ (x : ℝ) in atTop, ‖F_nat 0 0 x - 1‖ ≤ rexp (-π * x) / (1 - rexp (-π * x))

Proof state:
case pos
a : ℝ
ha : 0 ≤ a
h : a = 0
this : (fun t => F_nat 0 0 t - 1) =O[atTop] fun t => rexp (-π * t) / (1 - rexp (-π * t))
⊢ (fun t => rexp (-π * t) / (1 - rexp (-π * t))) =O[atTop] fun t => rexp (-π * t)

Tactic:
simpa using (isBigO_refl (fun t ↦ rexp (-π * t)) _).mul isBigO_one_aux

Result:
no goals

Proof state:
case pos
a : ℝ
ha : 0 ≤ a
h : a = 0
this : (fun t => F_nat 0 0 t - 1) =O[atTop] fun t => rexp (-π * t) / (1 - rexp (-π * t))
⊢ ∃ p, 0 < p ∧ (fun t => F_nat 0 0 t - 1) =O[atTop] fun t => rexp (-p * t)

Tactic:
refine ⟨_, pi_pos, this.trans ?_⟩

Result:
case pos
a : ℝ
ha : 0 ≤ a
h : a = 0
this : (fun t => F_nat 0 0 t - 1) =O[atTop] fun t => rexp (-π * t) / (1 - rexp (-π * t))
⊢ (fun t => rexp (-π * t) / (1 - rexp (-π * t))) =O[atTop] fun t => rexp (-π * t)

Proof state:
case neg
a : ℝ
ha : 0 ≤ a
h : ¬a = 0
this : (fun t => F_nat 0 a t) =O[atTop] fun t => rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t))
⊢ ∃ p, 0 < p ∧ (fun t => F_nat 0 a t) =O[atTop] fun t => rexp (-p * t)

Tactic:
refine ⟨π * a ^ 2, mul_pos pi_pos (sq_pos_of_ne_zero h), this.trans ?_⟩

Result:
case neg
a : ℝ
ha : 0 ≤ a
h : ¬a = 0
this : (fun t => F_nat 0 a t) =O[atTop] fun t => rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t))
⊢ (fun t => rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t))) =O[atTop] fun t => rexp (-(π * a ^ 2) * t)

Proof state:
case h
a : ℝ
ha : 0 ≤ a
h : ¬a = 0
t : ℝ
ht : 0 < t
⊢ ‖F_nat 0 a t‖ ≤ rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t))

Tactic:
exact F_nat_zero_le ha ht

Result:
no goals