-- Mathlib/Combinatorics/Extremal/RuzsaSzemeredi.lean
theorem ruzsaSzemerediNumberNat_asymptotic_lower_bound :
   (fun n ↦ n ^ 2 * exp (-4 * sqrt (log n)) : ℕ → ℝ) =O[atTop]
     fun n ↦ (ruzsaSzemerediNumberNat n : ℝ)

Proof state:
x : ℕ
hx : x ≥ 15
⊢ ↑x ≤ 12 * ↑((x - 3) / 6)

Tactic:
norm_cast

Result:
x : ℕ
hx : x ≥ 15
⊢ x ≤ 12 * ((x - 3) / 6)

Proof state:
case refine_2

⊢ Nat.cast =O[atTop] fun n => ↑((n - 3) / 6)

Tactic:
rw [IsBigO_def]

Result:
case refine_2

⊢ ∃ c, IsBigOWith c atTop Nat.cast fun n => ↑((n - 3) / 6)

Proof state:
n : ℕ
hn : 6 ≤ ↑n
⊢ 0 ≤ ↑n / 3 - 2

Tactic:
linarith

Result:
no goals

Proof state:
⊢ (fun n => ↑n * ↑n * rexp (-4 * √(Real.log ↑n))) =O[atTop] fun n =>
    (↑n / 3 - 2) * ↑((n - 3) / 6) * rexp (-4 * √(Real.log ↑((n - 3) / 6)))

Tactic:
refine (IsBigO.mul ?_ ?_).mul ?_

Result:
case refine_1

⊢ Nat.cast =O[atTop] fun n => ↑n / 3 - 2

case refine_2

⊢ Nat.cast =O[atTop] fun n => ↑((n - 3) / 6)

case refine_3

⊢ (fun n => rexp (-4 * √(Real.log ↑n))) =O[atTop] fun n => rexp (-4 * √(Real.log ↑((n - 3) / 6)))

Proof state:
x : ℕ
hx : x ≥ 15
⊢ x ≤ 12 * ((x - 3) / 6)

Tactic:
omega

Result:
no goals

Proof state:
case refine_2

⊢ ∃ c, IsBigOWith c atTop Nat.cast fun n => ↑((n - 3) / 6)

Tactic:
refine ⟨12, ?_⟩

Result:
case refine_2

⊢ IsBigOWith 12 atTop Nat.cast fun n => ↑((n - 3) / 6)

Proof state:
⊢ (fun n => ↑n ^ 2 * rexp (-4 * √(Real.log ↑n))) =O[atTop] fun n =>
    (↑n / 3 - 2) * ↑((n - 3) / 6) * rexp (-4 * √(Real.log ↑((n - 3) / 6)))

Tactic:
simp_rw [sq]

Result:
⊢ (fun n => ↑n * ↑n * rexp (-4 * √(Real.log ↑n))) =O[atTop] fun n =>
    (↑n / 3 - 2) * ↑((n - 3) / 6) * rexp (-4 * √(Real.log ↑((n - 3) / 6)))

Proof state:
⊢ (fun n => 2) =o[atTop] fun n => ↑n / 3

Tactic:
simpa [div_eq_inv_mul, Function.comp_def] using
  .atTop_of_const_mul₀ zero_lt_three (by simp [tendsto_natCast_atTop_atTop])

Result:
no goals

Proof state:
case h
n : ℕ
hn : 6 ≤ n
this : 0 ≤ ↑n / 3 - 2
⊢ ‖(↑n / 3 - 2) * ↑((n - 3) / 6) * rexp (-4 * √(Real.log ↑((n - 3) / 6)))‖ ≤ ↑(ruzsaSzemerediNumberNat n)

Tactic:
simpa [neg_mul, abs_mul, abs_of_nonneg this] using ruzsaSzemerediNumberNat_lower_bound n

Result:
no goals

Proof state:
⊢ Nat.cast =O[atTop] fun n => ↑n / 3

Tactic:
simp_rw [div_eq_inv_mul]

Result:
⊢ Nat.cast =O[atTop] fun n => 3⁻¹ * ↑n

Proof state:
⊢ Nat.cast =O[atTop] fun n => 3⁻¹ * ↑n

