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

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

Tactic:
let ⟨p, hp, hp'⟩ := this

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

Proof state:
a : ℝ
ha : 0 ≤ a
⊢ (fun t => ((1 - rexp (-π * t)) ^ 2)⁻¹) =O[atTop] fun x => 1

Tactic:
simpa only [inv_pow, one_pow] using isBigO_one_aux.pow 2

Result:
no goals

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

Tactic:
exact F_nat_one_le ha ht

Result:
no goals

Proof state:
case inr.refine_2
a : ℝ
ha : 0 ≤ a
aux' : (fun t => ((1 - rexp (-π * t)) ^ 2)⁻¹) =O[atTop] fun x => 1
ha' : 0 < a
⊢ (fun t => a * (rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t)))) =O[atTop] fun t => rexp (-π * a ^ 2 * t)

Tactic:
apply IsBigO.const_mul_left

Result:
case inr.refine_2.h
a : ℝ
ha : 0 ≤ a
aux' : (fun t => ((1 - rexp (-π * t)) ^ 2)⁻¹) =O[atTop] fun x => 1
ha' : 0 < a
⊢ (fun x => rexp (-π * a ^ 2 * x) / (1 - rexp (-π * x))) =O[atTop] fun t => rexp (-π * a ^ 2 * t)

Proof state:
case inr.refine_2.h
a : ℝ
ha : 0 ≤ a
aux' : (fun t => ((1 - rexp (-π * t)) ^ 2)⁻¹) =O[atTop] fun x => 1
ha' : 0 < a
⊢ (fun x => rexp (-π * a ^ 2 * x) / (1 - rexp (-π * x))) =O[atTop] fun t => rexp (-π * a ^ 2 * t)

Tactic:
simpa only [mul_one] using (isBigO_refl _ _).mul isBigO_one_aux

Result:
no goals

Proof state:
case h
a : ℝ
ha : 0 ≤ a
aux' : (fun t => ((1 - rexp (-π * t)) ^ 2)⁻¹) =O[atTop] fun x => 1
ha' : 0 < a
t : ℝ
ht : 0 < t
⊢ ‖rexp (-π * (a ^ 2 + 1) * t)‖ ≤ rexp (-(π * a ^ 2) * t)

Tactic:
rw [norm_of_nonneg (exp_pos _).le, exp_le_exp]

Result:
case h
a : ℝ
ha : 0 ≤ a
aux' : (fun t => ((1 - rexp (-π * t)) ^ 2)⁻¹) =O[atTop] fun x => 1
ha' : 0 < a
t : ℝ
ht : 0 < t
⊢ -π * (a ^ 2 + 1) * t ≤ -(π * a ^ 2) * t

Proof state:
case inr.refine_1
a : ℝ
ha : 0 ≤ a
aux' : (fun t => ((1 - rexp (-π * t)) ^ 2)⁻¹) =O[atTop] fun x => 1
ha' : 0 < a
⊢ (fun t => rexp (-π * (a ^ 2 + 1) * t) / (1 - rexp (-π * t)) ^ 2) =O[atTop] fun t => rexp (-(π * a ^ 2) * t) * 1

Tactic:
refine (Eventually.isBigO ?_).mul aux'

Result:
case inr.refine_1
a : ℝ
ha : 0 ≤ a
aux' : (fun t => ((1 - rexp (-π * t)) ^ 2)⁻¹) =O[atTop] fun x => 1
ha' : 0 < a
⊢ ∀ᶠ (x : ℝ) in atTop, ‖rexp (-π * (a ^ 2 + 1) * x)‖ ≤ rexp (-(π * a ^ 2) * x)

Proof state:
case inr.refine_2
a : ℝ
ha : 0 ≤ a
aux' : (fun t => ((1 - rexp (-π * t)) ^ 2)⁻¹) =O[atTop] fun x => 1
ha' : 0 < a
⊢ (fun t => a * rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t))) =O[atTop] fun t => rexp (-(π * a ^ 2) * t)

Tactic:
simp_rw [mul_div_assoc, ← neg_mul]

Result:
case inr.refine_2
a : ℝ
ha : 0 ≤ a
aux' : (fun t => ((1 - rexp (-π * t)) ^ 2)⁻¹) =O[atTop] fun x => 1
ha' : 0 < a
⊢ (fun t => a * (rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t)))) =O[atTop] fun t => rexp (-π * a ^ 2 * t)

Proof state:
aux' : (fun t => ((1 - rexp (-π * t)) ^ 2)⁻¹) =O[atTop] fun x => 1
ha : 0 ≤ 0
⊢ (fun t =>
      rexp (-π * (0 ^ 2 + 1) * t) / (1 - rexp (-π * t)) ^ 2 + 0 * rexp (-π * 0 ^ 2 * t) / (1 - rexp (-π * t))) =O[atTop]
    fun t => rexp (-π * t)

Tactic:
simpa only [zero_pow two_ne_zero, zero_add, mul_one, zero_mul, zero_div,
add_zero] using (isBigO_refl _ _).mul aux'

Result:
no goals

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

Tactic:
suffices ∃ p, 0 < p ∧ (fun t ↦ rexp (-π * (a ^ 2 + 1) * t) / (1 - rexp (-π * t)) ^ 2
    + a * rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t))) =O[atTop] fun t ↦ exp (-p * t) by
  let ⟨p, hp, hp'⟩ := this
  refine ⟨p, hp, (Eventually.isBigO ?_).trans hp'⟩
  filter_upwards [eventually_gt_atTop 0] with t ht
  exact F_nat_one_le ha ht

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

Proof state:
a : ℝ
ha : 0 ≤ a
this :
  ∃ p,
    0 < p ∧
      (fun t =>
          rexp (-π * (a ^ 2 + 1) * t) / (1 - rexp (-π * t)) ^ 2 +
            a * rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t))) =O[atTop]
        fun t => rexp (-p * t)
p : ℝ
hp : 0 < p
hp' :
  (fun t =>
      rexp (-π * (a ^ 2 + 1) * t) / (1 - rexp (-π * t)) ^ 2 + a * rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t))) =O[atTop]
    fun t => rexp (-p * t)
⊢ ∀ᶠ (x : ℝ) in atTop,
    ‖F_nat 1 a x‖ ≤
      rexp (-π * (a ^ 2 + 1) * x) / (1 - rexp (-π * x)) ^ 2 + a * rexp (-π * a ^ 2 * x) / (1 - rexp (-π * x))

Tactic:
filter_upwards [eventually_gt_atTop 0] with t ht

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

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

Tactic:
refine ⟨p, hp, (Eventually.isBigO ?_).trans hp'⟩

Result:
a : ℝ
ha : 0 ≤ a
this :
  ∃ p,
    0 < p ∧
      (fun t =>
          rexp (-π * (a ^ 2 + 1) * t) / (1 - rexp (-π * t)) ^ 2 +
            a * rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t))) =O[atTop]
        fun t => rexp (-p * t)
p : ℝ
hp : 0 < p
hp' :
  (fun t =>
      rexp (-π * (a ^ 2 + 1) * t) / (1 - rexp (-π * t)) ^ 2 + a * rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t))) =O[atTop]
    fun t => rexp (-p * t)
⊢ ∀ᶠ (x : ℝ) in atTop,
    ‖F_nat 1 a x‖ ≤
      rexp (-π * (a ^ 2 + 1) * x) / (1 - rexp (-π * x)) ^ 2 + a * rexp (-π * a ^ 2 * x) / (1 - rexp (-π * x))