Tactic:
exact (isBigO_refl ..).const_mul_right (by norm_num)

Result:
no goals

Proof state:
⊢ (fun n => ↑n ^ 2 * rexp (-4 * √(Real.log ↑n))) =O[atTop] fun n => ↑(ruzsaSzemerediNumberNat n)

Tactic:
trans fun n ↦ (n / 3 - 2) * ↑((n - 3) / 6) * exp (-4 * sqrt (log ↑((n - 3) / 6)))

Result:
⊢ (fun n => ↑n ^ 2 * rexp (-4 * √(Real.log ↑n))) =O[atTop] fun n =>
    (↑n / 3 - 2) * ↑((n - 3) / 6) * rexp (-4 * √(Real.log ↑((n - 3) / 6)))


⊢ (fun n => (↑n / 3 - 2) * ↑((n - 3) / 6) * rexp (-4 * √(Real.log ↑((n - 3) / 6)))) =O[atTop] fun n =>
    ↑(ruzsaSzemerediNumberNat n)

Proof state:
case refine_2

⊢ IsBigOWith 12 atTop Nat.cast fun n => ↑((n - 3) / 6)

Tactic:
simp only [IsBigOWith, norm_natCast, eventually_atTop]

Result:
case refine_2

⊢ ∃ a, ∀ b ≥ a, ↑b ≤ 12 * ↑((b - 3) / 6)

Proof state:
n : ℕ
hn : 6 ≤ n
⊢ 0 ≤ ↑n / 3 - 2

Tactic:
rify at hn

Result:
n : ℕ
hn : 6 ≤ ↑n
⊢ 0 ≤ ↑n / 3 - 2

Proof state:
case h
n : ℕ
hn : 6 ≤ n
⊢ ‖(↑n / 3 - 2) * ↑((n - 3) / 6) * rexp (-4 * √(Real.log ↑((n - 3) / 6)))‖ ≤ ↑(ruzsaSzemerediNumberNat n)

Tactic:
have : (0 : ℝ) ≤ n / 3 - 2 := by rify at hn; linarith

Result:
case h
n : ℕ
hn : 6 ≤ n
this : 0 ≤ ↑n / 3 - 2
⊢ ‖(↑n / 3 - 2) * ↑((n - 3) / 6) * rexp (-4 * √(Real.log ↑((n - 3) / 6)))‖ ≤ ↑(ruzsaSzemerediNumberNat n)

Proof state:
⊢ (fun n => (↑n / 3 - 2) * ↑((n - 3) / 6) * rexp (-4 * √(Real.log ↑((n - 3) / 6)))) =O[atTop] fun n =>
    ↑(ruzsaSzemerediNumberNat n)

Tactic:
refine .of_norm_eventuallyLE ?_

Result:
⊢ (fun x => ‖(↑x / 3 - 2) * ↑((x - 3) / 6) * rexp (-4 * √(Real.log ↑((x - 3) / 6)))‖) ≤ᶠ[atTop] fun n =>
    ↑(ruzsaSzemerediNumberNat n)

Proof state:
case refine_3

⊢ IsBoundedUnder (fun x1 x2 => x1 ≤ x2) atTop
    ((fun n => -4 * √(Real.log ↑n)) - fun n => -4 * √(Real.log ↑((n - 3) / 6)))

Tactic:
refine ⟨0, ?_⟩

Result:
case refine_3

⊢ ∀ᶠ (x : ℝ) in Filter.map ((fun n => -4 * √(Real.log ↑n)) - fun n => -4 * √(Real.log ↑((n - 3) / 6))) atTop,
    (fun x1 x2 => x1 ≤ x2) x 0

Proof state:
case refine_3

⊢ ∃ a, ∀ b ≥ a, √(Real.log ↑((b - 3) / 6)) ≤ √(Real.log ↑b)

Tactic:
refine ⟨9, fun x hx ↦ ?_⟩

Result:
case refine_3
x : ℕ
hx : x ≥ 9
⊢ √(Real.log ↑((x - 3) / 6)) ≤ √(Real.log ↑x)

Proof state:
case refine_2

⊢ ∃ a, ∀ b ≥ a, ↑b ≤ 12 * ↑((b - 3) / 6)

Tactic:
exact ⟨15, fun x hx ↦ by norm_cast; omega⟩

Result:
no goals

Proof state:
case refine_3.h.hx
x : ℕ
hx : x ≥ 9
⊢ 0 < ↑((x - 3) / 6)

Tactic:
simp

Result:
case refine_3.h.hx
x : ℕ
hx : x ≥ 9
⊢ 6 ≤ x - 3

Proof state:
case refine_3.h.hxy.h
x : ℕ
hx : x ≥ 9
⊢ (x - 3) / 6 ≤ x

Tactic:
omega

Result:
no goals

Proof state:
⊢ 3⁻¹ ≠ 0

Tactic:
norm_num

Result:
no goals

Proof state:
case refine_3
x : ℕ
hx : x ≥ 9
⊢ √(Real.log ↑((x - 3) / 6)) ≤ √(Real.log ↑x)

Tactic:
gcongr

Result:
case refine_3.h.hx
x : ℕ
hx : x ≥ 9
⊢ 0 < ↑((x - 3) / 6)

case refine_3.h.hxy.h
x : ℕ
hx : x ≥ 9
⊢ (x - 3) / 6 ≤ x

Proof state:
case refine_1

⊢ Nat.cast =O[atTop] fun n => ↑n / 3 - 2

Tactic:
trans fun n ↦ n / 3

Result:
⊢ Nat.cast =O[atTop] fun n => ↑n / 3


⊢ (fun n => ↑n / 3) =O[atTop] fun n => ↑n / 3 - 2

Proof state:
⊢ Tendsto (fun x => 3 * (3⁻¹ * ↑x)) atTop atTop

Tactic:
simp [tendsto_natCast_atTop_atTop]

Result:
no goals

Proof state:
case refine_3.h.hx
x : ℕ
hx : x ≥ 9
⊢ 6 ≤ x - 3

Tactic:
omega

Result:
no goals

Proof state:
⊢ (fun n => ↑n / 3) =O[atTop] fun n => ↑n / 3 - 2

Tactic:
refine IsLittleO.right_isBigO_sub ?_

Result:
⊢ (fun n => 2) =o[atTop] fun n => ↑n / 3

Proof state:
case refine_3

⊢ (fun n => rexp (-4 * √(Real.log ↑n))) =O[atTop] fun n => rexp (-4 * √(Real.log ↑((n - 3) / 6)))

Tactic:
rw [isBigO_exp_comp_exp_comp]

Result:
case refine_3

⊢ IsBoundedUnder (fun x1 x2 => x1 ≤ x2) atTop
    ((fun n => -4 * √(Real.log ↑n)) - fun n => -4 * √(Real.log ↑((n - 3) / 6)))

Proof state:
⊢ (fun x => ‖(↑x / 3 - 2) * ↑((x - 3) / 6) * rexp (-4 * √(Real.log ↑((x - 3) / 6)))‖) ≤ᶠ[atTop] fun n =>
    ↑(ruzsaSzemerediNumberNat n)

Tactic:
filter_upwards [eventually_ge_atTop 6] with n hn

Result:
case h
n : ℕ
hn : 6 ≤ n
⊢ ‖(↑n / 3 - 2) * ↑((n - 3) / 6) * rexp (-4 * √(Real.log ↑((n - 3) / 6)))‖ ≤ ↑(ruzsaSzemerediNumberNat n)

Proof state:
case refine_3

⊢ ∀ᶠ (x : ℝ) in Filter.map ((fun n => -4 * √(Real.log ↑n)) - fun n => -4 * √(Real.log ↑((n - 3) / 6))) atTop,
    (fun x1 x2 => x1 ≤ x2) x 0

Tactic:
simp only [neg_mul, eventually_map, Pi.sub_apply, sub_neg_eq_add, neg_add_le_iff_le_add,
  add_zero, ofNat_pos, _root_.mul_le_mul_left, eventually_atTop]

Result:
case refine_3

⊢ ∃ a, ∀ b ≥ a, √(Real.log ↑((b - 3) / 6)) ≤ √(Real.log ↑b)