Imports
/-
Copyright (c) 2026 Google LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
-/
module
public import Mathlib.Analysis.Complex.ExponentialBounds
public import Mathlib.Analysis.Real.Pi.Bounds
public import Mathlib.NumberTheory.Chebyshev
public import Mathlib.NumberTheory.LSeries.RiemannZeta
Large-x Real-Analytic Inequality (x ≥ 5000) for Explicit Chebyshev ψ Bound
This standalone file proves explicit_rhs_le_seven_eighths_of_five_thousand_le, showing that
for all x ≥ 5000, the explicit upper bound from
abs_psi_sub_self_le_weighted_riemannVonMangoldt_six_neg_one_fourth with parameters:
a_rvM = 16 / 5, C = 11 / 5, D = 0, A = 1, B = 85,
h = (7 / 20) * Real.sqrt x * (Real.log x) ^ 2,
T = (3 / 2) * Real.sqrt x / Real.log x,
satisfies the side conditions 1 ≤ x - h, 0 < h, 6 ≤ T and is bounded above by
(7 / 8) * Real.sqrt x * (Real.log x) ^ 2.
@[expose] public sectionopen Realnamespace ConjectureMachines.Semantics.Riemann.ExplicitLarge
For x ≥ 5000, 851 / 100 ≤ Real.log x (via 2 ^ 86 ≤ 5000 ^ 7).
lemma log_ge_851_div_100 {x : ℝ} (hx : 5000 ≤ x) :
(851 / 100 : ℝ) ≤ Real.log x := x:ℝhx:5000 ≤ x⊢ 851 / 100 ≤ log x
x:ℝhx:5000 ≤ xhpow:2 ^ 86 ≤ x ^ 7⊢ 851 / 100 ≤ log x
have hlog : Real.log ((2 : ℝ) ^ (86 : ℕ)) ≤ Real.log (x ^ (7 : ℕ)) :=
Real.log_le_log (by x:ℝhx:5000 ≤ xhpow:2 ^ 86 ≤ x ^ 7⊢ 0 < 2 ^ 86 positivity All goals completed! 🐙) hpow x:ℝhx:5000 ≤ xhpow:2 ^ 86 ≤ x ^ 7hlog:log (2 ^ 86) ≤ log (x ^ 7)⊢ 851 / 100 ≤ log x
rw [Real.log_pow, x:ℝhx:5000 ≤ xhpow:2 ^ 86 ≤ x ^ 7hlog:↑86 * log 2 ≤ log (x ^ 7)⊢ 851 / 100 ≤ log x Real.log_pow x:ℝhx:5000 ≤ xhpow:2 ^ 86 ≤ x ^ 7hlog:↑86 * log 2 ≤ ↑7 * log x⊢ 851 / 100 ≤ log x] at hlog x:ℝhx:5000 ≤ xhpow:2 ^ 86 ≤ x ^ 7hlog:↑86 * log 2 ≤ ↑7 * log x⊢ 851 / 100 ≤ log x
have hlog2 := Real.log_two_gt_d9 x:ℝhx:5000 ≤ xhpow:2 ^ 86 ≤ x ^ 7hlog:↑86 * log 2 ≤ ↑7 * log xhlog2:0.6931471803 < log 2⊢ 851 / 100 ≤ log x
push_cast at hlog x:ℝhx:5000 ≤ xhpow:2 ^ 86 ≤ x ^ 7hlog:86 * log 2 ≤ 7 * log xhlog2:0.6931471803 < log 2⊢ 851 / 100 ≤ log x
linarith All goals completed! 🐙
For x ≥ 5000, 70 ≤ Real.sqrt x.
lemma sqrt_ge_seventy {x : ℝ} (hx : 5000 ≤ x) :
(70 : ℝ) ≤ Real.sqrt x := by x:ℝhx:5000 ≤ x⊢ 70 ≤ √x
have h70 : (70 : ℝ) ^ 2 ≤ x := by norm_num x:ℝhx:5000 ≤ x⊢ 4900 ≤ x; linarith x:ℝhx:5000 ≤ xh70:70 ^ 2 ≤ x⊢ 70 ≤ √x
have hsqrt := Real.sqrt_le_sqrt h70 x:ℝhx:5000 ≤ xh70:70 ^ 2 ≤ xhsqrt:√(70 ^ 2) ≤ √x⊢ 70 ≤ √x
rwa [Real.sqrt_sq (by x:ℝhx:5000 ≤ xh70:70 ^ 2 ≤ xhsqrt:√(70 ^ 2) ≤ √x⊢ 0 ≤ 70 norm_num All goals completed! 🐙)] at hsqrt
For v ≥ 851 / 400, (39 / 10) * v ≤ Real.exp v via the degree-6 Taylor lower bound.
lemma exp_ge_thirty_nine_tenths_mul {v : ℝ} (hv : (851 / 400 : ℝ) ≤ v) :
(39 / 10 : ℝ) * v ≤ Real.exp v := by v:ℝhv:851 / 400 ≤ v⊢ 39 / 10 * v ≤ rexp v
have hv_nonneg : 0 ≤ v := by linarith v:ℝhv:851 / 400 ≤ vhv_nonneg:0 ≤ v⊢ 39 / 10 * v ≤ rexp v
have h_sum := Real.sum_le_exp_of_nonneg hv_nonneg 7 v:ℝhv:851 / 400 ≤ vhv_nonneg:0 ≤ vh_sum:∑ i ∈ Finset.range 7, v ^ i / ↑i.factorial ≤ rexp v⊢ 39 / 10 * v ≤ rexp v
simp only [Finset.sum_range_succ, Finset.range_zero, Finset.sum_empty, Nat.factorial,
Nat.cast_one, Nat.cast_mul, pow_zero, pow_one, zero_add] at h_sum v:ℝhv:851 / 400 ≤ vhv_nonneg:0 ≤ vh_sum:1 / 1 + v / (1 * 1) + v ^ 2 / (↑(Nat.succ 1) * (1 * 1)) + v ^ 3 / (↑(Nat.succ 2) * (↑(Nat.succ 1) * (1 * 1))) +
v ^ 4 / (↑(Nat.succ 3) * (↑(Nat.succ 2) * (↑(Nat.succ 1) * (1 * 1)))) +
v ^ 5 / (↑(Nat.succ 4) * (↑(Nat.succ 3) * (↑(Nat.succ 2) * (↑(Nat.succ 1) * (1 * 1))))) +
v ^ 6 / (↑(Nat.succ 5) * (↑(Nat.succ 4) * (↑(Nat.succ 3) * (↑(Nat.succ 2) * (↑(Nat.succ 1) * (1 * 1)))))) ≤
rexp v⊢ 39 / 10 * v ≤ rexp v
have h_amgm : 0 ≤ (v / 2 - 1) ^ 2 := sq_nonneg (v / 2 - 1) v:ℝhv:851 / 400 ≤ vhv_nonneg:0 ≤ vh_sum:1 / 1 + v / (1 * 1) + v ^ 2 / (↑(Nat.succ 1) * (1 * 1)) + v ^ 3 / (↑(Nat.succ 2) * (↑(Nat.succ 1) * (1 * 1))) +
v ^ 4 / (↑(Nat.succ 3) * (↑(Nat.succ 2) * (↑(Nat.succ 1) * (1 * 1)))) +
v ^ 5 / (↑(Nat.succ 4) * (↑(Nat.succ 3) * (↑(Nat.succ 2) * (↑(Nat.succ 1) * (1 * 1))))) +
v ^ 6 / (↑(Nat.succ 5) * (↑(Nat.succ 4) * (↑(Nat.succ 3) * (↑(Nat.succ 2) * (↑(Nat.succ 1) * (1 * 1)))))) ≤
rexp vh_amgm:0 ≤ (v / 2 - 1) ^ 2⊢ 39 / 10 * v ≤ rexp v
have h_v2 : (851 / 400 : ℝ) ^ 2 ≤ v ^ 2 := pow_le_pow_left₀ (by v:ℝhv:851 / 400 ≤ vhv_nonneg:0 ≤ vh_sum:1 / 1 + v / (1 * 1) + v ^ 2 / (↑(Nat.succ 1) * (1 * 1)) + v ^ 3 / (↑(Nat.succ 2) * (↑(Nat.succ 1) * (1 * 1))) +
v ^ 4 / (↑(Nat.succ 3) * (↑(Nat.succ 2) * (↑(Nat.succ 1) * (1 * 1)))) +
v ^ 5 / (↑(Nat.succ 4) * (↑(Nat.succ 3) * (↑(Nat.succ 2) * (↑(Nat.succ 1) * (1 * 1))))) +
v ^ 6 / (↑(Nat.succ 5) * (↑(Nat.succ 4) * (↑(Nat.succ 3) * (↑(Nat.succ 2) * (↑(Nat.succ 1) * (1 * 1)))))) ≤
rexp vh_amgm:0 ≤ (v / 2 - 1) ^ 2⊢ 0 ≤ 851 / 400 norm_num All goals completed! 🐙) hv 2 v:ℝhv:851 / 400 ≤ vhv_nonneg:0 ≤ vh_sum:1 / 1 + v / (1 * 1) + v ^ 2 / (↑(Nat.succ 1) * (1 * 1)) + v ^ 3 / (↑(Nat.succ 2) * (↑(Nat.succ 1) * (1 * 1))) +
v ^ 4 / (↑(Nat.succ 3) * (↑(Nat.succ 2) * (↑(Nat.succ 1) * (1 * 1)))) +
v ^ 5 / (↑(Nat.succ 4) * (↑(Nat.succ 3) * (↑(Nat.succ 2) * (↑(Nat.succ 1) * (1 * 1))))) +
v ^ 6 / (↑(Nat.succ 5) * (↑(Nat.succ 4) * (↑(Nat.succ 3) * (↑(Nat.succ 2) * (↑(Nat.succ 1) * (1 * 1)))))) ≤
rexp vh_amgm:0 ≤ (v / 2 - 1) ^ 2h_v2:(851 / 400) ^ 2 ≤ v ^ 2⊢ 39 / 10 * v ≤ rexp v
have h_v3 : (851 / 400 : ℝ) ^ 3 ≤ v ^ 3 := pow_le_pow_left₀ (by v:ℝhv:851 / 400 ≤ vhv_nonneg:0 ≤ vh_sum:1 / 1 + v / (1 * 1) + v ^ 2 / (↑(Nat.succ 1) * (1 * 1)) + v ^ 3 / (↑(Nat.succ 2) * (↑(Nat.succ 1) * (1 * 1))) +
v ^ 4 / (↑(Nat.succ 3) * (↑(Nat.succ 2) * (↑(Nat.succ 1) * (1 * 1)))) +
v ^ 5 / (↑(Nat.succ 4) * (↑(Nat.succ 3) * (↑(Nat.succ 2) * (↑(Nat.succ 1) * (1 * 1))))) +
v ^ 6 / (↑(Nat.succ 5) * (↑(Nat.succ 4) * (↑(Nat.succ 3) * (↑(Nat.succ 2) * (↑(Nat.succ 1) * (1 * 1)))))) ≤
rexp vh_amgm:0 ≤ (v / 2 - 1) ^ 2h_v2:(851 / 400) ^ 2 ≤ v ^ 2⊢ 0 ≤ 851 / 400 norm_num All goals completed! 🐙) hv 3 v:ℝhv:851 / 400 ≤ vhv_nonneg:0 ≤ vh_sum:1 / 1 + v / (1 * 1) + v ^ 2 / (↑(Nat.succ 1) * (1 * 1)) + v ^ 3 / (↑(Nat.succ 2) * (↑(Nat.succ 1) * (1 * 1))) +
v ^ 4 / (↑(Nat.succ 3) * (↑(Nat.succ 2) * (↑(Nat.succ 1) * (1 * 1)))) +
v ^ 5 / (↑(Nat.succ 4) * (↑(Nat.succ 3) * (↑(Nat.succ 2) * (↑(Nat.succ 1) * (1 * 1))))) +
v ^ 6 / (↑(Nat.succ 5) * (↑(Nat.succ 4) * (↑(Nat.succ 3) * (↑(Nat.succ 2) * (↑(Nat.succ 1) * (1 * 1)))))) ≤
rexp vh_amgm:0 ≤ (v / 2 - 1) ^ 2h_v2:(851 / 400) ^ 2 ≤ v ^ 2h_v3:(851 / 400) ^ 3 ≤ v ^ 3⊢ 39 / 10 * v ≤ rexp v
have h_v4 : (851 / 400 : ℝ) ^ 4 ≤ v ^ 4 := pow_le_pow_left₀ (by v:ℝhv:851 / 400 ≤ vhv_nonneg:0 ≤ vh_sum:1 / 1 + v / (1 * 1) + v ^ 2 / (↑(Nat.succ 1) * (1 * 1)) + v ^ 3 / (↑(Nat.succ 2) * (↑(Nat.succ 1) * (1 * 1))) +
v ^ 4 / (↑(Nat.succ 3) * (↑(Nat.succ 2) * (↑(Nat.succ 1) * (1 * 1)))) +
v ^ 5 / (↑(Nat.succ 4) * (↑(Nat.succ 3) * (↑(Nat.succ 2) * (↑(Nat.succ 1) * (1 * 1))))) +
v ^ 6 / (↑(Nat.succ 5) * (↑(Nat.succ 4) * (↑(Nat.succ 3) * (↑(Nat.succ 2) * (↑(Nat.succ 1) * (1 * 1)))))) ≤
rexp vh_amgm:0 ≤ (v / 2 - 1) ^ 2h_v2:(851 / 400) ^ 2 ≤ v ^ 2h_v3:(851 / 400) ^ 3 ≤ v ^ 3⊢ 0 ≤ 851 / 400 norm_num All goals completed! 🐙) hv 4 v:ℝhv:851 / 400 ≤ vhv_nonneg:0 ≤ vh_sum:1 / 1 + v / (1 * 1) + v ^ 2 / (↑(Nat.succ 1) * (1 * 1)) + v ^ 3 / (↑(Nat.succ 2) * (↑(Nat.succ 1) * (1 * 1))) +
v ^ 4 / (↑(Nat.succ 3) * (↑(Nat.succ 2) * (↑(Nat.succ 1) * (1 * 1)))) +
v ^ 5 / (↑(Nat.succ 4) * (↑(Nat.succ 3) * (↑(Nat.succ 2) * (↑(Nat.succ 1) * (1 * 1))))) +
v ^ 6 / (↑(Nat.succ 5) * (↑(Nat.succ 4) * (↑(Nat.succ 3) * (↑(Nat.succ 2) * (↑(Nat.succ 1) * (1 * 1)))))) ≤
rexp vh_amgm:0 ≤ (v / 2 - 1) ^ 2h_v2:(851 / 400) ^ 2 ≤ v ^ 2h_v3:(851 / 400) ^ 3 ≤ v ^ 3h_v4:(851 / 400) ^ 4 ≤ v ^ 4⊢ 39 / 10 * v ≤ rexp v
have h_v5 : (851 / 400 : ℝ) ^ 5 ≤ v ^ 5 := pow_le_pow_left₀ (by v:ℝhv:851 / 400 ≤ vhv_nonneg:0 ≤ vh_sum:1 / 1 + v / (1 * 1) + v ^ 2 / (↑(Nat.succ 1) * (1 * 1)) + v ^ 3 / (↑(Nat.succ 2) * (↑(Nat.succ 1) * (1 * 1))) +
v ^ 4 / (↑(Nat.succ 3) * (↑(Nat.succ 2) * (↑(Nat.succ 1) * (1 * 1)))) +
v ^ 5 / (↑(Nat.succ 4) * (↑(Nat.succ 3) * (↑(Nat.succ 2) * (↑(Nat.succ 1) * (1 * 1))))) +
v ^ 6 / (↑(Nat.succ 5) * (↑(Nat.succ 4) * (↑(Nat.succ 3) * (↑(Nat.succ 2) * (↑(Nat.succ 1) * (1 * 1)))))) ≤
rexp vh_amgm:0 ≤ (v / 2 - 1) ^ 2h_v2:(851 / 400) ^ 2 ≤ v ^ 2h_v3:(851 / 400) ^ 3 ≤ v ^ 3h_v4:(851 / 400) ^ 4 ≤ v ^ 4⊢ 0 ≤ 851 / 400 norm_num All goals completed! 🐙) hv 5 v:ℝhv:851 / 400 ≤ vhv_nonneg:0 ≤ vh_sum:1 / 1 + v / (1 * 1) + v ^ 2 / (↑(Nat.succ 1) * (1 * 1)) + v ^ 3 / (↑(Nat.succ 2) * (↑(Nat.succ 1) * (1 * 1))) +
v ^ 4 / (↑(Nat.succ 3) * (↑(Nat.succ 2) * (↑(Nat.succ 1) * (1 * 1)))) +
v ^ 5 / (↑(Nat.succ 4) * (↑(Nat.succ 3) * (↑(Nat.succ 2) * (↑(Nat.succ 1) * (1 * 1))))) +
v ^ 6 / (↑(Nat.succ 5) * (↑(Nat.succ 4) * (↑(Nat.succ 3) * (↑(Nat.succ 2) * (↑(Nat.succ 1) * (1 * 1)))))) ≤
rexp vh_amgm:0 ≤ (v / 2 - 1) ^ 2h_v2:(851 / 400) ^ 2 ≤ v ^ 2h_v3:(851 / 400) ^ 3 ≤ v ^ 3h_v4:(851 / 400) ^ 4 ≤ v ^ 4h_v5:(851 / 400) ^ 5 ≤ v ^ 5⊢ 39 / 10 * v ≤ rexp v
have h_mono :
(39 / 10 : ℝ) ≤ 2 + v / 4 + v ^ 2 / 6 + v ^ 3 / 24 + v ^ 4 / 120 + v ^ 5 / 720 := by
linarith v:ℝhv:851 / 400 ≤ vhv_nonneg:0 ≤ vh_sum:1 / 1 + v / (1 * 1) + v ^ 2 / (↑(Nat.succ 1) * (1 * 1)) + v ^ 3 / (↑(Nat.succ 2) * (↑(Nat.succ 1) * (1 * 1))) +
v ^ 4 / (↑(Nat.succ 3) * (↑(Nat.succ 2) * (↑(Nat.succ 1) * (1 * 1)))) +
v ^ 5 / (↑(Nat.succ 4) * (↑(Nat.succ 3) * (↑(Nat.succ 2) * (↑(Nat.succ 1) * (1 * 1))))) +
v ^ 6 / (↑(Nat.succ 5) * (↑(Nat.succ 4) * (↑(Nat.succ 3) * (↑(Nat.succ 2) * (↑(Nat.succ 1) * (1 * 1)))))) ≤
rexp vh_amgm:0 ≤ (v / 2 - 1) ^ 2h_v2:(851 / 400) ^ 2 ≤ v ^ 2h_v3:(851 / 400) ^ 3 ≤ v ^ 3h_v4:(851 / 400) ^ 4 ≤ v ^ 4h_v5:(851 / 400) ^ 5 ≤ v ^ 5h_mono:39 / 10 ≤ 2 + v / 4 + v ^ 2 / 6 + v ^ 3 / 24 + v ^ 4 / 120 + v ^ 5 / 720⊢ 39 / 10 * v ≤ rexp v
have h_mul :
(39 / 10 : ℝ) * v ≤
v * (2 + v / 4 + v ^ 2 / 6 + v ^ 3 / 24 + v ^ 4 / 120 + v ^ 5 / 720) := by
nlinarith v:ℝhv:851 / 400 ≤ vhv_nonneg:0 ≤ vh_sum:1 / 1 + v / (1 * 1) + v ^ 2 / (↑(Nat.succ 1) * (1 * 1)) + v ^ 3 / (↑(Nat.succ 2) * (↑(Nat.succ 1) * (1 * 1))) +
v ^ 4 / (↑(Nat.succ 3) * (↑(Nat.succ 2) * (↑(Nat.succ 1) * (1 * 1)))) +
v ^ 5 / (↑(Nat.succ 4) * (↑(Nat.succ 3) * (↑(Nat.succ 2) * (↑(Nat.succ 1) * (1 * 1))))) +
v ^ 6 / (↑(Nat.succ 5) * (↑(Nat.succ 4) * (↑(Nat.succ 3) * (↑(Nat.succ 2) * (↑(Nat.succ 1) * (1 * 1)))))) ≤
rexp vh_amgm:0 ≤ (v / 2 - 1) ^ 2h_v2:(851 / 400) ^ 2 ≤ v ^ 2h_v3:(851 / 400) ^ 3 ≤ v ^ 3h_v4:(851 / 400) ^ 4 ≤ v ^ 4h_v5:(851 / 400) ^ 5 ≤ v ^ 5h_mono:39 / 10 ≤ 2 + v / 4 + v ^ 2 / 6 + v ^ 3 / 24 + v ^ 4 / 120 + v ^ 5 / 720h_mul:39 / 10 * v ≤ v * (2 + v / 4 + v ^ 2 / 6 + v ^ 3 / 24 + v ^ 4 / 120 + v ^ 5 / 720)⊢ 39 / 10 * v ≤ rexp v
have h_id :
1 + v + v ^ 2 / 2 + v ^ 3 / 6 + v ^ 4 / 24 + v ^ 5 / 120 + v ^ 6 / 720 =
(v / 2 - 1) ^ 2 +
v * (2 + v / 4 + v ^ 2 / 6 + v ^ 3 / 24 + v ^ 4 / 120 + v ^ 5 / 720) := by
ring v:ℝhv:851 / 400 ≤ vhv_nonneg:0 ≤ vh_sum:1 / 1 + v / (1 * 1) + v ^ 2 / (↑(Nat.succ 1) * (1 * 1)) + v ^ 3 / (↑(Nat.succ 2) * (↑(Nat.succ 1) * (1 * 1))) +
v ^ 4 / (↑(Nat.succ 3) * (↑(Nat.succ 2) * (↑(Nat.succ 1) * (1 * 1)))) +
v ^ 5 / (↑(Nat.succ 4) * (↑(Nat.succ 3) * (↑(Nat.succ 2) * (↑(Nat.succ 1) * (1 * 1))))) +
v ^ 6 / (↑(Nat.succ 5) * (↑(Nat.succ 4) * (↑(Nat.succ 3) * (↑(Nat.succ 2) * (↑(Nat.succ 1) * (1 * 1)))))) ≤
rexp vh_amgm:0 ≤ (v / 2 - 1) ^ 2h_v2:(851 / 400) ^ 2 ≤ v ^ 2h_v3:(851 / 400) ^ 3 ≤ v ^ 3h_v4:(851 / 400) ^ 4 ≤ v ^ 4h_v5:(851 / 400) ^ 5 ≤ v ^ 5h_mono:39 / 10 ≤ 2 + v / 4 + v ^ 2 / 6 + v ^ 3 / 24 + v ^ 4 / 120 + v ^ 5 / 720h_mul:39 / 10 * v ≤ v * (2 + v / 4 + v ^ 2 / 6 + v ^ 3 / 24 + v ^ 4 / 120 + v ^ 5 / 720)h_id:1 + v + v ^ 2 / 2 + v ^ 3 / 6 + v ^ 4 / 24 + v ^ 5 / 120 + v ^ 6 / 720 =
(v / 2 - 1) ^ 2 + v * (2 + v / 4 + v ^ 2 / 6 + v ^ 3 / 24 + v ^ 4 / 120 + v ^ 5 / 720)⊢ 39 / 10 * v ≤ rexp v
linarith All goals completed! 🐙
For x ≥ 5000, (Real.log x) ^ 2 ≤ (20 / 19) * Real.sqrt x.
lemma sq_log_le_twenty_nineteenths_sqrt {x : ℝ} (hx : 5000 ≤ x) :
(Real.log x) ^ 2 ≤ (20 / 19 : ℝ) * Real.sqrt x := by x:ℝhx:5000 ≤ x⊢ log x ^ 2 ≤ 20 / 19 * √x
have hL : (851 / 100 : ℝ) ≤ Real.log x := log_ge_851_div_100 hx x:ℝhx:5000 ≤ xhL:851 / 100 ≤ log x⊢ log x ^ 2 ≤ 20 / 19 * √x
have hv : (851 / 400 : ℝ) ≤ Real.log x / 4 := by linarith x:ℝhx:5000 ≤ xhL:851 / 100 ≤ log xhv:851 / 400 ≤ log x / 4⊢ log x ^ 2 ≤ 20 / 19 * √x
have hexp := exp_ge_thirty_nine_tenths_mul hv x:ℝhx:5000 ≤ xhL:851 / 100 ≤ log xhv:851 / 400 ≤ log x / 4hexp:39 / 10 * (log x / 4) ≤ rexp (log x / 4)⊢ log x ^ 2 ≤ 20 / 19 * √x
have h_exp_sq : (Real.exp (Real.log x / 4)) ^ 2 = Real.sqrt x := by
rw [sq, x:ℝhx:5000 ≤ xhL:851 / 100 ≤ log xhv:851 / 400 ≤ log x / 4hexp:39 / 10 * (log x / 4) ≤ rexp (log x / 4)⊢ rexp (log x / 4) * rexp (log x / 4) = √x ← Real.exp_add x:ℝhx:5000 ≤ xhL:851 / 100 ≤ log xhv:851 / 400 ≤ log x / 4hexp:39 / 10 * (log x / 4) ≤ rexp (log x / 4)⊢ rexp (log x / 4 + log x / 4) = √x] x:ℝhx:5000 ≤ xhL:851 / 100 ≤ log xhv:851 / 400 ≤ log x / 4hexp:39 / 10 * (log x / 4) ≤ rexp (log x / 4)⊢ rexp (log x / 4 + log x / 4) = √x
have h_half : Real.log x / 4 + Real.log x / 4 = Real.log (Real.sqrt x) := by x:ℝhx:5000 ≤ x⊢ log x ^ 2 ≤ 20 / 19 * √x
rw [Real.log_sqrt (by x:ℝhx:5000 ≤ xhL:851 / 100 ≤ log xhv:851 / 400 ≤ log x / 4hexp:39 / 10 * (log x / 4) ≤ rexp (log x / 4)⊢ 0 ≤ x linarith All goals completed! 🐙)] x:ℝhx:5000 ≤ xhL:851 / 100 ≤ log xhv:851 / 400 ≤ log x / 4hexp:39 / 10 * (log x / 4) ≤ rexp (log x / 4)⊢ log x / 4 + log x / 4 = log x / 2
ring x:ℝhx:5000 ≤ xhL:851 / 100 ≤ log xhv:851 / 400 ≤ log x / 4hexp:39 / 10 * (log x / 4) ≤ rexp (log x / 4)h_half:log x / 4 + log x / 4 = log √x⊢ rexp (log x / 4 + log x / 4) = √x
rw [h_half, x:ℝhx:5000 ≤ xhL:851 / 100 ≤ log xhv:851 / 400 ≤ log x / 4hexp:39 / 10 * (log x / 4) ≤ rexp (log x / 4)h_half:log x / 4 + log x / 4 = log √x⊢ rexp (log √x) = √x Real.exp_log (Real.sqrt_pos.mpr (by x:ℝhx:5000 ≤ xhL:851 / 100 ≤ log xhv:851 / 400 ≤ log x / 4hexp:39 / 10 * (log x / 4) ≤ rexp (log x / 4)h_half:log x / 4 + log x / 4 = log √x⊢ 0 < x linarith All goals completed! 🐙))] x:ℝhx:5000 ≤ xhL:851 / 100 ≤ log xhv:851 / 400 ≤ log x / 4hexp:39 / 10 * (log x / 4) ≤ rexp (log x / 4)h_exp_sq:rexp (log x / 4) ^ 2 = √x⊢ log x ^ 2 ≤ 20 / 19 * √x
have h_lhs_nonneg : 0 ≤ (39 / 10 : ℝ) * (Real.log x / 4) := by linarith x:ℝhx:5000 ≤ xhL:851 / 100 ≤ log xhv:851 / 400 ≤ log x / 4hexp:39 / 10 * (log x / 4) ≤ rexp (log x / 4)h_exp_sq:rexp (log x / 4) ^ 2 = √xh_lhs_nonneg:0 ≤ 39 / 10 * (log x / 4)⊢ log x ^ 2 ≤ 20 / 19 * √x
have h_sq_le : ((39 / 10 : ℝ) * (Real.log x / 4)) ^ 2 ≤ (Real.exp (Real.log x / 4)) ^ 2 :=
pow_le_pow_left₀ h_lhs_nonneg hexp 2 x:ℝhx:5000 ≤ xhL:851 / 100 ≤ log xhv:851 / 400 ≤ log x / 4hexp:39 / 10 * (log x / 4) ≤ rexp (log x / 4)h_exp_sq:rexp (log x / 4) ^ 2 = √xh_lhs_nonneg:0 ≤ 39 / 10 * (log x / 4)h_sq_le:(39 / 10 * (log x / 4)) ^ 2 ≤ rexp (log x / 4) ^ 2⊢ log x ^ 2 ≤ 20 / 19 * √x
rw [h_exp_sq x:ℝhx:5000 ≤ xhL:851 / 100 ≤ log xhv:851 / 400 ≤ log x / 4hexp:39 / 10 * (log x / 4) ≤ rexp (log x / 4)h_exp_sq:rexp (log x / 4) ^ 2 = √xh_lhs_nonneg:0 ≤ 39 / 10 * (log x / 4)h_sq_le:(39 / 10 * (log x / 4)) ^ 2 ≤ √x⊢ log x ^ 2 ≤ 20 / 19 * √x] at h_sq_le x:ℝhx:5000 ≤ xhL:851 / 100 ≤ log xhv:851 / 400 ≤ log x / 4hexp:39 / 10 * (log x / 4) ≤ rexp (log x / 4)h_exp_sq:rexp (log x / 4) ^ 2 = √xh_lhs_nonneg:0 ≤ 39 / 10 * (log x / 4)h_sq_le:(39 / 10 * (log x / 4)) ^ 2 ≤ √x⊢ log x ^ 2 ≤ 20 / 19 * √x
nlinarith All goals completed! 🐙
Helper bounds on Real.sqrt (x + h), (x + h) ^ (3 / 2 : ℝ), and (x + h) ^ (3 / 4 : ℝ).
lemma rpow_xh_bounds {x h S L : ℝ} (hx : 5000 ≤ x) (hS : 70 ≤ S) (hS_sq : S ^ 2 = x)
(hL_sq : (7242 / 100 : ℝ) ≤ L ^ 2) (hh_def : h = (7 / 20 : ℝ) * S * L ^ 2)
(hh_le_x : h ≤ (7 / 19 : ℝ) * x) :
S ≤ Real.sqrt (x + h) ∧
Real.sqrt (x + h) ≤ (34 / 29 : ℝ) * S ∧
(x + h) ^ (3 / 2 : ℝ) ≤ (161 / 100 : ℝ) * S ^ 3 ∧
(x + h) ^ (3 / 4 : ℝ) ≤ (26 / 171 : ℝ) * S ^ 2 := by x:ℝh:ℝS:ℝL:ℝhx:5000 ≤ xhS:70 ≤ ShS_sq:S ^ 2 = xhL_sq:7242 / 100 ≤ L ^ 2hh_def:h = 7 / 20 * S * L ^ 2hh_le_x:h ≤ 7 / 19 * x⊢ S ≤ √(x + h) ∧ √(x + h) ≤ 34 / 29 * S ∧ (x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3 ∧ (x + h) ^ (3 / 4) ≤ 26 / 171 * S ^ 2
have hS_pos : 0 < S := by linarith x:ℝh:ℝS:ℝL:ℝhx:5000 ≤ xhS:70 ≤ ShS_sq:S ^ 2 = xhL_sq:7242 / 100 ≤ L ^ 2hh_def:h = 7 / 20 * S * L ^ 2hh_le_x:h ≤ 7 / 19 * xhS_pos:0 < S⊢ S ≤ √(x + h) ∧ √(x + h) ≤ 34 / 29 * S ∧ (x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3 ∧ (x + h) ^ (3 / 4) ≤ 26 / 171 * S ^ 2
have hh_ge : 1600 ≤ h := by
rw [hh_def x:ℝh:ℝS:ℝL:ℝhx:5000 ≤ xhS:70 ≤ ShS_sq:S ^ 2 = xhL_sq:7242 / 100 ≤ L ^ 2hh_def:h = 7 / 20 * S * L ^ 2hh_le_x:h ≤ 7 / 19 * xhS_pos:0 < S⊢ 1600 ≤ 7 / 20 * S * L ^ 2] x:ℝh:ℝS:ℝL:ℝhx:5000 ≤ xhS:70 ≤ ShS_sq:S ^ 2 = xhL_sq:7242 / 100 ≤ L ^ 2hh_def:h = 7 / 20 * S * L ^ 2hh_le_x:h ≤ 7 / 19 * xhS_pos:0 < S⊢ 1600 ≤ 7 / 20 * S * L ^ 2
nlinarith x:ℝh:ℝS:ℝL:ℝhx:5000 ≤ xhS:70 ≤ ShS_sq:S ^ 2 = xhL_sq:7242 / 100 ≤ L ^ 2hh_def:h = 7 / 20 * S * L ^ 2hh_le_x:h ≤ 7 / 19 * xhS_pos:0 < Shh_ge:1600 ≤ h⊢ S ≤ √(x + h) ∧ √(x + h) ≤ 34 / 29 * S ∧ (x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3 ∧ (x + h) ^ (3 / 4) ≤ 26 / 171 * S ^ 2
have hx_add_h_le' : x + h ≤ (26 / 19 : ℝ) * S ^ 2 := by linarith x:ℝh:ℝS:ℝL:ℝhx:5000 ≤ xhS:70 ≤ ShS_sq:S ^ 2 = xhL_sq:7242 / 100 ≤ L ^ 2hh_def:h = 7 / 20 * S * L ^ 2hh_le_x:h ≤ 7 / 19 * xhS_pos:0 < Shh_ge:1600 ≤ hhx_add_h_le':x + h ≤ 26 / 19 * S ^ 2⊢ S ≤ √(x + h) ∧ √(x + h) ≤ 34 / 29 * S ∧ (x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3 ∧ (x + h) ^ (3 / 4) ≤ 26 / 171 * S ^ 2
have hx_add_h_le : x + h ≤ ((34 / 29 : ℝ) * S) ^ 2 := by nlinarith x:ℝh:ℝS:ℝL:ℝhx:5000 ≤ xhS:70 ≤ ShS_sq:S ^ 2 = xhL_sq:7242 / 100 ≤ L ^ 2hh_def:h = 7 / 20 * S * L ^ 2hh_le_x:h ≤ 7 / 19 * xhS_pos:0 < Shh_ge:1600 ≤ hhx_add_h_le':x + h ≤ 26 / 19 * S ^ 2hx_add_h_le:x + h ≤ (34 / 29 * S) ^ 2⊢ S ≤ √(x + h) ∧ √(x + h) ≤ 34 / 29 * S ∧ (x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3 ∧ (x + h) ^ (3 / 4) ≤ 26 / 171 * S ^ 2
have h_sqrt_ge : S ≤ Real.sqrt (x + h) := by
have h1 : S ^ 2 ≤ x + h := by x:ℝh:ℝS:ℝL:ℝhx:5000 ≤ xhS:70 ≤ ShS_sq:S ^ 2 = xhL_sq:7242 / 100 ≤ L ^ 2hh_def:h = 7 / 20 * S * L ^ 2hh_le_x:h ≤ 7 / 19 * x⊢ S ≤ √(x + h) ∧ √(x + h) ≤ 34 / 29 * S ∧ (x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3 ∧ (x + h) ^ (3 / 4) ≤ 26 / 171 * S ^ 2 linarith x:ℝh:ℝS:ℝL:ℝhx:5000 ≤ xhS:70 ≤ ShS_sq:S ^ 2 = xhL_sq:7242 / 100 ≤ L ^ 2hh_def:h = 7 / 20 * S * L ^ 2hh_le_x:h ≤ 7 / 19 * xhS_pos:0 < Shh_ge:1600 ≤ hhx_add_h_le':x + h ≤ 26 / 19 * S ^ 2hx_add_h_le:x + h ≤ (34 / 29 * S) ^ 2h1:S ^ 2 ≤ x + h⊢ S ≤ √(x + h)
have h2 := Real.sqrt_le_sqrt h1 x:ℝh:ℝS:ℝL:ℝhx:5000 ≤ xhS:70 ≤ ShS_sq:S ^ 2 = xhL_sq:7242 / 100 ≤ L ^ 2hh_def:h = 7 / 20 * S * L ^ 2hh_le_x:h ≤ 7 / 19 * xhS_pos:0 < Shh_ge:1600 ≤ hhx_add_h_le':x + h ≤ 26 / 19 * S ^ 2hx_add_h_le:x + h ≤ (34 / 29 * S) ^ 2h1:S ^ 2 ≤ x + hh2:√(S ^ 2) ≤ √(x + h)⊢ S ≤ √(x + h)
rwa [Real.sqrt_sq hS_pos.le] at h2 x:ℝh:ℝS:ℝL:ℝhx:5000 ≤ xhS:70 ≤ ShS_sq:S ^ 2 = xhL_sq:7242 / 100 ≤ L ^ 2hh_def:h = 7 / 20 * S * L ^ 2hh_le_x:h ≤ 7 / 19 * xhS_pos:0 < Shh_ge:1600 ≤ hhx_add_h_le':x + h ≤ 26 / 19 * S ^ 2hx_add_h_le:x + h ≤ (34 / 29 * S) ^ 2h_sqrt_ge:S ≤ √(x + h)⊢ S ≤ √(x + h) ∧ √(x + h) ≤ 34 / 29 * S ∧ (x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3 ∧ (x + h) ^ (3 / 4) ≤ 26 / 171 * S ^ 2
have h_sqrt_xh : Real.sqrt (x + h) ≤ (34 / 29 : ℝ) * S := by
have h1 := Real.sqrt_le_sqrt hx_add_h_le x:ℝh:ℝS:ℝL:ℝhx:5000 ≤ xhS:70 ≤ ShS_sq:S ^ 2 = xhL_sq:7242 / 100 ≤ L ^ 2hh_def:h = 7 / 20 * S * L ^ 2hh_le_x:h ≤ 7 / 19 * xhS_pos:0 < Shh_ge:1600 ≤ hhx_add_h_le':x + h ≤ 26 / 19 * S ^ 2hx_add_h_le:x + h ≤ (34 / 29 * S) ^ 2h_sqrt_ge:S ≤ √(x + h)h1:√(x + h) ≤ √((34 / 29 * S) ^ 2)⊢ √(x + h) ≤ 34 / 29 * S
rwa [Real.sqrt_sq (by x:ℝh:ℝS:ℝL:ℝhx:5000 ≤ xhS:70 ≤ ShS_sq:S ^ 2 = xhL_sq:7242 / 100 ≤ L ^ 2hh_def:h = 7 / 20 * S * L ^ 2hh_le_x:h ≤ 7 / 19 * xhS_pos:0 < Shh_ge:1600 ≤ hhx_add_h_le':x + h ≤ 26 / 19 * S ^ 2hx_add_h_le:x + h ≤ (34 / 29 * S) ^ 2h_sqrt_ge:S ≤ √(x + h)h1:√(x + h) ≤ √((34 / 29 * S) ^ 2)⊢ 0 ≤ 34 / 29 * S positivity All goals completed! 🐙)] at h1 x:ℝh:ℝS:ℝL:ℝhx:5000 ≤ xhS:70 ≤ ShS_sq:S ^ 2 = xhL_sq:7242 / 100 ≤ L ^ 2hh_def:h = 7 / 20 * S * L ^ 2hh_le_x:h ≤ 7 / 19 * xhS_pos:0 < Shh_ge:1600 ≤ hhx_add_h_le':x + h ≤ 26 / 19 * S ^ 2hx_add_h_le:x + h ≤ (34 / 29 * S) ^ 2h_sqrt_ge:S ≤ √(x + h)h_sqrt_xh:√(x + h) ≤ 34 / 29 * S⊢ S ≤ √(x + h) ∧ √(x + h) ≤ 34 / 29 * S ∧ (x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3 ∧ (x + h) ^ (3 / 4) ≤ 26 / 171 * S ^ 2
have h_rpow_32 : (x + h) ^ (3 / 2 : ℝ) ≤ (161 / 100 : ℝ) * S ^ 3 := by
have h_split : (x + h) ^ (3 / 2 : ℝ) = (x + h) * Real.sqrt (x + h) := by x:ℝh:ℝS:ℝL:ℝhx:5000 ≤ xhS:70 ≤ ShS_sq:S ^ 2 = xhL_sq:7242 / 100 ≤ L ^ 2hh_def:h = 7 / 20 * S * L ^ 2hh_le_x:h ≤ 7 / 19 * x⊢ S ≤ √(x + h) ∧ √(x + h) ≤ 34 / 29 * S ∧ (x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3 ∧ (x + h) ^ (3 / 4) ≤ 26 / 171 * S ^ 2
have h_eq : (3 / 2 : ℝ) = 1 + 1 / 2 := by x:ℝh:ℝS:ℝL:ℝhx:5000 ≤ xhS:70 ≤ ShS_sq:S ^ 2 = xhL_sq:7242 / 100 ≤ L ^ 2hh_def:h = 7 / 20 * S * L ^ 2hh_le_x:h ≤ 7 / 19 * x⊢ S ≤ √(x + h) ∧ √(x + h) ≤ 34 / 29 * S ∧ (x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3 ∧ (x + h) ^ (3 / 4) ≤ 26 / 171 * S ^ 2 norm_num x:ℝh:ℝS:ℝL:ℝhx:5000 ≤ xhS:70 ≤ ShS_sq:S ^ 2 = xhL_sq:7242 / 100 ≤ L ^ 2hh_def:h = 7 / 20 * S * L ^ 2hh_le_x:h ≤ 7 / 19 * xhS_pos:0 < Shh_ge:1600 ≤ hhx_add_h_le':x + h ≤ 26 / 19 * S ^ 2hx_add_h_le:x + h ≤ (34 / 29 * S) ^ 2h_sqrt_ge:S ≤ √(x + h)h_sqrt_xh:√(x + h) ≤ 34 / 29 * Sh_eq:3 / 2 = 1 + 1 / 2⊢ (x + h) ^ (3 / 2) = (x + h) * √(x + h)
rw [h_eq, x:ℝh:ℝS:ℝL:ℝhx:5000 ≤ xhS:70 ≤ ShS_sq:S ^ 2 = xhL_sq:7242 / 100 ≤ L ^ 2hh_def:h = 7 / 20 * S * L ^ 2hh_le_x:h ≤ 7 / 19 * xhS_pos:0 < Shh_ge:1600 ≤ hhx_add_h_le':x + h ≤ 26 / 19 * S ^ 2hx_add_h_le:x + h ≤ (34 / 29 * S) ^ 2h_sqrt_ge:S ≤ √(x + h)h_sqrt_xh:√(x + h) ≤ 34 / 29 * Sh_eq:3 / 2 = 1 + 1 / 2⊢ (x + h) ^ (1 + 1 / 2) = (x + h) * √(x + h) Real.rpow_add (by x:ℝh:ℝS:ℝL:ℝhx:5000 ≤ xhS:70 ≤ ShS_sq:S ^ 2 = xhL_sq:7242 / 100 ≤ L ^ 2hh_def:h = 7 / 20 * S * L ^ 2hh_le_x:h ≤ 7 / 19 * xhS_pos:0 < Shh_ge:1600 ≤ hhx_add_h_le':x + h ≤ 26 / 19 * S ^ 2hx_add_h_le:x + h ≤ (34 / 29 * S) ^ 2h_sqrt_ge:S ≤ √(x + h)h_sqrt_xh:√(x + h) ≤ 34 / 29 * Sh_eq:3 / 2 = 1 + 1 / 2⊢ 0 < x + h linarith All goals completed! 🐙), Real.rpow_one, x:ℝh:ℝS:ℝL:ℝhx:5000 ≤ xhS:70 ≤ ShS_sq:S ^ 2 = xhL_sq:7242 / 100 ≤ L ^ 2hh_def:h = 7 / 20 * S * L ^ 2hh_le_x:h ≤ 7 / 19 * xhS_pos:0 < Shh_ge:1600 ≤ hhx_add_h_le':x + h ≤ 26 / 19 * S ^ 2hx_add_h_le:x + h ≤ (34 / 29 * S) ^ 2h_sqrt_ge:S ≤ √(x + h)h_sqrt_xh:√(x + h) ≤ 34 / 29 * Sh_eq:3 / 2 = 1 + 1 / 2⊢ (x + h) * (x + h) ^ (1 / 2) = (x + h) * √(x + h) ← Real.sqrt_eq_rpow x:ℝh:ℝS:ℝL:ℝhx:5000 ≤ xhS:70 ≤ ShS_sq:S ^ 2 = xhL_sq:7242 / 100 ≤ L ^ 2hh_def:h = 7 / 20 * S * L ^ 2hh_le_x:h ≤ 7 / 19 * xhS_pos:0 < Shh_ge:1600 ≤ hhx_add_h_le':x + h ≤ 26 / 19 * S ^ 2hx_add_h_le:x + h ≤ (34 / 29 * S) ^ 2h_sqrt_ge:S ≤ √(x + h)h_sqrt_xh:√(x + h) ≤ 34 / 29 * Sh_eq:3 / 2 = 1 + 1 / 2⊢ (x + h) * √(x + h) = (x + h) * √(x + h)] x:ℝh:ℝS:ℝL:ℝhx:5000 ≤ xhS:70 ≤ ShS_sq:S ^ 2 = xhL_sq:7242 / 100 ≤ L ^ 2hh_def:h = 7 / 20 * S * L ^ 2hh_le_x:h ≤ 7 / 19 * xhS_pos:0 < Shh_ge:1600 ≤ hhx_add_h_le':x + h ≤ 26 / 19 * S ^ 2hx_add_h_le:x + h ≤ (34 / 29 * S) ^ 2h_sqrt_ge:S ≤ √(x + h)h_sqrt_xh:√(x + h) ≤ 34 / 29 * Sh_split:(x + h) ^ (3 / 2) = (x + h) * √(x + h)⊢ (x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3
have h_sqrt_nonneg : 0 ≤ Real.sqrt (x + h) := Real.sqrt_nonneg _ x:ℝh:ℝS:ℝL:ℝhx:5000 ≤ xhS:70 ≤ ShS_sq:S ^ 2 = xhL_sq:7242 / 100 ≤ L ^ 2hh_def:h = 7 / 20 * S * L ^ 2hh_le_x:h ≤ 7 / 19 * xhS_pos:0 < Shh_ge:1600 ≤ hhx_add_h_le':x + h ≤ 26 / 19 * S ^ 2hx_add_h_le:x + h ≤ (34 / 29 * S) ^ 2h_sqrt_ge:S ≤ √(x + h)h_sqrt_xh:√(x + h) ≤ 34 / 29 * Sh_split:(x + h) ^ (3 / 2) = (x + h) * √(x + h)h_sqrt_nonneg:0 ≤ √(x + h)⊢ (x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3
rw [h_split x:ℝh:ℝS:ℝL:ℝhx:5000 ≤ xhS:70 ≤ ShS_sq:S ^ 2 = xhL_sq:7242 / 100 ≤ L ^ 2hh_def:h = 7 / 20 * S * L ^ 2hh_le_x:h ≤ 7 / 19 * xhS_pos:0 < Shh_ge:1600 ≤ hhx_add_h_le':x + h ≤ 26 / 19 * S ^ 2hx_add_h_le:x + h ≤ (34 / 29 * S) ^ 2h_sqrt_ge:S ≤ √(x + h)h_sqrt_xh:√(x + h) ≤ 34 / 29 * Sh_split:(x + h) ^ (3 / 2) = (x + h) * √(x + h)h_sqrt_nonneg:0 ≤ √(x + h)⊢ (x + h) * √(x + h) ≤ 161 / 100 * S ^ 3] x:ℝh:ℝS:ℝL:ℝhx:5000 ≤ xhS:70 ≤ ShS_sq:S ^ 2 = xhL_sq:7242 / 100 ≤ L ^ 2hh_def:h = 7 / 20 * S * L ^ 2hh_le_x:h ≤ 7 / 19 * xhS_pos:0 < Shh_ge:1600 ≤ hhx_add_h_le':x + h ≤ 26 / 19 * S ^ 2hx_add_h_le:x + h ≤ (34 / 29 * S) ^ 2h_sqrt_ge:S ≤ √(x + h)h_sqrt_xh:√(x + h) ≤ 34 / 29 * Sh_split:(x + h) ^ (3 / 2) = (x + h) * √(x + h)h_sqrt_nonneg:0 ≤ √(x + h)⊢ (x + h) * √(x + h) ≤ 161 / 100 * S ^ 3
nlinarith x:ℝh:ℝS:ℝL:ℝhx:5000 ≤ xhS:70 ≤ ShS_sq:S ^ 2 = xhL_sq:7242 / 100 ≤ L ^ 2hh_def:h = 7 / 20 * S * L ^ 2hh_le_x:h ≤ 7 / 19 * xhS_pos:0 < Shh_ge:1600 ≤ hhx_add_h_le':x + h ≤ 26 / 19 * S ^ 2hx_add_h_le:x + h ≤ (34 / 29 * S) ^ 2h_sqrt_ge:S ≤ √(x + h)h_sqrt_xh:√(x + h) ≤ 34 / 29 * Sh_rpow_32:(x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3⊢ S ≤ √(x + h) ∧ √(x + h) ≤ 34 / 29 * S ∧ (x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3 ∧ (x + h) ^ (3 / 4) ≤ 26 / 171 * S ^ 2
have h_rpow_34 : (x + h) ^ (3 / 4 : ℝ) ≤ (26 / 171 : ℝ) * S ^ 2 := by
have h6561 : (9 : ℝ) ^ (4 : ℝ) ≤ x + h := by x:ℝh:ℝS:ℝL:ℝhx:5000 ≤ xhS:70 ≤ ShS_sq:S ^ 2 = xhL_sq:7242 / 100 ≤ L ^ 2hh_def:h = 7 / 20 * S * L ^ 2hh_le_x:h ≤ 7 / 19 * x⊢ S ≤ √(x + h) ∧ √(x + h) ≤ 34 / 29 * S ∧ (x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3 ∧ (x + h) ^ (3 / 4) ≤ 26 / 171 * S ^ 2 norm_num x:ℝh:ℝS:ℝL:ℝhx:5000 ≤ xhS:70 ≤ ShS_sq:S ^ 2 = xhL_sq:7242 / 100 ≤ L ^ 2hh_def:h = 7 / 20 * S * L ^ 2hh_le_x:h ≤ 7 / 19 * xhS_pos:0 < Shh_ge:1600 ≤ hhx_add_h_le':x + h ≤ 26 / 19 * S ^ 2hx_add_h_le:x + h ≤ (34 / 29 * S) ^ 2h_sqrt_ge:S ≤ √(x + h)h_sqrt_xh:√(x + h) ≤ 34 / 29 * Sh_rpow_32:(x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3⊢ 6561 ≤ x + h; linarith x:ℝh:ℝS:ℝL:ℝhx:5000 ≤ xhS:70 ≤ ShS_sq:S ^ 2 = xhL_sq:7242 / 100 ≤ L ^ 2hh_def:h = 7 / 20 * S * L ^ 2hh_le_x:h ≤ 7 / 19 * xhS_pos:0 < Shh_ge:1600 ≤ hhx_add_h_le':x + h ≤ 26 / 19 * S ^ 2hx_add_h_le:x + h ≤ (34 / 29 * S) ^ 2h_sqrt_ge:S ≤ √(x + h)h_sqrt_xh:√(x + h) ≤ 34 / 29 * Sh_rpow_32:(x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3h6561:9 ^ 4 ≤ x + h⊢ (x + h) ^ (3 / 4) ≤ 26 / 171 * S ^ 2
have h9_le : (9 : ℝ) ≤ (x + h) ^ (1 / 4 : ℝ) := by x:ℝh:ℝS:ℝL:ℝhx:5000 ≤ xhS:70 ≤ ShS_sq:S ^ 2 = xhL_sq:7242 / 100 ≤ L ^ 2hh_def:h = 7 / 20 * S * L ^ 2hh_le_x:h ≤ 7 / 19 * x⊢ S ≤ √(x + h) ∧ √(x + h) ≤ 34 / 29 * S ∧ (x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3 ∧ (x + h) ^ (3 / 4) ≤ 26 / 171 * S ^ 2
have h1 := Real.rpow_le_rpow (by x:ℝh:ℝS:ℝL:ℝhx:5000 ≤ xhS:70 ≤ ShS_sq:S ^ 2 = xhL_sq:7242 / 100 ≤ L ^ 2hh_def:h = 7 / 20 * S * L ^ 2hh_le_x:h ≤ 7 / 19 * xhS_pos:0 < Shh_ge:1600 ≤ hhx_add_h_le':x + h ≤ 26 / 19 * S ^ 2hx_add_h_le:x + h ≤ (34 / 29 * S) ^ 2h_sqrt_ge:S ≤ √(x + h)h_sqrt_xh:√(x + h) ≤ 34 / 29 * Sh_rpow_32:(x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3h6561:9 ^ 4 ≤ x + h⊢ 0 ≤ 9 ^ 4 positivity All goals completed! 🐙) h6561 (by x:ℝh:ℝS:ℝL:ℝhx:5000 ≤ xhS:70 ≤ ShS_sq:S ^ 2 = xhL_sq:7242 / 100 ≤ L ^ 2hh_def:h = 7 / 20 * S * L ^ 2hh_le_x:h ≤ 7 / 19 * xhS_pos:0 < Shh_ge:1600 ≤ hhx_add_h_le':x + h ≤ 26 / 19 * S ^ 2hx_add_h_le:x + h ≤ (34 / 29 * S) ^ 2h_sqrt_ge:S ≤ √(x + h)h_sqrt_xh:√(x + h) ≤ 34 / 29 * Sh_rpow_32:(x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3h6561:9 ^ 4 ≤ x + h⊢ 0 ≤ 1 / 4 norm_num All goals completed! 🐙 : (0 : ℝ) ≤ 1 / 4) x:ℝh:ℝS:ℝL:ℝhx:5000 ≤ xhS:70 ≤ ShS_sq:S ^ 2 = xhL_sq:7242 / 100 ≤ L ^ 2hh_def:h = 7 / 20 * S * L ^ 2hh_le_x:h ≤ 7 / 19 * xhS_pos:0 < Shh_ge:1600 ≤ hhx_add_h_le':x + h ≤ 26 / 19 * S ^ 2hx_add_h_le:x + h ≤ (34 / 29 * S) ^ 2h_sqrt_ge:S ≤ √(x + h)h_sqrt_xh:√(x + h) ≤ 34 / 29 * Sh_rpow_32:(x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3h6561:9 ^ 4 ≤ x + hh1:(9 ^ 4) ^ (1 / 4) ≤ (x + h) ^ (1 / 4)⊢ 9 ≤ (x + h) ^ (1 / 4)
rw [← Real.rpow_mul (by x:ℝh:ℝS:ℝL:ℝhx:5000 ≤ xhS:70 ≤ ShS_sq:S ^ 2 = xhL_sq:7242 / 100 ≤ L ^ 2hh_def:h = 7 / 20 * S * L ^ 2hh_le_x:h ≤ 7 / 19 * xhS_pos:0 < Shh_ge:1600 ≤ hhx_add_h_le':x + h ≤ 26 / 19 * S ^ 2hx_add_h_le:x + h ≤ (34 / 29 * S) ^ 2h_sqrt_ge:S ≤ √(x + h)h_sqrt_xh:√(x + h) ≤ 34 / 29 * Sh_rpow_32:(x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3h6561:9 ^ 4 ≤ x + hh1:(9 ^ 4) ^ (1 / 4) ≤ (x + h) ^ (1 / 4)⊢ 0 ≤ 9 norm_num All goals completed! 🐙)] at h1 x:ℝh:ℝS:ℝL:ℝhx:5000 ≤ xhS:70 ≤ ShS_sq:S ^ 2 = xhL_sq:7242 / 100 ≤ L ^ 2hh_def:h = 7 / 20 * S * L ^ 2hh_le_x:h ≤ 7 / 19 * xhS_pos:0 < Shh_ge:1600 ≤ hhx_add_h_le':x + h ≤ 26 / 19 * S ^ 2hx_add_h_le:x + h ≤ (34 / 29 * S) ^ 2h_sqrt_ge:S ≤ √(x + h)h_sqrt_xh:√(x + h) ≤ 34 / 29 * Sh_rpow_32:(x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3h6561:9 ^ 4 ≤ x + hh1:9 ^ (4 * (1 / 4)) ≤ (x + h) ^ (1 / 4)⊢ 9 ≤ (x + h) ^ (1 / 4)
norm_num at h1 x:ℝh:ℝS:ℝL:ℝhx:5000 ≤ xhS:70 ≤ ShS_sq:S ^ 2 = xhL_sq:7242 / 100 ≤ L ^ 2hh_def:h = 7 / 20 * S * L ^ 2hh_le_x:h ≤ 7 / 19 * xhS_pos:0 < Shh_ge:1600 ≤ hhx_add_h_le':x + h ≤ 26 / 19 * S ^ 2hx_add_h_le:x + h ≤ (34 / 29 * S) ^ 2h_sqrt_ge:S ≤ √(x + h)h_sqrt_xh:√(x + h) ≤ 34 / 29 * Sh_rpow_32:(x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3h6561:9 ^ 4 ≤ x + hh1:9 ≤ (x + h) ^ (1 / 4)⊢ 9 ≤ (x + h) ^ (1 / 4)
exact h1 x:ℝh:ℝS:ℝL:ℝhx:5000 ≤ xhS:70 ≤ ShS_sq:S ^ 2 = xhL_sq:7242 / 100 ≤ L ^ 2hh_def:h = 7 / 20 * S * L ^ 2hh_le_x:h ≤ 7 / 19 * xhS_pos:0 < Shh_ge:1600 ≤ hhx_add_h_le':x + h ≤ 26 / 19 * S ^ 2hx_add_h_le:x + h ≤ (34 / 29 * S) ^ 2h_sqrt_ge:S ≤ √(x + h)h_sqrt_xh:√(x + h) ≤ 34 / 29 * Sh_rpow_32:(x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3h6561:9 ^ 4 ≤ x + hh9_le:9 ≤ (x + h) ^ (1 / 4)⊢ (x + h) ^ (3 / 4) ≤ 26 / 171 * S ^ 2
have h_prod : (x + h) ^ (3 / 4 : ℝ) * (x + h) ^ (1 / 4 : ℝ) = x + h := by x:ℝh:ℝS:ℝL:ℝhx:5000 ≤ xhS:70 ≤ ShS_sq:S ^ 2 = xhL_sq:7242 / 100 ≤ L ^ 2hh_def:h = 7 / 20 * S * L ^ 2hh_le_x:h ≤ 7 / 19 * x⊢ S ≤ √(x + h) ∧ √(x + h) ≤ 34 / 29 * S ∧ (x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3 ∧ (x + h) ^ (3 / 4) ≤ 26 / 171 * S ^ 2
rw [← Real.rpow_add (by x:ℝh:ℝS:ℝL:ℝhx:5000 ≤ xhS:70 ≤ ShS_sq:S ^ 2 = xhL_sq:7242 / 100 ≤ L ^ 2hh_def:h = 7 / 20 * S * L ^ 2hh_le_x:h ≤ 7 / 19 * xhS_pos:0 < Shh_ge:1600 ≤ hhx_add_h_le':x + h ≤ 26 / 19 * S ^ 2hx_add_h_le:x + h ≤ (34 / 29 * S) ^ 2h_sqrt_ge:S ≤ √(x + h)h_sqrt_xh:√(x + h) ≤ 34 / 29 * Sh_rpow_32:(x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3h6561:9 ^ 4 ≤ x + hh9_le:9 ≤ (x + h) ^ (1 / 4)⊢ 0 < x + h linarith All goals completed! 🐙)] x:ℝh:ℝS:ℝL:ℝhx:5000 ≤ xhS:70 ≤ ShS_sq:S ^ 2 = xhL_sq:7242 / 100 ≤ L ^ 2hh_def:h = 7 / 20 * S * L ^ 2hh_le_x:h ≤ 7 / 19 * xhS_pos:0 < Shh_ge:1600 ≤ hhx_add_h_le':x + h ≤ 26 / 19 * S ^ 2hx_add_h_le:x + h ≤ (34 / 29 * S) ^ 2h_sqrt_ge:S ≤ √(x + h)h_sqrt_xh:√(x + h) ≤ 34 / 29 * Sh_rpow_32:(x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3h6561:9 ^ 4 ≤ x + hh9_le:9 ≤ (x + h) ^ (1 / 4)⊢ (x + h) ^ (3 / 4 + 1 / 4) = x + h
norm_num x:ℝh:ℝS:ℝL:ℝhx:5000 ≤ xhS:70 ≤ ShS_sq:S ^ 2 = xhL_sq:7242 / 100 ≤ L ^ 2hh_def:h = 7 / 20 * S * L ^ 2hh_le_x:h ≤ 7 / 19 * xhS_pos:0 < Shh_ge:1600 ≤ hhx_add_h_le':x + h ≤ 26 / 19 * S ^ 2hx_add_h_le:x + h ≤ (34 / 29 * S) ^ 2h_sqrt_ge:S ≤ √(x + h)h_sqrt_xh:√(x + h) ≤ 34 / 29 * Sh_rpow_32:(x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3h6561:9 ^ 4 ≤ x + hh9_le:9 ≤ (x + h) ^ (1 / 4)h_prod:(x + h) ^ (3 / 4) * (x + h) ^ (1 / 4) = x + h⊢ (x + h) ^ (3 / 4) ≤ 26 / 171 * S ^ 2
have h_nonneg : 0 ≤ (x + h) ^ (3 / 4 : ℝ) := Real.rpow_nonneg (by x:ℝh:ℝS:ℝL:ℝhx:5000 ≤ xhS:70 ≤ ShS_sq:S ^ 2 = xhL_sq:7242 / 100 ≤ L ^ 2hh_def:h = 7 / 20 * S * L ^ 2hh_le_x:h ≤ 7 / 19 * xhS_pos:0 < Shh_ge:1600 ≤ hhx_add_h_le':x + h ≤ 26 / 19 * S ^ 2hx_add_h_le:x + h ≤ (34 / 29 * S) ^ 2h_sqrt_ge:S ≤ √(x + h)h_sqrt_xh:√(x + h) ≤ 34 / 29 * Sh_rpow_32:(x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3h6561:9 ^ 4 ≤ x + hh9_le:9 ≤ (x + h) ^ (1 / 4)h_prod:(x + h) ^ (3 / 4) * (x + h) ^ (1 / 4) = x + h⊢ 0 ≤ x + h linarith All goals completed! 🐙) _ x:ℝh:ℝS:ℝL:ℝhx:5000 ≤ xhS:70 ≤ ShS_sq:S ^ 2 = xhL_sq:7242 / 100 ≤ L ^ 2hh_def:h = 7 / 20 * S * L ^ 2hh_le_x:h ≤ 7 / 19 * xhS_pos:0 < Shh_ge:1600 ≤ hhx_add_h_le':x + h ≤ 26 / 19 * S ^ 2hx_add_h_le:x + h ≤ (34 / 29 * S) ^ 2h_sqrt_ge:S ≤ √(x + h)h_sqrt_xh:√(x + h) ≤ 34 / 29 * Sh_rpow_32:(x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3h6561:9 ^ 4 ≤ x + hh9_le:9 ≤ (x + h) ^ (1 / 4)h_prod:(x + h) ^ (3 / 4) * (x + h) ^ (1 / 4) = x + hh_nonneg:0 ≤ (x + h) ^ (3 / 4)⊢ (x + h) ^ (3 / 4) ≤ 26 / 171 * S ^ 2
nlinarith x:ℝh:ℝS:ℝL:ℝhx:5000 ≤ xhS:70 ≤ ShS_sq:S ^ 2 = xhL_sq:7242 / 100 ≤ L ^ 2hh_def:h = 7 / 20 * S * L ^ 2hh_le_x:h ≤ 7 / 19 * xhS_pos:0 < Shh_ge:1600 ≤ hhx_add_h_le':x + h ≤ 26 / 19 * S ^ 2hx_add_h_le:x + h ≤ (34 / 29 * S) ^ 2h_sqrt_ge:S ≤ √(x + h)h_sqrt_xh:√(x + h) ≤ 34 / 29 * Sh_rpow_32:(x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3h_rpow_34:(x + h) ^ (3 / 4) ≤ 26 / 171 * S ^ 2⊢ S ≤ √(x + h) ∧ √(x + h) ≤ 34 / 29 * S ∧ (x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3 ∧ (x + h) ^ (3 / 4) ≤ 26 / 171 * S ^ 2
exact ⟨h_sqrt_ge, h_sqrt_xh, h_rpow_32, h_rpow_34⟩ All goals completed! 🐙
Helper bounds on Real.log T and Real.log 6.
lemma log_T_and_six_bounds {L S T : ℝ}
(hL : (851 / 100 : ℝ) ≤ L) (hS_pos : 0 < S) (hS_log : Real.log S = L / 2)
(h6_le_T : 6 ≤ T) (hT_def : T = (3 / 2 : ℝ) * S / L) :
0 ≤ Real.log T ∧ Real.log T ≤ L / 2 - 429 / 250 ∧ (89 / 50 : ℝ) ≤ Real.log 6 := by L:ℝS:ℝT:ℝhL:851 / 100 ≤ LhS_pos:0 < ShS_log:log S = L / 2h6_le_T:6 ≤ ThT_def:T = 3 / 2 * S / L⊢ 0 ≤ log T ∧ log T ≤ L / 2 - 429 / 250 ∧ 89 / 50 ≤ log 6
have hL_pos : 0 < L := by linarith L:ℝS:ℝT:ℝhL:851 / 100 ≤ LhS_pos:0 < ShS_log:log S = L / 2h6_le_T:6 ≤ ThT_def:T = 3 / 2 * S / LhL_pos:0 < L⊢ 0 ≤ log T ∧ log T ≤ L / 2 - 429 / 250 ∧ 89 / 50 ≤ log 6
have h_logL : (533 / 250 : ℝ) ≤ Real.log L := by
have hpow : (2 : ℝ) ^ (40 : ℕ) ≤ L ^ (13 : ℕ) := by L:ℝS:ℝT:ℝhL:851 / 100 ≤ LhS_pos:0 < ShS_log:log S = L / 2h6_le_T:6 ≤ ThT_def:T = 3 / 2 * S / L⊢ 0 ≤ log T ∧ log T ≤ L / 2 - 429 / 250 ∧ 89 / 50 ≤ log 6
have h1 : (2 : ℝ) ^ (40 : ℕ) ≤ (851 / 100 : ℝ) ^ (13 : ℕ) := by L:ℝS:ℝT:ℝhL:851 / 100 ≤ LhS_pos:0 < ShS_log:log S = L / 2h6_le_T:6 ≤ ThT_def:T = 3 / 2 * S / L⊢ 0 ≤ log T ∧ log T ≤ L / 2 - 429 / 250 ∧ 89 / 50 ≤ log 6 norm_num L:ℝS:ℝT:ℝhL:851 / 100 ≤ LhS_pos:0 < ShS_log:log S = L / 2h6_le_T:6 ≤ ThT_def:T = 3 / 2 * S / LhL_pos:0 < Lh1:2 ^ 40 ≤ (851 / 100) ^ 13⊢ 2 ^ 40 ≤ L ^ 13
have h2 : (851 / 100 : ℝ) ^ (13 : ℕ) ≤ L ^ (13 : ℕ) :=
pow_le_pow_left₀ (by L:ℝS:ℝT:ℝhL:851 / 100 ≤ LhS_pos:0 < ShS_log:log S = L / 2h6_le_T:6 ≤ ThT_def:T = 3 / 2 * S / LhL_pos:0 < Lh1:2 ^ 40 ≤ (851 / 100) ^ 13⊢ 0 ≤ 851 / 100 norm_num All goals completed! 🐙) hL 13 L:ℝS:ℝT:ℝhL:851 / 100 ≤ LhS_pos:0 < ShS_log:log S = L / 2h6_le_T:6 ≤ ThT_def:T = 3 / 2 * S / LhL_pos:0 < Lh1:2 ^ 40 ≤ (851 / 100) ^ 13h2:(851 / 100) ^ 13 ≤ L ^ 13⊢ 2 ^ 40 ≤ L ^ 13
exact h1.trans h2 L:ℝS:ℝT:ℝhL:851 / 100 ≤ LhS_pos:0 < ShS_log:log S = L / 2h6_le_T:6 ≤ ThT_def:T = 3 / 2 * S / LhL_pos:0 < Lhpow:2 ^ 40 ≤ L ^ 13⊢ 533 / 250 ≤ log L
have hlog := Real.log_le_log (by L:ℝS:ℝT:ℝhL:851 / 100 ≤ LhS_pos:0 < ShS_log:log S = L / 2h6_le_T:6 ≤ ThT_def:T = 3 / 2 * S / LhL_pos:0 < Lhpow:2 ^ 40 ≤ L ^ 13⊢ 0 < 2 ^ 40 positivity All goals completed! 🐙) hpow L:ℝS:ℝT:ℝhL:851 / 100 ≤ LhS_pos:0 < ShS_log:log S = L / 2h6_le_T:6 ≤ ThT_def:T = 3 / 2 * S / LhL_pos:0 < Lhpow:2 ^ 40 ≤ L ^ 13hlog:log (2 ^ 40) ≤ log (L ^ 13)⊢ 533 / 250 ≤ log L
rw [Real.log_pow, L:ℝS:ℝT:ℝhL:851 / 100 ≤ LhS_pos:0 < ShS_log:log S = L / 2h6_le_T:6 ≤ ThT_def:T = 3 / 2 * S / LhL_pos:0 < Lhpow:2 ^ 40 ≤ L ^ 13hlog:↑40 * log 2 ≤ log (L ^ 13)⊢ 533 / 250 ≤ log L Real.log_pow L:ℝS:ℝT:ℝhL:851 / 100 ≤ LhS_pos:0 < ShS_log:log S = L / 2h6_le_T:6 ≤ ThT_def:T = 3 / 2 * S / LhL_pos:0 < Lhpow:2 ^ 40 ≤ L ^ 13hlog:↑40 * log 2 ≤ ↑13 * log L⊢ 533 / 250 ≤ log L] at hlog L:ℝS:ℝT:ℝhL:851 / 100 ≤ LhS_pos:0 < ShS_log:log S = L / 2h6_le_T:6 ≤ ThT_def:T = 3 / 2 * S / LhL_pos:0 < Lhpow:2 ^ 40 ≤ L ^ 13hlog:↑40 * log 2 ≤ ↑13 * log L⊢ 533 / 250 ≤ log L
have hlog2 := Real.log_two_gt_d9 L:ℝS:ℝT:ℝhL:851 / 100 ≤ LhS_pos:0 < ShS_log:log S = L / 2h6_le_T:6 ≤ ThT_def:T = 3 / 2 * S / LhL_pos:0 < Lhpow:2 ^ 40 ≤ L ^ 13hlog:↑40 * log 2 ≤ ↑13 * log Lhlog2:0.6931471803 < log 2⊢ 533 / 250 ≤ log L
push_cast at hlog L:ℝS:ℝT:ℝhL:851 / 100 ≤ LhS_pos:0 < ShS_log:log S = L / 2h6_le_T:6 ≤ ThT_def:T = 3 / 2 * S / LhL_pos:0 < Lhpow:2 ^ 40 ≤ L ^ 13hlog:40 * log 2 ≤ 13 * log Lhlog2:0.6931471803 < log 2⊢ 533 / 250 ≤ log L
linarith L:ℝS:ℝT:ℝhL:851 / 100 ≤ LhS_pos:0 < ShS_log:log S = L / 2h6_le_T:6 ≤ ThT_def:T = 3 / 2 * S / LhL_pos:0 < Lh_logL:533 / 250 ≤ log L⊢ 0 ≤ log T ∧ log T ≤ L / 2 - 429 / 250 ∧ 89 / 50 ≤ log 6
have h_log32 : Real.log (3 / 2 : ℝ) ≤ 52 / 125 := by
have hpow : ((3 / 2 : ℝ) ^ (5 : ℕ)) ≤ (2 : ℝ) ^ (3 : ℕ) := by L:ℝS:ℝT:ℝhL:851 / 100 ≤ LhS_pos:0 < ShS_log:log S = L / 2h6_le_T:6 ≤ ThT_def:T = 3 / 2 * S / L⊢ 0 ≤ log T ∧ log T ≤ L / 2 - 429 / 250 ∧ 89 / 50 ≤ log 6 norm_num L:ℝS:ℝT:ℝhL:851 / 100 ≤ LhS_pos:0 < ShS_log:log S = L / 2h6_le_T:6 ≤ ThT_def:T = 3 / 2 * S / LhL_pos:0 < Lh_logL:533 / 250 ≤ log Lhpow:(3 / 2) ^ 5 ≤ 2 ^ 3⊢ log (3 / 2) ≤ 52 / 125
have hlog := Real.log_le_log (by L:ℝS:ℝT:ℝhL:851 / 100 ≤ LhS_pos:0 < ShS_log:log S = L / 2h6_le_T:6 ≤ ThT_def:T = 3 / 2 * S / LhL_pos:0 < Lh_logL:533 / 250 ≤ log Lhpow:(3 / 2) ^ 5 ≤ 2 ^ 3⊢ 0 < (3 / 2) ^ 5 positivity All goals completed! 🐙) hpow L:ℝS:ℝT:ℝhL:851 / 100 ≤ LhS_pos:0 < ShS_log:log S = L / 2h6_le_T:6 ≤ ThT_def:T = 3 / 2 * S / LhL_pos:0 < Lh_logL:533 / 250 ≤ log Lhpow:(3 / 2) ^ 5 ≤ 2 ^ 3hlog:log ((3 / 2) ^ 5) ≤ log (2 ^ 3)⊢ log (3 / 2) ≤ 52 / 125
rw [Real.log_pow, L:ℝS:ℝT:ℝhL:851 / 100 ≤ LhS_pos:0 < ShS_log:log S = L / 2h6_le_T:6 ≤ ThT_def:T = 3 / 2 * S / LhL_pos:0 < Lh_logL:533 / 250 ≤ log Lhpow:(3 / 2) ^ 5 ≤ 2 ^ 3hlog:↑5 * log (3 / 2) ≤ log (2 ^ 3)⊢ log (3 / 2) ≤ 52 / 125 Real.log_pow L:ℝS:ℝT:ℝhL:851 / 100 ≤ LhS_pos:0 < ShS_log:log S = L / 2h6_le_T:6 ≤ ThT_def:T = 3 / 2 * S / LhL_pos:0 < Lh_logL:533 / 250 ≤ log Lhpow:(3 / 2) ^ 5 ≤ 2 ^ 3hlog:↑5 * log (3 / 2) ≤ ↑3 * log 2⊢ log (3 / 2) ≤ 52 / 125] at hlog L:ℝS:ℝT:ℝhL:851 / 100 ≤ LhS_pos:0 < ShS_log:log S = L / 2h6_le_T:6 ≤ ThT_def:T = 3 / 2 * S / LhL_pos:0 < Lh_logL:533 / 250 ≤ log Lhpow:(3 / 2) ^ 5 ≤ 2 ^ 3hlog:↑5 * log (3 / 2) ≤ ↑3 * log 2⊢ log (3 / 2) ≤ 52 / 125
have hlog2 := Real.log_two_lt_d9 L:ℝS:ℝT:ℝhL:851 / 100 ≤ LhS_pos:0 < ShS_log:log S = L / 2h6_le_T:6 ≤ ThT_def:T = 3 / 2 * S / LhL_pos:0 < Lh_logL:533 / 250 ≤ log Lhpow:(3 / 2) ^ 5 ≤ 2 ^ 3hlog:↑5 * log (3 / 2) ≤ ↑3 * log 2hlog2:log 2 < 0.6931471808⊢ log (3 / 2) ≤ 52 / 125
push_cast at hlog L:ℝS:ℝT:ℝhL:851 / 100 ≤ LhS_pos:0 < ShS_log:log S = L / 2h6_le_T:6 ≤ ThT_def:T = 3 / 2 * S / LhL_pos:0 < Lh_logL:533 / 250 ≤ log Lhpow:(3 / 2) ^ 5 ≤ 2 ^ 3hlog:5 * log (3 / 2) ≤ 3 * log 2hlog2:log 2 < 0.6931471808⊢ log (3 / 2) ≤ 52 / 125
linarith L:ℝS:ℝT:ℝhL:851 / 100 ≤ LhS_pos:0 < ShS_log:log S = L / 2h6_le_T:6 ≤ ThT_def:T = 3 / 2 * S / LhL_pos:0 < Lh_logL:533 / 250 ≤ log Lh_log32:log (3 / 2) ≤ 52 / 125⊢ 0 ≤ log T ∧ log T ≤ L / 2 - 429 / 250 ∧ 89 / 50 ≤ log 6
have h_logT_eq : Real.log T = Real.log (3 / 2 : ℝ) + Real.log S - Real.log L := by
rw [hT_def, L:ℝS:ℝT:ℝhL:851 / 100 ≤ LhS_pos:0 < ShS_log:log S = L / 2h6_le_T:6 ≤ ThT_def:T = 3 / 2 * S / LhL_pos:0 < Lh_logL:533 / 250 ≤ log Lh_log32:log (3 / 2) ≤ 52 / 125⊢ log (3 / 2 * S / L) = log (3 / 2) + log S - log L Real.log_div (by L:ℝS:ℝT:ℝhL:851 / 100 ≤ LhS_pos:0 < ShS_log:log S = L / 2h6_le_T:6 ≤ ThT_def:T = 3 / 2 * S / LhL_pos:0 < Lh_logL:533 / 250 ≤ log Lh_log32:log (3 / 2) ≤ 52 / 125⊢ 3 / 2 * S ≠ 0 positivity All goals completed! 🐙) hL_pos.ne',
Real.log_mul (by L:ℝS:ℝT:ℝhL:851 / 100 ≤ LhS_pos:0 < ShS_log:log S = L / 2h6_le_T:6 ≤ ThT_def:T = 3 / 2 * S / LhL_pos:0 < Lh_logL:533 / 250 ≤ log Lh_log32:log (3 / 2) ≤ 52 / 125⊢ 3 / 2 ≠ 0 norm_num All goals completed! 🐙) hS_pos.ne'] L:ℝS:ℝT:ℝhL:851 / 100 ≤ LhS_pos:0 < ShS_log:log S = L / 2h6_le_T:6 ≤ ThT_def:T = 3 / 2 * S / LhL_pos:0 < Lh_logL:533 / 250 ≤ log Lh_log32:log (3 / 2) ≤ 52 / 125h_logT_eq:log T = log (3 / 2) + log S - log L⊢ 0 ≤ log T ∧ log T ≤ L / 2 - 429 / 250 ∧ 89 / 50 ≤ log 6
have h_logT_le : Real.log T ≤ L / 2 - 429 / 250 := by linarith L:ℝS:ℝT:ℝhL:851 / 100 ≤ LhS_pos:0 < ShS_log:log S = L / 2h6_le_T:6 ≤ ThT_def:T = 3 / 2 * S / LhL_pos:0 < Lh_logL:533 / 250 ≤ log Lh_log32:log (3 / 2) ≤ 52 / 125h_logT_eq:log T = log (3 / 2) + log S - log Lh_logT_le:log T ≤ L / 2 - 429 / 250⊢ 0 ≤ log T ∧ log T ≤ L / 2 - 429 / 250 ∧ 89 / 50 ≤ log 6
have h_logT_nonneg : 0 ≤ Real.log T := Real.log_nonneg (by L:ℝS:ℝT:ℝhL:851 / 100 ≤ LhS_pos:0 < ShS_log:log S = L / 2h6_le_T:6 ≤ ThT_def:T = 3 / 2 * S / LhL_pos:0 < Lh_logL:533 / 250 ≤ log Lh_log32:log (3 / 2) ≤ 52 / 125h_logT_eq:log T = log (3 / 2) + log S - log Lh_logT_le:log T ≤ L / 2 - 429 / 250⊢ 1 ≤ T linarith All goals completed! 🐙) L:ℝS:ℝT:ℝhL:851 / 100 ≤ LhS_pos:0 < ShS_log:log S = L / 2h6_le_T:6 ≤ ThT_def:T = 3 / 2 * S / LhL_pos:0 < Lh_logL:533 / 250 ≤ log Lh_log32:log (3 / 2) ≤ 52 / 125h_logT_eq:log T = log (3 / 2) + log S - log Lh_logT_le:log T ≤ L / 2 - 429 / 250h_logT_nonneg:0 ≤ log T⊢ 0 ≤ log T ∧ log T ≤ L / 2 - 429 / 250 ∧ 89 / 50 ≤ log 6
have h_log6_ge : (89 / 50 : ℝ) ≤ Real.log 6 := by
have hpow : (2 : ℝ) ^ (18 : ℕ) ≤ (6 : ℝ) ^ (7 : ℕ) := by L:ℝS:ℝT:ℝhL:851 / 100 ≤ LhS_pos:0 < ShS_log:log S = L / 2h6_le_T:6 ≤ ThT_def:T = 3 / 2 * S / L⊢ 0 ≤ log T ∧ log T ≤ L / 2 - 429 / 250 ∧ 89 / 50 ≤ log 6 norm_num L:ℝS:ℝT:ℝhL:851 / 100 ≤ LhS_pos:0 < ShS_log:log S = L / 2h6_le_T:6 ≤ ThT_def:T = 3 / 2 * S / LhL_pos:0 < Lh_logL:533 / 250 ≤ log Lh_log32:log (3 / 2) ≤ 52 / 125h_logT_eq:log T = log (3 / 2) + log S - log Lh_logT_le:log T ≤ L / 2 - 429 / 250h_logT_nonneg:0 ≤ log Thpow:2 ^ 18 ≤ 6 ^ 7⊢ 89 / 50 ≤ log 6
have hlog := Real.log_le_log (by L:ℝS:ℝT:ℝhL:851 / 100 ≤ LhS_pos:0 < ShS_log:log S = L / 2h6_le_T:6 ≤ ThT_def:T = 3 / 2 * S / LhL_pos:0 < Lh_logL:533 / 250 ≤ log Lh_log32:log (3 / 2) ≤ 52 / 125h_logT_eq:log T = log (3 / 2) + log S - log Lh_logT_le:log T ≤ L / 2 - 429 / 250h_logT_nonneg:0 ≤ log Thpow:2 ^ 18 ≤ 6 ^ 7⊢ 0 < 2 ^ 18 positivity All goals completed! 🐙) hpow L:ℝS:ℝT:ℝhL:851 / 100 ≤ LhS_pos:0 < ShS_log:log S = L / 2h6_le_T:6 ≤ ThT_def:T = 3 / 2 * S / LhL_pos:0 < Lh_logL:533 / 250 ≤ log Lh_log32:log (3 / 2) ≤ 52 / 125h_logT_eq:log T = log (3 / 2) + log S - log Lh_logT_le:log T ≤ L / 2 - 429 / 250h_logT_nonneg:0 ≤ log Thpow:2 ^ 18 ≤ 6 ^ 7hlog:log (2 ^ 18) ≤ log (6 ^ 7)⊢ 89 / 50 ≤ log 6
rw [Real.log_pow, L:ℝS:ℝT:ℝhL:851 / 100 ≤ LhS_pos:0 < ShS_log:log S = L / 2h6_le_T:6 ≤ ThT_def:T = 3 / 2 * S / LhL_pos:0 < Lh_logL:533 / 250 ≤ log Lh_log32:log (3 / 2) ≤ 52 / 125h_logT_eq:log T = log (3 / 2) + log S - log Lh_logT_le:log T ≤ L / 2 - 429 / 250h_logT_nonneg:0 ≤ log Thpow:2 ^ 18 ≤ 6 ^ 7hlog:↑18 * log 2 ≤ log (6 ^ 7)⊢ 89 / 50 ≤ log 6 Real.log_pow L:ℝS:ℝT:ℝhL:851 / 100 ≤ LhS_pos:0 < ShS_log:log S = L / 2h6_le_T:6 ≤ ThT_def:T = 3 / 2 * S / LhL_pos:0 < Lh_logL:533 / 250 ≤ log Lh_log32:log (3 / 2) ≤ 52 / 125h_logT_eq:log T = log (3 / 2) + log S - log Lh_logT_le:log T ≤ L / 2 - 429 / 250h_logT_nonneg:0 ≤ log Thpow:2 ^ 18 ≤ 6 ^ 7hlog:↑18 * log 2 ≤ ↑7 * log 6⊢ 89 / 50 ≤ log 6] at hlog L:ℝS:ℝT:ℝhL:851 / 100 ≤ LhS_pos:0 < ShS_log:log S = L / 2h6_le_T:6 ≤ ThT_def:T = 3 / 2 * S / LhL_pos:0 < Lh_logL:533 / 250 ≤ log Lh_log32:log (3 / 2) ≤ 52 / 125h_logT_eq:log T = log (3 / 2) + log S - log Lh_logT_le:log T ≤ L / 2 - 429 / 250h_logT_nonneg:0 ≤ log Thpow:2 ^ 18 ≤ 6 ^ 7hlog:↑18 * log 2 ≤ ↑7 * log 6⊢ 89 / 50 ≤ log 6
have hlog2 := Real.log_two_gt_d9 L:ℝS:ℝT:ℝhL:851 / 100 ≤ LhS_pos:0 < ShS_log:log S = L / 2h6_le_T:6 ≤ ThT_def:T = 3 / 2 * S / LhL_pos:0 < Lh_logL:533 / 250 ≤ log Lh_log32:log (3 / 2) ≤ 52 / 125h_logT_eq:log T = log (3 / 2) + log S - log Lh_logT_le:log T ≤ L / 2 - 429 / 250h_logT_nonneg:0 ≤ log Thpow:2 ^ 18 ≤ 6 ^ 7hlog:↑18 * log 2 ≤ ↑7 * log 6hlog2:0.6931471803 < log 2⊢ 89 / 50 ≤ log 6
push_cast at hlog L:ℝS:ℝT:ℝhL:851 / 100 ≤ LhS_pos:0 < ShS_log:log S = L / 2h6_le_T:6 ≤ ThT_def:T = 3 / 2 * S / LhL_pos:0 < Lh_logL:533 / 250 ≤ log Lh_log32:log (3 / 2) ≤ 52 / 125h_logT_eq:log T = log (3 / 2) + log S - log Lh_logT_le:log T ≤ L / 2 - 429 / 250h_logT_nonneg:0 ≤ log Thpow:2 ^ 18 ≤ 6 ^ 7hlog:18 * log 2 ≤ 7 * log 6hlog2:0.6931471803 < log 2⊢ 89 / 50 ≤ log 6
linarith L:ℝS:ℝT:ℝhL:851 / 100 ≤ LhS_pos:0 < ShS_log:log S = L / 2h6_le_T:6 ≤ ThT_def:T = 3 / 2 * S / LhL_pos:0 < Lh_logL:533 / 250 ≤ log Lh_log32:log (3 / 2) ≤ 52 / 125h_logT_eq:log T = log (3 / 2) + log S - log Lh_logT_le:log T ≤ L / 2 - 429 / 250h_logT_nonneg:0 ≤ log Th_log6_ge:89 / 50 ≤ log 6⊢ 0 ≤ log T ∧ log T ≤ L / 2 - 429 / 250 ∧ 89 / 50 ≤ log 6
exact ⟨h_logT_nonneg, h_logT_le, h_log6_ge⟩ All goals completed! 🐙
Helper bound for Term 2: Real.log (2 * Real.pi) ≤ (1 / 500) * S * L ^ 2.
lemma term2_bound {S L : ℝ} (hS : 70 ≤ S) (hL_sq : (7242 / 100 : ℝ) ≤ L ^ 2) :
Real.log (2 * Real.pi) ≤ (1 / 500 : ℝ) * S * L ^ 2 := by S:ℝL:ℝhS:70 ≤ ShL_sq:7242 / 100 ≤ L ^ 2⊢ log (2 * π) ≤ 1 / 500 * S * L ^ 2
have hpi : 2 * Real.pi ≤ 8 := by have := Real.pi_le_four S:ℝL:ℝhS:70 ≤ ShL_sq:7242 / 100 ≤ L ^ 2this:π ≤ 4⊢ 2 * π ≤ 8; linarith S:ℝL:ℝhS:70 ≤ ShL_sq:7242 / 100 ≤ L ^ 2hpi:2 * π ≤ 8⊢ log (2 * π) ≤ 1 / 500 * S * L ^ 2
have hlog_2pi : Real.log (2 * Real.pi) ≤ 2 * Real.pi - 1 :=
Real.log_le_sub_one_of_pos (by S:ℝL:ℝhS:70 ≤ ShL_sq:7242 / 100 ≤ L ^ 2hpi:2 * π ≤ 8⊢ 0 < 2 * π positivity All goals completed! 🐙) S:ℝL:ℝhS:70 ≤ ShL_sq:7242 / 100 ≤ L ^ 2hpi:2 * π ≤ 8hlog_2pi:log (2 * π) ≤ 2 * π - 1⊢ log (2 * π) ≤ 1 / 500 * S * L ^ 2
have hSL : 4000 ≤ S * L ^ 2 := by nlinarith S:ℝL:ℝhS:70 ≤ ShL_sq:7242 / 100 ≤ L ^ 2hpi:2 * π ≤ 8hlog_2pi:log (2 * π) ≤ 2 * π - 1hSL:4000 ≤ S * L ^ 2⊢ log (2 * π) ≤ 1 / 500 * S * L ^ 2
linarith All goals completed! 🐙Helper bound for Term 3 + Term 4 combined.
lemma term3_add_term4_bound {x h S L T : ℝ} (hS_pos : 0 < S) (hL : (851 / 100 : ℝ) ≤ L)
(hL_sq : (7242 / 100 : ℝ) ≤ L ^ 2) (hh_pos : 0 < h) (hT_pos : 0 < T)
(hh_def : h = (7 / 20 : ℝ) * S * L ^ 2) (hT_def : T = (3 / 2 : ℝ) * S / L)
(h_sqrt_ge : S ≤ Real.sqrt (x + h))
(h_sqrt_xh : Real.sqrt (x + h) ≤ (34 / 29 : ℝ) * S)
(h_rpow_32 : (x + h) ^ (3 / 2 : ℝ) ≤ (161 / 100 : ℝ) * S ^ 3)
(h_logT_nonneg : 0 ≤ Real.log T) (h_logT_le : Real.log T ≤ L / 2 - 429 / 250)
(h_log6_ge : (89 / 50 : ℝ) ≤ Real.log 6) :
Real.sqrt (x + h) *
((16 / 5 : ℝ) / 2 * (Real.log T) ^ 2 + ((16 / 5 : ℝ) + (11 / 5 : ℝ)) * Real.log T +
(11 / 5 : ℝ) + (0 : ℝ) / 6 -
(16 / 5 : ℝ) / 2 * (Real.log 6) ^ 2 - (11 / 5 : ℝ) * Real.log 6) +
(2 * (x + h) ^ (3 / 2 : ℝ) / h) *
((2 * (16 / 5 : ℝ) * Real.log T + 2 * (16 / 5 : ℝ) + 2 * (11 / 5 : ℝ)) / T +
2 * (0 : ℝ) / T ^ 2) ≤
(59 / 100 : ℝ) * S * L ^ 2 := by x:ℝh:ℝS:ℝL:ℝT:ℝhS_pos:0 < ShL:851 / 100 ≤ LhL_sq:7242 / 100 ≤ L ^ 2hh_pos:0 < hhT_pos:0 < Thh_def:h = 7 / 20 * S * L ^ 2hT_def:T = 3 / 2 * S / Lh_sqrt_ge:S ≤ √(x + h)h_sqrt_xh:√(x + h) ≤ 34 / 29 * Sh_rpow_32:(x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3h_logT_nonneg:0 ≤ log Th_logT_le:log T ≤ L / 2 - 429 / 250h_log6_ge:89 / 50 ≤ log 6⊢ √(x + h) *
(16 / 5 / 2 * log T ^ 2 + (16 / 5 + 11 / 5) * log T + 11 / 5 + 0 / 6 - 16 / 5 / 2 * log 6 ^ 2 - 11 / 5 * log 6) +
2 * (x + h) ^ (3 / 2) / h * ((2 * (16 / 5) * log T + 2 * (16 / 5) + 2 * (11 / 5)) / T + 2 * 0 / T ^ 2) ≤
59 / 100 * S * L ^ 2
have hL_pos : 0 < L := by linarith x:ℝh:ℝS:ℝL:ℝT:ℝhS_pos:0 < ShL:851 / 100 ≤ LhL_sq:7242 / 100 ≤ L ^ 2hh_pos:0 < hhT_pos:0 < Thh_def:h = 7 / 20 * S * L ^ 2hT_def:T = 3 / 2 * S / Lh_sqrt_ge:S ≤ √(x + h)h_sqrt_xh:√(x + h) ≤ 34 / 29 * Sh_rpow_32:(x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3h_logT_nonneg:0 ≤ log Th_logT_le:log T ≤ L / 2 - 429 / 250h_log6_ge:89 / 50 ≤ log 6hL_pos:0 < L⊢ √(x + h) *
(16 / 5 / 2 * log T ^ 2 + (16 / 5 + 11 / 5) * log T + 11 / 5 + 0 / 6 - 16 / 5 / 2 * log 6 ^ 2 - 11 / 5 * log 6) +
2 * (x + h) ^ (3 / 2) / h * ((2 * (16 / 5) * log T + 2 * (16 / 5) + 2 * (11 / 5)) / T + 2 * 0 / T ^ 2) ≤
59 / 100 * S * L ^ 2
-- Bound on Term 3
have h_sq_T : (Real.log T) ^ 2 ≤ (L / 2 - 429 / 250) ^ 2 :=
sq_le_sq' (by x:ℝh:ℝS:ℝL:ℝT:ℝhS_pos:0 < ShL:851 / 100 ≤ LhL_sq:7242 / 100 ≤ L ^ 2hh_pos:0 < hhT_pos:0 < Thh_def:h = 7 / 20 * S * L ^ 2hT_def:T = 3 / 2 * S / Lh_sqrt_ge:S ≤ √(x + h)h_sqrt_xh:√(x + h) ≤ 34 / 29 * Sh_rpow_32:(x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3h_logT_nonneg:0 ≤ log Th_logT_le:log T ≤ L / 2 - 429 / 250h_log6_ge:89 / 50 ≤ log 6hL_pos:0 < L⊢ -(L / 2 - 429 / 250) ≤ log T linarith All goals completed! 🐙) h_logT_le x:ℝh:ℝS:ℝL:ℝT:ℝhS_pos:0 < ShL:851 / 100 ≤ LhL_sq:7242 / 100 ≤ L ^ 2hh_pos:0 < hhT_pos:0 < Thh_def:h = 7 / 20 * S * L ^ 2hT_def:T = 3 / 2 * S / Lh_sqrt_ge:S ≤ √(x + h)h_sqrt_xh:√(x + h) ≤ 34 / 29 * Sh_rpow_32:(x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3h_logT_nonneg:0 ≤ log Th_logT_le:log T ≤ L / 2 - 429 / 250h_log6_ge:89 / 50 ≤ log 6hL_pos:0 < Lh_sq_T:log T ^ 2 ≤ (L / 2 - 429 / 250) ^ 2⊢ √(x + h) *
(16 / 5 / 2 * log T ^ 2 + (16 / 5 + 11 / 5) * log T + 11 / 5 + 0 / 6 - 16 / 5 / 2 * log 6 ^ 2 - 11 / 5 * log 6) +
2 * (x + h) ^ (3 / 2) / h * ((2 * (16 / 5) * log T + 2 * (16 / 5) + 2 * (11 / 5)) / T + 2 * 0 / T ^ 2) ≤
59 / 100 * S * L ^ 2
have h_sq_6 : (89 / 50 : ℝ) ^ 2 ≤ (Real.log 6) ^ 2 :=
sq_le_sq' (by x:ℝh:ℝS:ℝL:ℝT:ℝhS_pos:0 < ShL:851 / 100 ≤ LhL_sq:7242 / 100 ≤ L ^ 2hh_pos:0 < hhT_pos:0 < Thh_def:h = 7 / 20 * S * L ^ 2hT_def:T = 3 / 2 * S / Lh_sqrt_ge:S ≤ √(x + h)h_sqrt_xh:√(x + h) ≤ 34 / 29 * Sh_rpow_32:(x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3h_logT_nonneg:0 ≤ log Th_logT_le:log T ≤ L / 2 - 429 / 250h_log6_ge:89 / 50 ≤ log 6hL_pos:0 < Lh_sq_T:log T ^ 2 ≤ (L / 2 - 429 / 250) ^ 2⊢ -log 6 ≤ 89 / 50 linarith All goals completed! 🐙) h_log6_ge x:ℝh:ℝS:ℝL:ℝT:ℝhS_pos:0 < ShL:851 / 100 ≤ LhL_sq:7242 / 100 ≤ L ^ 2hh_pos:0 < hhT_pos:0 < Thh_def:h = 7 / 20 * S * L ^ 2hT_def:T = 3 / 2 * S / Lh_sqrt_ge:S ≤ √(x + h)h_sqrt_xh:√(x + h) ≤ 34 / 29 * Sh_rpow_32:(x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3h_logT_nonneg:0 ≤ log Th_logT_le:log T ≤ L / 2 - 429 / 250h_log6_ge:89 / 50 ≤ log 6hL_pos:0 < Lh_sq_T:log T ^ 2 ≤ (L / 2 - 429 / 250) ^ 2h_sq_6:(89 / 50) ^ 2 ≤ log 6 ^ 2⊢ √(x + h) *
(16 / 5 / 2 * log T ^ 2 + (16 / 5 + 11 / 5) * log T + 11 / 5 + 0 / 6 - 16 / 5 / 2 * log 6 ^ 2 - 11 / 5 * log 6) +
2 * (x + h) ^ (3 / 2) / h * ((2 * (16 / 5) * log T + 2 * (16 / 5) + 2 * (11 / 5)) / T + 2 * 0 / T ^ 2) ≤
59 / 100 * S * L ^ 2
have h_bracket3 :
(16 / 5 : ℝ) / 2 * (Real.log T) ^ 2 + ((16 / 5 : ℝ) + (11 / 5 : ℝ)) * Real.log T +
(11 / 5 : ℝ) + (0 : ℝ) / 6 -
(16 / 5 : ℝ) / 2 * (Real.log 6) ^ 2 - (11 / 5 : ℝ) * Real.log 6 ≤
(2 / 5 : ℝ) * L ^ 2 - 23 / 2 := by
nlinarith x:ℝh:ℝS:ℝL:ℝT:ℝhS_pos:0 < ShL:851 / 100 ≤ LhL_sq:7242 / 100 ≤ L ^ 2hh_pos:0 < hhT_pos:0 < Thh_def:h = 7 / 20 * S * L ^ 2hT_def:T = 3 / 2 * S / Lh_sqrt_ge:S ≤ √(x + h)h_sqrt_xh:√(x + h) ≤ 34 / 29 * Sh_rpow_32:(x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3h_logT_nonneg:0 ≤ log Th_logT_le:log T ≤ L / 2 - 429 / 250h_log6_ge:89 / 50 ≤ log 6hL_pos:0 < Lh_sq_T:log T ^ 2 ≤ (L / 2 - 429 / 250) ^ 2h_sq_6:(89 / 50) ^ 2 ≤ log 6 ^ 2h_bracket3:16 / 5 / 2 * log T ^ 2 + (16 / 5 + 11 / 5) * log T + 11 / 5 + 0 / 6 - 16 / 5 / 2 * log 6 ^ 2 - 11 / 5 * log 6 ≤
2 / 5 * L ^ 2 - 23 / 2⊢ √(x + h) *
(16 / 5 / 2 * log T ^ 2 + (16 / 5 + 11 / 5) * log T + 11 / 5 + 0 / 6 - 16 / 5 / 2 * log 6 ^ 2 - 11 / 5 * log 6) +
2 * (x + h) ^ (3 / 2) / h * ((2 * (16 / 5) * log T + 2 * (16 / 5) + 2 * (11 / 5)) / T + 2 * 0 / T ^ 2) ≤
59 / 100 * S * L ^ 2
have h_term3 :
Real.sqrt (x + h) *
((16 / 5 : ℝ) / 2 * (Real.log T) ^ 2 + ((16 / 5 : ℝ) + (11 / 5 : ℝ)) * Real.log T +
(11 / 5 : ℝ) + (0 : ℝ) / 6 -
(16 / 5 : ℝ) / 2 * (Real.log 6) ^ 2 - (11 / 5 : ℝ) * Real.log 6) ≤
(68 / 145 : ℝ) * S * L ^ 2 - (23 / 2 : ℝ) * S := by
have h1 := mul_le_mul_of_nonneg_left h_bracket3 (Real.sqrt_nonneg (x + h)) x:ℝh:ℝS:ℝL:ℝT:ℝhS_pos:0 < ShL:851 / 100 ≤ LhL_sq:7242 / 100 ≤ L ^ 2hh_pos:0 < hhT_pos:0 < Thh_def:h = 7 / 20 * S * L ^ 2hT_def:T = 3 / 2 * S / Lh_sqrt_ge:S ≤ √(x + h)h_sqrt_xh:√(x + h) ≤ 34 / 29 * Sh_rpow_32:(x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3h_logT_nonneg:0 ≤ log Th_logT_le:log T ≤ L / 2 - 429 / 250h_log6_ge:89 / 50 ≤ log 6hL_pos:0 < Lh_sq_T:log T ^ 2 ≤ (L / 2 - 429 / 250) ^ 2h_sq_6:(89 / 50) ^ 2 ≤ log 6 ^ 2h_bracket3:16 / 5 / 2 * log T ^ 2 + (16 / 5 + 11 / 5) * log T + 11 / 5 + 0 / 6 - 16 / 5 / 2 * log 6 ^ 2 - 11 / 5 * log 6 ≤
2 / 5 * L ^ 2 - 23 / 2h1:√(x + h) *
(16 / 5 / 2 * log T ^ 2 + (16 / 5 + 11 / 5) * log T + 11 / 5 + 0 / 6 - 16 / 5 / 2 * log 6 ^ 2 - 11 / 5 * log 6) ≤
√(x + h) * (2 / 5 * L ^ 2 - 23 / 2)⊢ √(x + h) *
(16 / 5 / 2 * log T ^ 2 + (16 / 5 + 11 / 5) * log T + 11 / 5 + 0 / 6 - 16 / 5 / 2 * log 6 ^ 2 - 11 / 5 * log 6) ≤
68 / 145 * S * L ^ 2 - 23 / 2 * S
have h2 : Real.sqrt (x + h) * ((2 / 5 : ℝ) * L ^ 2) ≤
((34 / 29 : ℝ) * S) * ((2 / 5 : ℝ) * L ^ 2) :=
mul_le_mul_of_nonneg_right h_sqrt_xh (by x:ℝh:ℝS:ℝL:ℝT:ℝhS_pos:0 < ShL:851 / 100 ≤ LhL_sq:7242 / 100 ≤ L ^ 2hh_pos:0 < hhT_pos:0 < Thh_def:h = 7 / 20 * S * L ^ 2hT_def:T = 3 / 2 * S / Lh_sqrt_ge:S ≤ √(x + h)h_sqrt_xh:√(x + h) ≤ 34 / 29 * Sh_rpow_32:(x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3h_logT_nonneg:0 ≤ log Th_logT_le:log T ≤ L / 2 - 429 / 250h_log6_ge:89 / 50 ≤ log 6hL_pos:0 < Lh_sq_T:log T ^ 2 ≤ (L / 2 - 429 / 250) ^ 2h_sq_6:(89 / 50) ^ 2 ≤ log 6 ^ 2h_bracket3:16 / 5 / 2 * log T ^ 2 + (16 / 5 + 11 / 5) * log T + 11 / 5 + 0 / 6 - 16 / 5 / 2 * log 6 ^ 2 - 11 / 5 * log 6 ≤
2 / 5 * L ^ 2 - 23 / 2h1:√(x + h) *
(16 / 5 / 2 * log T ^ 2 + (16 / 5 + 11 / 5) * log T + 11 / 5 + 0 / 6 - 16 / 5 / 2 * log 6 ^ 2 - 11 / 5 * log 6) ≤
√(x + h) * (2 / 5 * L ^ 2 - 23 / 2)⊢ 0 ≤ 2 / 5 * L ^ 2 positivity All goals completed! 🐙) x:ℝh:ℝS:ℝL:ℝT:ℝhS_pos:0 < ShL:851 / 100 ≤ LhL_sq:7242 / 100 ≤ L ^ 2hh_pos:0 < hhT_pos:0 < Thh_def:h = 7 / 20 * S * L ^ 2hT_def:T = 3 / 2 * S / Lh_sqrt_ge:S ≤ √(x + h)h_sqrt_xh:√(x + h) ≤ 34 / 29 * Sh_rpow_32:(x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3h_logT_nonneg:0 ≤ log Th_logT_le:log T ≤ L / 2 - 429 / 250h_log6_ge:89 / 50 ≤ log 6hL_pos:0 < Lh_sq_T:log T ^ 2 ≤ (L / 2 - 429 / 250) ^ 2h_sq_6:(89 / 50) ^ 2 ≤ log 6 ^ 2h_bracket3:16 / 5 / 2 * log T ^ 2 + (16 / 5 + 11 / 5) * log T + 11 / 5 + 0 / 6 - 16 / 5 / 2 * log 6 ^ 2 - 11 / 5 * log 6 ≤
2 / 5 * L ^ 2 - 23 / 2h1:√(x + h) *
(16 / 5 / 2 * log T ^ 2 + (16 / 5 + 11 / 5) * log T + 11 / 5 + 0 / 6 - 16 / 5 / 2 * log 6 ^ 2 - 11 / 5 * log 6) ≤
√(x + h) * (2 / 5 * L ^ 2 - 23 / 2)h2:√(x + h) * (2 / 5 * L ^ 2) ≤ 34 / 29 * S * (2 / 5 * L ^ 2)⊢ √(x + h) *
(16 / 5 / 2 * log T ^ 2 + (16 / 5 + 11 / 5) * log T + 11 / 5 + 0 / 6 - 16 / 5 / 2 * log 6 ^ 2 - 11 / 5 * log 6) ≤
68 / 145 * S * L ^ 2 - 23 / 2 * S
linarith x:ℝh:ℝS:ℝL:ℝT:ℝhS_pos:0 < ShL:851 / 100 ≤ LhL_sq:7242 / 100 ≤ L ^ 2hh_pos:0 < hhT_pos:0 < Thh_def:h = 7 / 20 * S * L ^ 2hT_def:T = 3 / 2 * S / Lh_sqrt_ge:S ≤ √(x + h)h_sqrt_xh:√(x + h) ≤ 34 / 29 * Sh_rpow_32:(x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3h_logT_nonneg:0 ≤ log Th_logT_le:log T ≤ L / 2 - 429 / 250h_log6_ge:89 / 50 ≤ log 6hL_pos:0 < Lh_sq_T:log T ^ 2 ≤ (L / 2 - 429 / 250) ^ 2h_sq_6:(89 / 50) ^ 2 ≤ log 6 ^ 2h_bracket3:16 / 5 / 2 * log T ^ 2 + (16 / 5 + 11 / 5) * log T + 11 / 5 + 0 / 6 - 16 / 5 / 2 * log 6 ^ 2 - 11 / 5 * log 6 ≤
2 / 5 * L ^ 2 - 23 / 2h_term3:√(x + h) *
(16 / 5 / 2 * log T ^ 2 + (16 / 5 + 11 / 5) * log T + 11 / 5 + 0 / 6 - 16 / 5 / 2 * log 6 ^ 2 - 11 / 5 * log 6) ≤
68 / 145 * S * L ^ 2 - 23 / 2 * S⊢ √(x + h) *
(16 / 5 / 2 * log T ^ 2 + (16 / 5 + 11 / 5) * log T + 11 / 5 + 0 / 6 - 16 / 5 / 2 * log 6 ^ 2 - 11 / 5 * log 6) +
2 * (x + h) ^ (3 / 2) / h * ((2 * (16 / 5) * log T + 2 * (16 / 5) + 2 * (11 / 5)) / T + 2 * 0 / T ^ 2) ≤
59 / 100 * S * L ^ 2
-- Bound on Term 4
have h_term4 :
(2 * (x + h) ^ (3 / 2 : ℝ) / h) *
((2 * (16 / 5 : ℝ) * Real.log T + 2 * (16 / 5 : ℝ) + 2 * (11 / 5 : ℝ)) / T +
2 * (0 : ℝ) / T ^ 2) ≤
(99 / 5 : ℝ) * S := by
rw [mul_zero, x:ℝh:ℝS:ℝL:ℝT:ℝhS_pos:0 < ShL:851 / 100 ≤ LhL_sq:7242 / 100 ≤ L ^ 2hh_pos:0 < hhT_pos:0 < Thh_def:h = 7 / 20 * S * L ^ 2hT_def:T = 3 / 2 * S / Lh_sqrt_ge:S ≤ √(x + h)h_sqrt_xh:√(x + h) ≤ 34 / 29 * Sh_rpow_32:(x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3h_logT_nonneg:0 ≤ log Th_logT_le:log T ≤ L / 2 - 429 / 250h_log6_ge:89 / 50 ≤ log 6hL_pos:0 < Lh_sq_T:log T ^ 2 ≤ (L / 2 - 429 / 250) ^ 2h_sq_6:(89 / 50) ^ 2 ≤ log 6 ^ 2h_bracket3:16 / 5 / 2 * log T ^ 2 + (16 / 5 + 11 / 5) * log T + 11 / 5 + 0 / 6 - 16 / 5 / 2 * log 6 ^ 2 - 11 / 5 * log 6 ≤
2 / 5 * L ^ 2 - 23 / 2h_term3:√(x + h) *
(16 / 5 / 2 * log T ^ 2 + (16 / 5 + 11 / 5) * log T + 11 / 5 + 0 / 6 - 16 / 5 / 2 * log 6 ^ 2 - 11 / 5 * log 6) ≤
68 / 145 * S * L ^ 2 - 23 / 2 * S⊢ 2 * (x + h) ^ (3 / 2) / h * ((2 * (16 / 5) * log T + 2 * (16 / 5) + 2 * (11 / 5)) / T + 0 / T ^ 2) ≤ 99 / 5 * S zero_div, x:ℝh:ℝS:ℝL:ℝT:ℝhS_pos:0 < ShL:851 / 100 ≤ LhL_sq:7242 / 100 ≤ L ^ 2hh_pos:0 < hhT_pos:0 < Thh_def:h = 7 / 20 * S * L ^ 2hT_def:T = 3 / 2 * S / Lh_sqrt_ge:S ≤ √(x + h)h_sqrt_xh:√(x + h) ≤ 34 / 29 * Sh_rpow_32:(x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3h_logT_nonneg:0 ≤ log Th_logT_le:log T ≤ L / 2 - 429 / 250h_log6_ge:89 / 50 ≤ log 6hL_pos:0 < Lh_sq_T:log T ^ 2 ≤ (L / 2 - 429 / 250) ^ 2h_sq_6:(89 / 50) ^ 2 ≤ log 6 ^ 2h_bracket3:16 / 5 / 2 * log T ^ 2 + (16 / 5 + 11 / 5) * log T + 11 / 5 + 0 / 6 - 16 / 5 / 2 * log 6 ^ 2 - 11 / 5 * log 6 ≤
2 / 5 * L ^ 2 - 23 / 2h_term3:√(x + h) *
(16 / 5 / 2 * log T ^ 2 + (16 / 5 + 11 / 5) * log T + 11 / 5 + 0 / 6 - 16 / 5 / 2 * log 6 ^ 2 - 11 / 5 * log 6) ≤
68 / 145 * S * L ^ 2 - 23 / 2 * S⊢ 2 * (x + h) ^ (3 / 2) / h * ((2 * (16 / 5) * log T + 2 * (16 / 5) + 2 * (11 / 5)) / T + 0) ≤ 99 / 5 * S add_zero, x:ℝh:ℝS:ℝL:ℝT:ℝhS_pos:0 < ShL:851 / 100 ≤ LhL_sq:7242 / 100 ≤ L ^ 2hh_pos:0 < hhT_pos:0 < Thh_def:h = 7 / 20 * S * L ^ 2hT_def:T = 3 / 2 * S / Lh_sqrt_ge:S ≤ √(x + h)h_sqrt_xh:√(x + h) ≤ 34 / 29 * Sh_rpow_32:(x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3h_logT_nonneg:0 ≤ log Th_logT_le:log T ≤ L / 2 - 429 / 250h_log6_ge:89 / 50 ≤ log 6hL_pos:0 < Lh_sq_T:log T ^ 2 ≤ (L / 2 - 429 / 250) ^ 2h_sq_6:(89 / 50) ^ 2 ≤ log 6 ^ 2h_bracket3:16 / 5 / 2 * log T ^ 2 + (16 / 5 + 11 / 5) * log T + 11 / 5 + 0 / 6 - 16 / 5 / 2 * log 6 ^ 2 - 11 / 5 * log 6 ≤
2 / 5 * L ^ 2 - 23 / 2h_term3:√(x + h) *
(16 / 5 / 2 * log T ^ 2 + (16 / 5 + 11 / 5) * log T + 11 / 5 + 0 / 6 - 16 / 5 / 2 * log 6 ^ 2 - 11 / 5 * log 6) ≤
68 / 145 * S * L ^ 2 - 23 / 2 * S⊢ 2 * (x + h) ^ (3 / 2) / h * ((2 * (16 / 5) * log T + 2 * (16 / 5) + 2 * (11 / 5)) / T) ≤ 99 / 5 * S div_mul_div_comm x:ℝh:ℝS:ℝL:ℝT:ℝhS_pos:0 < ShL:851 / 100 ≤ LhL_sq:7242 / 100 ≤ L ^ 2hh_pos:0 < hhT_pos:0 < Thh_def:h = 7 / 20 * S * L ^ 2hT_def:T = 3 / 2 * S / Lh_sqrt_ge:S ≤ √(x + h)h_sqrt_xh:√(x + h) ≤ 34 / 29 * Sh_rpow_32:(x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3h_logT_nonneg:0 ≤ log Th_logT_le:log T ≤ L / 2 - 429 / 250h_log6_ge:89 / 50 ≤ log 6hL_pos:0 < Lh_sq_T:log T ^ 2 ≤ (L / 2 - 429 / 250) ^ 2h_sq_6:(89 / 50) ^ 2 ≤ log 6 ^ 2h_bracket3:16 / 5 / 2 * log T ^ 2 + (16 / 5 + 11 / 5) * log T + 11 / 5 + 0 / 6 - 16 / 5 / 2 * log 6 ^ 2 - 11 / 5 * log 6 ≤
2 / 5 * L ^ 2 - 23 / 2h_term3:√(x + h) *
(16 / 5 / 2 * log T ^ 2 + (16 / 5 + 11 / 5) * log T + 11 / 5 + 0 / 6 - 16 / 5 / 2 * log 6 ^ 2 - 11 / 5 * log 6) ≤
68 / 145 * S * L ^ 2 - 23 / 2 * S⊢ 2 * (x + h) ^ (3 / 2) * (2 * (16 / 5) * log T + 2 * (16 / 5) + 2 * (11 / 5)) / (h * T) ≤ 99 / 5 * S] x:ℝh:ℝS:ℝL:ℝT:ℝhS_pos:0 < ShL:851 / 100 ≤ LhL_sq:7242 / 100 ≤ L ^ 2hh_pos:0 < hhT_pos:0 < Thh_def:h = 7 / 20 * S * L ^ 2hT_def:T = 3 / 2 * S / Lh_sqrt_ge:S ≤ √(x + h)h_sqrt_xh:√(x + h) ≤ 34 / 29 * Sh_rpow_32:(x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3h_logT_nonneg:0 ≤ log Th_logT_le:log T ≤ L / 2 - 429 / 250h_log6_ge:89 / 50 ≤ log 6hL_pos:0 < Lh_sq_T:log T ^ 2 ≤ (L / 2 - 429 / 250) ^ 2h_sq_6:(89 / 50) ^ 2 ≤ log 6 ^ 2h_bracket3:16 / 5 / 2 * log T ^ 2 + (16 / 5 + 11 / 5) * log T + 11 / 5 + 0 / 6 - 16 / 5 / 2 * log 6 ^ 2 - 11 / 5 * log 6 ≤
2 / 5 * L ^ 2 - 23 / 2h_term3:√(x + h) *
(16 / 5 / 2 * log T ^ 2 + (16 / 5 + 11 / 5) * log T + 11 / 5 + 0 / 6 - 16 / 5 / 2 * log 6 ^ 2 - 11 / 5 * log 6) ≤
68 / 145 * S * L ^ 2 - 23 / 2 * S⊢ 2 * (x + h) ^ (3 / 2) * (2 * (16 / 5) * log T + 2 * (16 / 5) + 2 * (11 / 5)) / (h * T) ≤ 99 / 5 * S
rw [div_le_iff₀ (mul_pos hh_pos hT_pos) x:ℝh:ℝS:ℝL:ℝT:ℝhS_pos:0 < ShL:851 / 100 ≤ LhL_sq:7242 / 100 ≤ L ^ 2hh_pos:0 < hhT_pos:0 < Thh_def:h = 7 / 20 * S * L ^ 2hT_def:T = 3 / 2 * S / Lh_sqrt_ge:S ≤ √(x + h)h_sqrt_xh:√(x + h) ≤ 34 / 29 * Sh_rpow_32:(x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3h_logT_nonneg:0 ≤ log Th_logT_le:log T ≤ L / 2 - 429 / 250h_log6_ge:89 / 50 ≤ log 6hL_pos:0 < Lh_sq_T:log T ^ 2 ≤ (L / 2 - 429 / 250) ^ 2h_sq_6:(89 / 50) ^ 2 ≤ log 6 ^ 2h_bracket3:16 / 5 / 2 * log T ^ 2 + (16 / 5 + 11 / 5) * log T + 11 / 5 + 0 / 6 - 16 / 5 / 2 * log 6 ^ 2 - 11 / 5 * log 6 ≤
2 / 5 * L ^ 2 - 23 / 2h_term3:√(x + h) *
(16 / 5 / 2 * log T ^ 2 + (16 / 5 + 11 / 5) * log T + 11 / 5 + 0 / 6 - 16 / 5 / 2 * log 6 ^ 2 - 11 / 5 * log 6) ≤
68 / 145 * S * L ^ 2 - 23 / 2 * S⊢ 2 * (x + h) ^ (3 / 2) * (2 * (16 / 5) * log T + 2 * (16 / 5) + 2 * (11 / 5)) ≤ 99 / 5 * S * (h * T)] x:ℝh:ℝS:ℝL:ℝT:ℝhS_pos:0 < ShL:851 / 100 ≤ LhL_sq:7242 / 100 ≤ L ^ 2hh_pos:0 < hhT_pos:0 < Thh_def:h = 7 / 20 * S * L ^ 2hT_def:T = 3 / 2 * S / Lh_sqrt_ge:S ≤ √(x + h)h_sqrt_xh:√(x + h) ≤ 34 / 29 * Sh_rpow_32:(x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3h_logT_nonneg:0 ≤ log Th_logT_le:log T ≤ L / 2 - 429 / 250h_log6_ge:89 / 50 ≤ log 6hL_pos:0 < Lh_sq_T:log T ^ 2 ≤ (L / 2 - 429 / 250) ^ 2h_sq_6:(89 / 50) ^ 2 ≤ log 6 ^ 2h_bracket3:16 / 5 / 2 * log T ^ 2 + (16 / 5 + 11 / 5) * log T + 11 / 5 + 0 / 6 - 16 / 5 / 2 * log 6 ^ 2 - 11 / 5 * log 6 ≤
2 / 5 * L ^ 2 - 23 / 2h_term3:√(x + h) *
(16 / 5 / 2 * log T ^ 2 + (16 / 5 + 11 / 5) * log T + 11 / 5 + 0 / 6 - 16 / 5 / 2 * log 6 ^ 2 - 11 / 5 * log 6) ≤
68 / 145 * S * L ^ 2 - 23 / 2 * S⊢ 2 * (x + h) ^ (3 / 2) * (2 * (16 / 5) * log T + 2 * (16 / 5) + 2 * (11 / 5)) ≤ 99 / 5 * S * (h * T)
have h_hT : h * T = (21 / 40 : ℝ) * S ^ 2 * L := by x:ℝh:ℝS:ℝL:ℝT:ℝhS_pos:0 < ShL:851 / 100 ≤ LhL_sq:7242 / 100 ≤ L ^ 2hh_pos:0 < hhT_pos:0 < Thh_def:h = 7 / 20 * S * L ^ 2hT_def:T = 3 / 2 * S / Lh_sqrt_ge:S ≤ √(x + h)h_sqrt_xh:√(x + h) ≤ 34 / 29 * Sh_rpow_32:(x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3h_logT_nonneg:0 ≤ log Th_logT_le:log T ≤ L / 2 - 429 / 250h_log6_ge:89 / 50 ≤ log 6⊢ √(x + h) *
(16 / 5 / 2 * log T ^ 2 + (16 / 5 + 11 / 5) * log T + 11 / 5 + 0 / 6 - 16 / 5 / 2 * log 6 ^ 2 - 11 / 5 * log 6) +
2 * (x + h) ^ (3 / 2) / h * ((2 * (16 / 5) * log T + 2 * (16 / 5) + 2 * (11 / 5)) / T + 2 * 0 / T ^ 2) ≤
59 / 100 * S * L ^ 2
rw [hh_def, x:ℝh:ℝS:ℝL:ℝT:ℝhS_pos:0 < ShL:851 / 100 ≤ LhL_sq:7242 / 100 ≤ L ^ 2hh_pos:0 < hhT_pos:0 < Thh_def:h = 7 / 20 * S * L ^ 2hT_def:T = 3 / 2 * S / Lh_sqrt_ge:S ≤ √(x + h)h_sqrt_xh:√(x + h) ≤ 34 / 29 * Sh_rpow_32:(x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3h_logT_nonneg:0 ≤ log Th_logT_le:log T ≤ L / 2 - 429 / 250h_log6_ge:89 / 50 ≤ log 6hL_pos:0 < Lh_sq_T:log T ^ 2 ≤ (L / 2 - 429 / 250) ^ 2h_sq_6:(89 / 50) ^ 2 ≤ log 6 ^ 2h_bracket3:16 / 5 / 2 * log T ^ 2 + (16 / 5 + 11 / 5) * log T + 11 / 5 + 0 / 6 - 16 / 5 / 2 * log 6 ^ 2 - 11 / 5 * log 6 ≤
2 / 5 * L ^ 2 - 23 / 2h_term3:√(x + h) *
(16 / 5 / 2 * log T ^ 2 + (16 / 5 + 11 / 5) * log T + 11 / 5 + 0 / 6 - 16 / 5 / 2 * log 6 ^ 2 - 11 / 5 * log 6) ≤
68 / 145 * S * L ^ 2 - 23 / 2 * S⊢ 7 / 20 * S * L ^ 2 * T = 21 / 40 * S ^ 2 * L hT_def x:ℝh:ℝS:ℝL:ℝT:ℝhS_pos:0 < ShL:851 / 100 ≤ LhL_sq:7242 / 100 ≤ L ^ 2hh_pos:0 < hhT_pos:0 < Thh_def:h = 7 / 20 * S * L ^ 2hT_def:T = 3 / 2 * S / Lh_sqrt_ge:S ≤ √(x + h)h_sqrt_xh:√(x + h) ≤ 34 / 29 * Sh_rpow_32:(x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3h_logT_nonneg:0 ≤ log Th_logT_le:log T ≤ L / 2 - 429 / 250h_log6_ge:89 / 50 ≤ log 6hL_pos:0 < Lh_sq_T:log T ^ 2 ≤ (L / 2 - 429 / 250) ^ 2h_sq_6:(89 / 50) ^ 2 ≤ log 6 ^ 2h_bracket3:16 / 5 / 2 * log T ^ 2 + (16 / 5 + 11 / 5) * log T + 11 / 5 + 0 / 6 - 16 / 5 / 2 * log 6 ^ 2 - 11 / 5 * log 6 ≤
2 / 5 * L ^ 2 - 23 / 2h_term3:√(x + h) *
(16 / 5 / 2 * log T ^ 2 + (16 / 5 + 11 / 5) * log T + 11 / 5 + 0 / 6 - 16 / 5 / 2 * log 6 ^ 2 - 11 / 5 * log 6) ≤
68 / 145 * S * L ^ 2 - 23 / 2 * S⊢ 7 / 20 * S * L ^ 2 * (3 / 2 * S / L) = 21 / 40 * S ^ 2 * L] x:ℝh:ℝS:ℝL:ℝT:ℝhS_pos:0 < ShL:851 / 100 ≤ LhL_sq:7242 / 100 ≤ L ^ 2hh_pos:0 < hhT_pos:0 < Thh_def:h = 7 / 20 * S * L ^ 2hT_def:T = 3 / 2 * S / Lh_sqrt_ge:S ≤ √(x + h)h_sqrt_xh:√(x + h) ≤ 34 / 29 * Sh_rpow_32:(x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3h_logT_nonneg:0 ≤ log Th_logT_le:log T ≤ L / 2 - 429 / 250h_log6_ge:89 / 50 ≤ log 6hL_pos:0 < Lh_sq_T:log T ^ 2 ≤ (L / 2 - 429 / 250) ^ 2h_sq_6:(89 / 50) ^ 2 ≤ log 6 ^ 2h_bracket3:16 / 5 / 2 * log T ^ 2 + (16 / 5 + 11 / 5) * log T + 11 / 5 + 0 / 6 - 16 / 5 / 2 * log 6 ^ 2 - 11 / 5 * log 6 ≤
2 / 5 * L ^ 2 - 23 / 2h_term3:√(x + h) *
(16 / 5 / 2 * log T ^ 2 + (16 / 5 + 11 / 5) * log T + 11 / 5 + 0 / 6 - 16 / 5 / 2 * log 6 ^ 2 - 11 / 5 * log 6) ≤
68 / 145 * S * L ^ 2 - 23 / 2 * S⊢ 7 / 20 * S * L ^ 2 * (3 / 2 * S / L) = 21 / 40 * S ^ 2 * L
field_simp [hL_pos.ne'] x:ℝh:ℝS:ℝL:ℝT:ℝhS_pos:0 < ShL:851 / 100 ≤ LhL_sq:7242 / 100 ≤ L ^ 2hh_pos:0 < hhT_pos:0 < Thh_def:h = 7 / 20 * S * L ^ 2hT_def:T = 3 / 2 * S / Lh_sqrt_ge:S ≤ √(x + h)h_sqrt_xh:√(x + h) ≤ 34 / 29 * Sh_rpow_32:(x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3h_logT_nonneg:0 ≤ log Th_logT_le:log T ≤ L / 2 - 429 / 250h_log6_ge:89 / 50 ≤ log 6hL_pos:0 < Lh_sq_T:log T ^ 2 ≤ (L / 2 - 429 / 250) ^ 2h_sq_6:(89 / 50) ^ 2 ≤ log 6 ^ 2h_bracket3:16 / 5 / 2 * log T ^ 2 + (16 / 5 + 11 / 5) * log T + 11 / 5 + 0 / 6 - 16 / 5 / 2 * log 6 ^ 2 - 11 / 5 * log 6 ≤
2 / 5 * L ^ 2 - 23 / 2h_term3:√(x + h) *
(16 / 5 / 2 * log T ^ 2 + (16 / 5 + 11 / 5) * log T + 11 / 5 + 0 / 6 - 16 / 5 / 2 * log 6 ^ 2 - 11 / 5 * log 6) ≤
68 / 145 * S * L ^ 2 - 23 / 2 * S⊢ 7 * 3 * 40 = 20 * 2 * 21
ring x:ℝh:ℝS:ℝL:ℝT:ℝhS_pos:0 < ShL:851 / 100 ≤ LhL_sq:7242 / 100 ≤ L ^ 2hh_pos:0 < hhT_pos:0 < Thh_def:h = 7 / 20 * S * L ^ 2hT_def:T = 3 / 2 * S / Lh_sqrt_ge:S ≤ √(x + h)h_sqrt_xh:√(x + h) ≤ 34 / 29 * Sh_rpow_32:(x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3h_logT_nonneg:0 ≤ log Th_logT_le:log T ≤ L / 2 - 429 / 250h_log6_ge:89 / 50 ≤ log 6hL_pos:0 < Lh_sq_T:log T ^ 2 ≤ (L / 2 - 429 / 250) ^ 2h_sq_6:(89 / 50) ^ 2 ≤ log 6 ^ 2h_bracket3:16 / 5 / 2 * log T ^ 2 + (16 / 5 + 11 / 5) * log T + 11 / 5 + 0 / 6 - 16 / 5 / 2 * log 6 ^ 2 - 11 / 5 * log 6 ≤
2 / 5 * L ^ 2 - 23 / 2h_term3:√(x + h) *
(16 / 5 / 2 * log T ^ 2 + (16 / 5 + 11 / 5) * log T + 11 / 5 + 0 / 6 - 16 / 5 / 2 * log 6 ^ 2 - 11 / 5 * log 6) ≤
68 / 145 * S * L ^ 2 - 23 / 2 * Sh_hT:h * T = 21 / 40 * S ^ 2 * L⊢ 2 * (x + h) ^ (3 / 2) * (2 * (16 / 5) * log T + 2 * (16 / 5) + 2 * (11 / 5)) ≤ 99 / 5 * S * (h * T)
rw [h_hT x:ℝh:ℝS:ℝL:ℝT:ℝhS_pos:0 < ShL:851 / 100 ≤ LhL_sq:7242 / 100 ≤ L ^ 2hh_pos:0 < hhT_pos:0 < Thh_def:h = 7 / 20 * S * L ^ 2hT_def:T = 3 / 2 * S / Lh_sqrt_ge:S ≤ √(x + h)h_sqrt_xh:√(x + h) ≤ 34 / 29 * Sh_rpow_32:(x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3h_logT_nonneg:0 ≤ log Th_logT_le:log T ≤ L / 2 - 429 / 250h_log6_ge:89 / 50 ≤ log 6hL_pos:0 < Lh_sq_T:log T ^ 2 ≤ (L / 2 - 429 / 250) ^ 2h_sq_6:(89 / 50) ^ 2 ≤ log 6 ^ 2h_bracket3:16 / 5 / 2 * log T ^ 2 + (16 / 5 + 11 / 5) * log T + 11 / 5 + 0 / 6 - 16 / 5 / 2 * log 6 ^ 2 - 11 / 5 * log 6 ≤
2 / 5 * L ^ 2 - 23 / 2h_term3:√(x + h) *
(16 / 5 / 2 * log T ^ 2 + (16 / 5 + 11 / 5) * log T + 11 / 5 + 0 / 6 - 16 / 5 / 2 * log 6 ^ 2 - 11 / 5 * log 6) ≤
68 / 145 * S * L ^ 2 - 23 / 2 * Sh_hT:h * T = 21 / 40 * S ^ 2 * L⊢ 2 * (x + h) ^ (3 / 2) * (2 * (16 / 5) * log T + 2 * (16 / 5) + 2 * (11 / 5)) ≤ 99 / 5 * S * (21 / 40 * S ^ 2 * L)] x:ℝh:ℝS:ℝL:ℝT:ℝhS_pos:0 < ShL:851 / 100 ≤ LhL_sq:7242 / 100 ≤ L ^ 2hh_pos:0 < hhT_pos:0 < Thh_def:h = 7 / 20 * S * L ^ 2hT_def:T = 3 / 2 * S / Lh_sqrt_ge:S ≤ √(x + h)h_sqrt_xh:√(x + h) ≤ 34 / 29 * Sh_rpow_32:(x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3h_logT_nonneg:0 ≤ log Th_logT_le:log T ≤ L / 2 - 429 / 250h_log6_ge:89 / 50 ≤ log 6hL_pos:0 < Lh_sq_T:log T ^ 2 ≤ (L / 2 - 429 / 250) ^ 2h_sq_6:(89 / 50) ^ 2 ≤ log 6 ^ 2h_bracket3:16 / 5 / 2 * log T ^ 2 + (16 / 5 + 11 / 5) * log T + 11 / 5 + 0 / 6 - 16 / 5 / 2 * log 6 ^ 2 - 11 / 5 * log 6 ≤
2 / 5 * L ^ 2 - 23 / 2h_term3:√(x + h) *
(16 / 5 / 2 * log T ^ 2 + (16 / 5 + 11 / 5) * log T + 11 / 5 + 0 / 6 - 16 / 5 / 2 * log 6 ^ 2 - 11 / 5 * log 6) ≤
68 / 145 * S * L ^ 2 - 23 / 2 * Sh_hT:h * T = 21 / 40 * S ^ 2 * L⊢ 2 * (x + h) ^ (3 / 2) * (2 * (16 / 5) * log T + 2 * (16 / 5) + 2 * (11 / 5)) ≤ 99 / 5 * S * (21 / 40 * S ^ 2 * L)
have h_num1 : 2 * (x + h) ^ (3 / 2 : ℝ) ≤ (161 / 50 : ℝ) * S ^ 3 := by x:ℝh:ℝS:ℝL:ℝT:ℝhS_pos:0 < ShL:851 / 100 ≤ LhL_sq:7242 / 100 ≤ L ^ 2hh_pos:0 < hhT_pos:0 < Thh_def:h = 7 / 20 * S * L ^ 2hT_def:T = 3 / 2 * S / Lh_sqrt_ge:S ≤ √(x + h)h_sqrt_xh:√(x + h) ≤ 34 / 29 * Sh_rpow_32:(x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3h_logT_nonneg:0 ≤ log Th_logT_le:log T ≤ L / 2 - 429 / 250h_log6_ge:89 / 50 ≤ log 6⊢ √(x + h) *
(16 / 5 / 2 * log T ^ 2 + (16 / 5 + 11 / 5) * log T + 11 / 5 + 0 / 6 - 16 / 5 / 2 * log 6 ^ 2 - 11 / 5 * log 6) +
2 * (x + h) ^ (3 / 2) / h * ((2 * (16 / 5) * log T + 2 * (16 / 5) + 2 * (11 / 5)) / T + 2 * 0 / T ^ 2) ≤
59 / 100 * S * L ^ 2 linarith x:ℝh:ℝS:ℝL:ℝT:ℝhS_pos:0 < ShL:851 / 100 ≤ LhL_sq:7242 / 100 ≤ L ^ 2hh_pos:0 < hhT_pos:0 < Thh_def:h = 7 / 20 * S * L ^ 2hT_def:T = 3 / 2 * S / Lh_sqrt_ge:S ≤ √(x + h)h_sqrt_xh:√(x + h) ≤ 34 / 29 * Sh_rpow_32:(x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3h_logT_nonneg:0 ≤ log Th_logT_le:log T ≤ L / 2 - 429 / 250h_log6_ge:89 / 50 ≤ log 6hL_pos:0 < Lh_sq_T:log T ^ 2 ≤ (L / 2 - 429 / 250) ^ 2h_sq_6:(89 / 50) ^ 2 ≤ log 6 ^ 2h_bracket3:16 / 5 / 2 * log T ^ 2 + (16 / 5 + 11 / 5) * log T + 11 / 5 + 0 / 6 - 16 / 5 / 2 * log 6 ^ 2 - 11 / 5 * log 6 ≤
2 / 5 * L ^ 2 - 23 / 2h_term3:√(x + h) *
(16 / 5 / 2 * log T ^ 2 + (16 / 5 + 11 / 5) * log T + 11 / 5 + 0 / 6 - 16 / 5 / 2 * log 6 ^ 2 - 11 / 5 * log 6) ≤
68 / 145 * S * L ^ 2 - 23 / 2 * Sh_hT:h * T = 21 / 40 * S ^ 2 * Lh_num1:2 * (x + h) ^ (3 / 2) ≤ 161 / 50 * S ^ 3⊢ 2 * (x + h) ^ (3 / 2) * (2 * (16 / 5) * log T + 2 * (16 / 5) + 2 * (11 / 5)) ≤ 99 / 5 * S * (21 / 40 * S ^ 2 * L)
have h_num2 : 2 * (16 / 5 : ℝ) * Real.log T + 2 * (16 / 5 : ℝ) + 2 * (11 / 5 : ℝ) ≤
(16 / 5 : ℝ) * L := by x:ℝh:ℝS:ℝL:ℝT:ℝhS_pos:0 < ShL:851 / 100 ≤ LhL_sq:7242 / 100 ≤ L ^ 2hh_pos:0 < hhT_pos:0 < Thh_def:h = 7 / 20 * S * L ^ 2hT_def:T = 3 / 2 * S / Lh_sqrt_ge:S ≤ √(x + h)h_sqrt_xh:√(x + h) ≤ 34 / 29 * Sh_rpow_32:(x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3h_logT_nonneg:0 ≤ log Th_logT_le:log T ≤ L / 2 - 429 / 250h_log6_ge:89 / 50 ≤ log 6⊢ √(x + h) *
(16 / 5 / 2 * log T ^ 2 + (16 / 5 + 11 / 5) * log T + 11 / 5 + 0 / 6 - 16 / 5 / 2 * log 6 ^ 2 - 11 / 5 * log 6) +
2 * (x + h) ^ (3 / 2) / h * ((2 * (16 / 5) * log T + 2 * (16 / 5) + 2 * (11 / 5)) / T + 2 * 0 / T ^ 2) ≤
59 / 100 * S * L ^ 2 linarith x:ℝh:ℝS:ℝL:ℝT:ℝhS_pos:0 < ShL:851 / 100 ≤ LhL_sq:7242 / 100 ≤ L ^ 2hh_pos:0 < hhT_pos:0 < Thh_def:h = 7 / 20 * S * L ^ 2hT_def:T = 3 / 2 * S / Lh_sqrt_ge:S ≤ √(x + h)h_sqrt_xh:√(x + h) ≤ 34 / 29 * Sh_rpow_32:(x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3h_logT_nonneg:0 ≤ log Th_logT_le:log T ≤ L / 2 - 429 / 250h_log6_ge:89 / 50 ≤ log 6hL_pos:0 < Lh_sq_T:log T ^ 2 ≤ (L / 2 - 429 / 250) ^ 2h_sq_6:(89 / 50) ^ 2 ≤ log 6 ^ 2h_bracket3:16 / 5 / 2 * log T ^ 2 + (16 / 5 + 11 / 5) * log T + 11 / 5 + 0 / 6 - 16 / 5 / 2 * log 6 ^ 2 - 11 / 5 * log 6 ≤
2 / 5 * L ^ 2 - 23 / 2h_term3:√(x + h) *
(16 / 5 / 2 * log T ^ 2 + (16 / 5 + 11 / 5) * log T + 11 / 5 + 0 / 6 - 16 / 5 / 2 * log 6 ^ 2 - 11 / 5 * log 6) ≤
68 / 145 * S * L ^ 2 - 23 / 2 * Sh_hT:h * T = 21 / 40 * S ^ 2 * Lh_num1:2 * (x + h) ^ (3 / 2) ≤ 161 / 50 * S ^ 3h_num2:2 * (16 / 5) * log T + 2 * (16 / 5) + 2 * (11 / 5) ≤ 16 / 5 * L⊢ 2 * (x + h) ^ (3 / 2) * (2 * (16 / 5) * log T + 2 * (16 / 5) + 2 * (11 / 5)) ≤ 99 / 5 * S * (21 / 40 * S ^ 2 * L)
have h_prod :
2 * (x + h) ^ (3 / 2 : ℝ) *
(2 * (16 / 5 : ℝ) * Real.log T + 2 * (16 / 5 : ℝ) + 2 * (11 / 5 : ℝ)) ≤
((161 / 50 : ℝ) * S ^ 3) * ((16 / 5 : ℝ) * L) :=
mul_le_mul h_num1 h_num2 (by x:ℝh:ℝS:ℝL:ℝT:ℝhS_pos:0 < ShL:851 / 100 ≤ LhL_sq:7242 / 100 ≤ L ^ 2hh_pos:0 < hhT_pos:0 < Thh_def:h = 7 / 20 * S * L ^ 2hT_def:T = 3 / 2 * S / Lh_sqrt_ge:S ≤ √(x + h)h_sqrt_xh:√(x + h) ≤ 34 / 29 * Sh_rpow_32:(x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3h_logT_nonneg:0 ≤ log Th_logT_le:log T ≤ L / 2 - 429 / 250h_log6_ge:89 / 50 ≤ log 6hL_pos:0 < Lh_sq_T:log T ^ 2 ≤ (L / 2 - 429 / 250) ^ 2h_sq_6:(89 / 50) ^ 2 ≤ log 6 ^ 2h_bracket3:16 / 5 / 2 * log T ^ 2 + (16 / 5 + 11 / 5) * log T + 11 / 5 + 0 / 6 - 16 / 5 / 2 * log 6 ^ 2 - 11 / 5 * log 6 ≤
2 / 5 * L ^ 2 - 23 / 2h_term3:√(x + h) *
(16 / 5 / 2 * log T ^ 2 + (16 / 5 + 11 / 5) * log T + 11 / 5 + 0 / 6 - 16 / 5 / 2 * log 6 ^ 2 - 11 / 5 * log 6) ≤
68 / 145 * S * L ^ 2 - 23 / 2 * Sh_hT:h * T = 21 / 40 * S ^ 2 * Lh_num1:2 * (x + h) ^ (3 / 2) ≤ 161 / 50 * S ^ 3h_num2:2 * (16 / 5) * log T + 2 * (16 / 5) + 2 * (11 / 5) ≤ 16 / 5 * L⊢ 0 ≤ 2 * (16 / 5) * log T + 2 * (16 / 5) + 2 * (11 / 5) positivity All goals completed! 🐙) (by x:ℝh:ℝS:ℝL:ℝT:ℝhS_pos:0 < ShL:851 / 100 ≤ LhL_sq:7242 / 100 ≤ L ^ 2hh_pos:0 < hhT_pos:0 < Thh_def:h = 7 / 20 * S * L ^ 2hT_def:T = 3 / 2 * S / Lh_sqrt_ge:S ≤ √(x + h)h_sqrt_xh:√(x + h) ≤ 34 / 29 * Sh_rpow_32:(x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3h_logT_nonneg:0 ≤ log Th_logT_le:log T ≤ L / 2 - 429 / 250h_log6_ge:89 / 50 ≤ log 6hL_pos:0 < Lh_sq_T:log T ^ 2 ≤ (L / 2 - 429 / 250) ^ 2h_sq_6:(89 / 50) ^ 2 ≤ log 6 ^ 2h_bracket3:16 / 5 / 2 * log T ^ 2 + (16 / 5 + 11 / 5) * log T + 11 / 5 + 0 / 6 - 16 / 5 / 2 * log 6 ^ 2 - 11 / 5 * log 6 ≤
2 / 5 * L ^ 2 - 23 / 2h_term3:√(x + h) *
(16 / 5 / 2 * log T ^ 2 + (16 / 5 + 11 / 5) * log T + 11 / 5 + 0 / 6 - 16 / 5 / 2 * log 6 ^ 2 - 11 / 5 * log 6) ≤
68 / 145 * S * L ^ 2 - 23 / 2 * Sh_hT:h * T = 21 / 40 * S ^ 2 * Lh_num1:2 * (x + h) ^ (3 / 2) ≤ 161 / 50 * S ^ 3h_num2:2 * (16 / 5) * log T + 2 * (16 / 5) + 2 * (11 / 5) ≤ 16 / 5 * L⊢ 0 ≤ 161 / 50 * S ^ 3 positivity All goals completed! 🐙) x:ℝh:ℝS:ℝL:ℝT:ℝhS_pos:0 < ShL:851 / 100 ≤ LhL_sq:7242 / 100 ≤ L ^ 2hh_pos:0 < hhT_pos:0 < Thh_def:h = 7 / 20 * S * L ^ 2hT_def:T = 3 / 2 * S / Lh_sqrt_ge:S ≤ √(x + h)h_sqrt_xh:√(x + h) ≤ 34 / 29 * Sh_rpow_32:(x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3h_logT_nonneg:0 ≤ log Th_logT_le:log T ≤ L / 2 - 429 / 250h_log6_ge:89 / 50 ≤ log 6hL_pos:0 < Lh_sq_T:log T ^ 2 ≤ (L / 2 - 429 / 250) ^ 2h_sq_6:(89 / 50) ^ 2 ≤ log 6 ^ 2h_bracket3:16 / 5 / 2 * log T ^ 2 + (16 / 5 + 11 / 5) * log T + 11 / 5 + 0 / 6 - 16 / 5 / 2 * log 6 ^ 2 - 11 / 5 * log 6 ≤
2 / 5 * L ^ 2 - 23 / 2h_term3:√(x + h) *
(16 / 5 / 2 * log T ^ 2 + (16 / 5 + 11 / 5) * log T + 11 / 5 + 0 / 6 - 16 / 5 / 2 * log 6 ^ 2 - 11 / 5 * log 6) ≤
68 / 145 * S * L ^ 2 - 23 / 2 * Sh_hT:h * T = 21 / 40 * S ^ 2 * Lh_num1:2 * (x + h) ^ (3 / 2) ≤ 161 / 50 * S ^ 3h_num2:2 * (16 / 5) * log T + 2 * (16 / 5) + 2 * (11 / 5) ≤ 16 / 5 * Lh_prod:2 * (x + h) ^ (3 / 2) * (2 * (16 / 5) * log T + 2 * (16 / 5) + 2 * (11 / 5)) ≤ 161 / 50 * S ^ 3 * (16 / 5 * L)⊢ 2 * (x + h) ^ (3 / 2) * (2 * (16 / 5) * log T + 2 * (16 / 5) + 2 * (11 / 5)) ≤ 99 / 5 * S * (21 / 40 * S ^ 2 * L)
have h_rhs :
((161 / 50 : ℝ) * S ^ 3) * ((16 / 5 : ℝ) * L) ≤
(99 / 5 : ℝ) * S * ((21 / 40 : ℝ) * S ^ 2 * L) := by x:ℝh:ℝS:ℝL:ℝT:ℝhS_pos:0 < ShL:851 / 100 ≤ LhL_sq:7242 / 100 ≤ L ^ 2hh_pos:0 < hhT_pos:0 < Thh_def:h = 7 / 20 * S * L ^ 2hT_def:T = 3 / 2 * S / Lh_sqrt_ge:S ≤ √(x + h)h_sqrt_xh:√(x + h) ≤ 34 / 29 * Sh_rpow_32:(x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3h_logT_nonneg:0 ≤ log Th_logT_le:log T ≤ L / 2 - 429 / 250h_log6_ge:89 / 50 ≤ log 6⊢ √(x + h) *
(16 / 5 / 2 * log T ^ 2 + (16 / 5 + 11 / 5) * log T + 11 / 5 + 0 / 6 - 16 / 5 / 2 * log 6 ^ 2 - 11 / 5 * log 6) +
2 * (x + h) ^ (3 / 2) / h * ((2 * (16 / 5) * log T + 2 * (16 / 5) + 2 * (11 / 5)) / T + 2 * 0 / T ^ 2) ≤
59 / 100 * S * L ^ 2
have h_diff :
(99 / 5 : ℝ) * S * ((21 / 40 : ℝ) * S ^ 2 * L) -
((161 / 50 : ℝ) * S ^ 3) * ((16 / 5 : ℝ) * L) =
(91 / 1000 : ℝ) * S ^ 3 * L := by x:ℝh:ℝS:ℝL:ℝT:ℝhS_pos:0 < ShL:851 / 100 ≤ LhL_sq:7242 / 100 ≤ L ^ 2hh_pos:0 < hhT_pos:0 < Thh_def:h = 7 / 20 * S * L ^ 2hT_def:T = 3 / 2 * S / Lh_sqrt_ge:S ≤ √(x + h)h_sqrt_xh:√(x + h) ≤ 34 / 29 * Sh_rpow_32:(x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3h_logT_nonneg:0 ≤ log Th_logT_le:log T ≤ L / 2 - 429 / 250h_log6_ge:89 / 50 ≤ log 6⊢ √(x + h) *
(16 / 5 / 2 * log T ^ 2 + (16 / 5 + 11 / 5) * log T + 11 / 5 + 0 / 6 - 16 / 5 / 2 * log 6 ^ 2 - 11 / 5 * log 6) +
2 * (x + h) ^ (3 / 2) / h * ((2 * (16 / 5) * log T + 2 * (16 / 5) + 2 * (11 / 5)) / T + 2 * 0 / T ^ 2) ≤
59 / 100 * S * L ^ 2 ring x:ℝh:ℝS:ℝL:ℝT:ℝhS_pos:0 < ShL:851 / 100 ≤ LhL_sq:7242 / 100 ≤ L ^ 2hh_pos:0 < hhT_pos:0 < Thh_def:h = 7 / 20 * S * L ^ 2hT_def:T = 3 / 2 * S / Lh_sqrt_ge:S ≤ √(x + h)h_sqrt_xh:√(x + h) ≤ 34 / 29 * Sh_rpow_32:(x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3h_logT_nonneg:0 ≤ log Th_logT_le:log T ≤ L / 2 - 429 / 250h_log6_ge:89 / 50 ≤ log 6hL_pos:0 < Lh_sq_T:log T ^ 2 ≤ (L / 2 - 429 / 250) ^ 2h_sq_6:(89 / 50) ^ 2 ≤ log 6 ^ 2h_bracket3:16 / 5 / 2 * log T ^ 2 + (16 / 5 + 11 / 5) * log T + 11 / 5 + 0 / 6 - 16 / 5 / 2 * log 6 ^ 2 - 11 / 5 * log 6 ≤
2 / 5 * L ^ 2 - 23 / 2h_term3:√(x + h) *
(16 / 5 / 2 * log T ^ 2 + (16 / 5 + 11 / 5) * log T + 11 / 5 + 0 / 6 - 16 / 5 / 2 * log 6 ^ 2 - 11 / 5 * log 6) ≤
68 / 145 * S * L ^ 2 - 23 / 2 * Sh_hT:h * T = 21 / 40 * S ^ 2 * Lh_num1:2 * (x + h) ^ (3 / 2) ≤ 161 / 50 * S ^ 3h_num2:2 * (16 / 5) * log T + 2 * (16 / 5) + 2 * (11 / 5) ≤ 16 / 5 * Lh_prod:2 * (x + h) ^ (3 / 2) * (2 * (16 / 5) * log T + 2 * (16 / 5) + 2 * (11 / 5)) ≤ 161 / 50 * S ^ 3 * (16 / 5 * L)h_diff:99 / 5 * S * (21 / 40 * S ^ 2 * L) - 161 / 50 * S ^ 3 * (16 / 5 * L) = 91 / 1000 * S ^ 3 * L⊢ 161 / 50 * S ^ 3 * (16 / 5 * L) ≤ 99 / 5 * S * (21 / 40 * S ^ 2 * L)
have : 0 ≤ (91 / 1000 : ℝ) * S ^ 3 * L := by x:ℝh:ℝS:ℝL:ℝT:ℝhS_pos:0 < ShL:851 / 100 ≤ LhL_sq:7242 / 100 ≤ L ^ 2hh_pos:0 < hhT_pos:0 < Thh_def:h = 7 / 20 * S * L ^ 2hT_def:T = 3 / 2 * S / Lh_sqrt_ge:S ≤ √(x + h)h_sqrt_xh:√(x + h) ≤ 34 / 29 * Sh_rpow_32:(x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3h_logT_nonneg:0 ≤ log Th_logT_le:log T ≤ L / 2 - 429 / 250h_log6_ge:89 / 50 ≤ log 6⊢ √(x + h) *
(16 / 5 / 2 * log T ^ 2 + (16 / 5 + 11 / 5) * log T + 11 / 5 + 0 / 6 - 16 / 5 / 2 * log 6 ^ 2 - 11 / 5 * log 6) +
2 * (x + h) ^ (3 / 2) / h * ((2 * (16 / 5) * log T + 2 * (16 / 5) + 2 * (11 / 5)) / T + 2 * 0 / T ^ 2) ≤
59 / 100 * S * L ^ 2 positivity x:ℝh:ℝS:ℝL:ℝT:ℝhS_pos:0 < ShL:851 / 100 ≤ LhL_sq:7242 / 100 ≤ L ^ 2hh_pos:0 < hhT_pos:0 < Thh_def:h = 7 / 20 * S * L ^ 2hT_def:T = 3 / 2 * S / Lh_sqrt_ge:S ≤ √(x + h)h_sqrt_xh:√(x + h) ≤ 34 / 29 * Sh_rpow_32:(x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3h_logT_nonneg:0 ≤ log Th_logT_le:log T ≤ L / 2 - 429 / 250h_log6_ge:89 / 50 ≤ log 6hL_pos:0 < Lh_sq_T:log T ^ 2 ≤ (L / 2 - 429 / 250) ^ 2h_sq_6:(89 / 50) ^ 2 ≤ log 6 ^ 2h_bracket3:16 / 5 / 2 * log T ^ 2 + (16 / 5 + 11 / 5) * log T + 11 / 5 + 0 / 6 - 16 / 5 / 2 * log 6 ^ 2 - 11 / 5 * log 6 ≤
2 / 5 * L ^ 2 - 23 / 2h_term3:√(x + h) *
(16 / 5 / 2 * log T ^ 2 + (16 / 5 + 11 / 5) * log T + 11 / 5 + 0 / 6 - 16 / 5 / 2 * log 6 ^ 2 - 11 / 5 * log 6) ≤
68 / 145 * S * L ^ 2 - 23 / 2 * Sh_hT:h * T = 21 / 40 * S ^ 2 * Lh_num1:2 * (x + h) ^ (3 / 2) ≤ 161 / 50 * S ^ 3h_num2:2 * (16 / 5) * log T + 2 * (16 / 5) + 2 * (11 / 5) ≤ 16 / 5 * Lh_prod:2 * (x + h) ^ (3 / 2) * (2 * (16 / 5) * log T + 2 * (16 / 5) + 2 * (11 / 5)) ≤ 161 / 50 * S ^ 3 * (16 / 5 * L)h_diff:99 / 5 * S * (21 / 40 * S ^ 2 * L) - 161 / 50 * S ^ 3 * (16 / 5 * L) = 91 / 1000 * S ^ 3 * Lthis:0 ≤ 91 / 1000 * S ^ 3 * L⊢ 161 / 50 * S ^ 3 * (16 / 5 * L) ≤ 99 / 5 * S * (21 / 40 * S ^ 2 * L)
linarith x:ℝh:ℝS:ℝL:ℝT:ℝhS_pos:0 < ShL:851 / 100 ≤ LhL_sq:7242 / 100 ≤ L ^ 2hh_pos:0 < hhT_pos:0 < Thh_def:h = 7 / 20 * S * L ^ 2hT_def:T = 3 / 2 * S / Lh_sqrt_ge:S ≤ √(x + h)h_sqrt_xh:√(x + h) ≤ 34 / 29 * Sh_rpow_32:(x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3h_logT_nonneg:0 ≤ log Th_logT_le:log T ≤ L / 2 - 429 / 250h_log6_ge:89 / 50 ≤ log 6hL_pos:0 < Lh_sq_T:log T ^ 2 ≤ (L / 2 - 429 / 250) ^ 2h_sq_6:(89 / 50) ^ 2 ≤ log 6 ^ 2h_bracket3:16 / 5 / 2 * log T ^ 2 + (16 / 5 + 11 / 5) * log T + 11 / 5 + 0 / 6 - 16 / 5 / 2 * log 6 ^ 2 - 11 / 5 * log 6 ≤
2 / 5 * L ^ 2 - 23 / 2h_term3:√(x + h) *
(16 / 5 / 2 * log T ^ 2 + (16 / 5 + 11 / 5) * log T + 11 / 5 + 0 / 6 - 16 / 5 / 2 * log 6 ^ 2 - 11 / 5 * log 6) ≤
68 / 145 * S * L ^ 2 - 23 / 2 * Sh_hT:h * T = 21 / 40 * S ^ 2 * Lh_num1:2 * (x + h) ^ (3 / 2) ≤ 161 / 50 * S ^ 3h_num2:2 * (16 / 5) * log T + 2 * (16 / 5) + 2 * (11 / 5) ≤ 16 / 5 * Lh_prod:2 * (x + h) ^ (3 / 2) * (2 * (16 / 5) * log T + 2 * (16 / 5) + 2 * (11 / 5)) ≤ 161 / 50 * S ^ 3 * (16 / 5 * L)h_rhs:161 / 50 * S ^ 3 * (16 / 5 * L) ≤ 99 / 5 * S * (21 / 40 * S ^ 2 * L)⊢ 2 * (x + h) ^ (3 / 2) * (2 * (16 / 5) * log T + 2 * (16 / 5) + 2 * (11 / 5)) ≤ 99 / 5 * S * (21 / 40 * S ^ 2 * L)
linarith x:ℝh:ℝS:ℝL:ℝT:ℝhS_pos:0 < ShL:851 / 100 ≤ LhL_sq:7242 / 100 ≤ L ^ 2hh_pos:0 < hhT_pos:0 < Thh_def:h = 7 / 20 * S * L ^ 2hT_def:T = 3 / 2 * S / Lh_sqrt_ge:S ≤ √(x + h)h_sqrt_xh:√(x + h) ≤ 34 / 29 * Sh_rpow_32:(x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3h_logT_nonneg:0 ≤ log Th_logT_le:log T ≤ L / 2 - 429 / 250h_log6_ge:89 / 50 ≤ log 6hL_pos:0 < Lh_sq_T:log T ^ 2 ≤ (L / 2 - 429 / 250) ^ 2h_sq_6:(89 / 50) ^ 2 ≤ log 6 ^ 2h_bracket3:16 / 5 / 2 * log T ^ 2 + (16 / 5 + 11 / 5) * log T + 11 / 5 + 0 / 6 - 16 / 5 / 2 * log 6 ^ 2 - 11 / 5 * log 6 ≤
2 / 5 * L ^ 2 - 23 / 2h_term3:√(x + h) *
(16 / 5 / 2 * log T ^ 2 + (16 / 5 + 11 / 5) * log T + 11 / 5 + 0 / 6 - 16 / 5 / 2 * log 6 ^ 2 - 11 / 5 * log 6) ≤
68 / 145 * S * L ^ 2 - 23 / 2 * Sh_term4:2 * (x + h) ^ (3 / 2) / h * ((2 * (16 / 5) * log T + 2 * (16 / 5) + 2 * (11 / 5)) / T + 2 * 0 / T ^ 2) ≤ 99 / 5 * S⊢ √(x + h) *
(16 / 5 / 2 * log T ^ 2 + (16 / 5 + 11 / 5) * log T + 11 / 5 + 0 / 6 - 16 / 5 / 2 * log 6 ^ 2 - 11 / 5 * log 6) +
2 * (x + h) ^ (3 / 2) / h * ((2 * (16 / 5) * log T + 2 * (16 / 5) + 2 * (11 / 5)) / T + 2 * 0 / T ^ 2) ≤
59 / 100 * S * L ^ 2
have hS_le_SL2 : (83 / 10 : ℝ) * S ≤ (59 / 100 - 68 / 145 : ℝ) * S * L ^ 2 := by
nlinarith x:ℝh:ℝS:ℝL:ℝT:ℝhS_pos:0 < ShL:851 / 100 ≤ LhL_sq:7242 / 100 ≤ L ^ 2hh_pos:0 < hhT_pos:0 < Thh_def:h = 7 / 20 * S * L ^ 2hT_def:T = 3 / 2 * S / Lh_sqrt_ge:S ≤ √(x + h)h_sqrt_xh:√(x + h) ≤ 34 / 29 * Sh_rpow_32:(x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3h_logT_nonneg:0 ≤ log Th_logT_le:log T ≤ L / 2 - 429 / 250h_log6_ge:89 / 50 ≤ log 6hL_pos:0 < Lh_sq_T:log T ^ 2 ≤ (L / 2 - 429 / 250) ^ 2h_sq_6:(89 / 50) ^ 2 ≤ log 6 ^ 2h_bracket3:16 / 5 / 2 * log T ^ 2 + (16 / 5 + 11 / 5) * log T + 11 / 5 + 0 / 6 - 16 / 5 / 2 * log 6 ^ 2 - 11 / 5 * log 6 ≤
2 / 5 * L ^ 2 - 23 / 2h_term3:√(x + h) *
(16 / 5 / 2 * log T ^ 2 + (16 / 5 + 11 / 5) * log T + 11 / 5 + 0 / 6 - 16 / 5 / 2 * log 6 ^ 2 - 11 / 5 * log 6) ≤
68 / 145 * S * L ^ 2 - 23 / 2 * Sh_term4:2 * (x + h) ^ (3 / 2) / h * ((2 * (16 / 5) * log T + 2 * (16 / 5) + 2 * (11 / 5)) / T + 2 * 0 / T ^ 2) ≤ 99 / 5 * ShS_le_SL2:83 / 10 * S ≤ (59 / 100 - 68 / 145) * S * L ^ 2⊢ √(x + h) *
(16 / 5 / 2 * log T ^ 2 + (16 / 5 + 11 / 5) * log T + 11 / 5 + 0 / 6 - 16 / 5 / 2 * log 6 ^ 2 - 11 / 5 * log 6) +
2 * (x + h) ^ (3 / 2) / h * ((2 * (16 / 5) * log T + 2 * (16 / 5) + 2 * (11 / 5)) / T + 2 * 0 / T ^ 2) ≤
59 / 100 * S * L ^ 2
linarith All goals completed! 🐙
Helper bound for Term 5: left-vertical line Re s = -1 / 4 contribution.
lemma term5_bound {x h S L : ℝ} (hS_pos : 0 < S) (hL_pos : 0 < L)
(hL_sq : (7242 / 100 : ℝ) ≤ L ^ 2) (hh_pos : 0 < h)
(hh_def : h = (7 / 20 : ℝ) * S * L ^ 2)
(h_rpow_34 : (x + h) ^ (3 / 4 : ℝ) ≤ (26 / 171 : ℝ) * S ^ 2) :
32 * (2 * (1 : ℝ) + (85 : ℝ)) / (Real.pi * h) * (x + h) ^ (3 / 4 : ℝ) ≤
(8 / 100 : ℝ) * S * L ^ 2 := by x:ℝh:ℝS:ℝL:ℝhS_pos:0 < ShL_pos:0 < LhL_sq:7242 / 100 ≤ L ^ 2hh_pos:0 < hhh_def:h = 7 / 20 * S * L ^ 2h_rpow_34:(x + h) ^ (3 / 4) ≤ 26 / 171 * S ^ 2⊢ 32 * (2 * 1 + 85) / (π * h) * (x + h) ^ (3 / 4) ≤ 8 / 100 * S * L ^ 2
rw [div_mul_eq_mul_div, x:ℝh:ℝS:ℝL:ℝhS_pos:0 < ShL_pos:0 < LhL_sq:7242 / 100 ≤ L ^ 2hh_pos:0 < hhh_def:h = 7 / 20 * S * L ^ 2h_rpow_34:(x + h) ^ (3 / 4) ≤ 26 / 171 * S ^ 2⊢ 32 * (2 * 1 + 85) * (x + h) ^ (3 / 4) / (π * h) ≤ 8 / 100 * S * L ^ 2 div_le_iff₀ (mul_pos Real.pi_pos hh_pos) x:ℝh:ℝS:ℝL:ℝhS_pos:0 < ShL_pos:0 < LhL_sq:7242 / 100 ≤ L ^ 2hh_pos:0 < hhh_def:h = 7 / 20 * S * L ^ 2h_rpow_34:(x + h) ^ (3 / 4) ≤ 26 / 171 * S ^ 2⊢ 32 * (2 * 1 + 85) * (x + h) ^ (3 / 4) ≤ 8 / 100 * S * L ^ 2 * (π * h)] x:ℝh:ℝS:ℝL:ℝhS_pos:0 < ShL_pos:0 < LhL_sq:7242 / 100 ≤ L ^ 2hh_pos:0 < hhh_def:h = 7 / 20 * S * L ^ 2h_rpow_34:(x + h) ^ (3 / 4) ≤ 26 / 171 * S ^ 2⊢ 32 * (2 * 1 + 85) * (x + h) ^ (3 / 4) ≤ 8 / 100 * S * L ^ 2 * (π * h)
have hpi_gt : (3 : ℝ) ≤ Real.pi := by x:ℝh:ℝS:ℝL:ℝhS_pos:0 < ShL_pos:0 < LhL_sq:7242 / 100 ≤ L ^ 2hh_pos:0 < hhh_def:h = 7 / 20 * S * L ^ 2h_rpow_34:(x + h) ^ (3 / 4) ≤ 26 / 171 * S ^ 2⊢ 32 * (2 * 1 + 85) / (π * h) * (x + h) ^ (3 / 4) ≤ 8 / 100 * S * L ^ 2
have h_sin : (1 / 2 : ℝ) < Real.pi / 6 := by x:ℝh:ℝS:ℝL:ℝhS_pos:0 < ShL_pos:0 < LhL_sq:7242 / 100 ≤ L ^ 2hh_pos:0 < hhh_def:h = 7 / 20 * S * L ^ 2h_rpow_34:(x + h) ^ (3 / 4) ≤ 26 / 171 * S ^ 2⊢ 32 * (2 * 1 + 85) / (π * h) * (x + h) ^ (3 / 4) ≤ 8 / 100 * S * L ^ 2
rw [← Real.sin_pi_div_six x:ℝh:ℝS:ℝL:ℝhS_pos:0 < ShL_pos:0 < LhL_sq:7242 / 100 ≤ L ^ 2hh_pos:0 < hhh_def:h = 7 / 20 * S * L ^ 2h_rpow_34:(x + h) ^ (3 / 4) ≤ 26 / 171 * S ^ 2⊢ sin (π / 6) < π / 6] x:ℝh:ℝS:ℝL:ℝhS_pos:0 < ShL_pos:0 < LhL_sq:7242 / 100 ≤ L ^ 2hh_pos:0 < hhh_def:h = 7 / 20 * S * L ^ 2h_rpow_34:(x + h) ^ (3 / 4) ≤ 26 / 171 * S ^ 2⊢ sin (π / 6) < π / 6
exact Real.sin_lt (by x:ℝh:ℝS:ℝL:ℝhS_pos:0 < ShL_pos:0 < LhL_sq:7242 / 100 ≤ L ^ 2hh_pos:0 < hhh_def:h = 7 / 20 * S * L ^ 2h_rpow_34:(x + h) ^ (3 / 4) ≤ 26 / 171 * S ^ 2⊢ 0 < π / 6 positivity All goals completed! 🐙) x:ℝh:ℝS:ℝL:ℝhS_pos:0 < ShL_pos:0 < LhL_sq:7242 / 100 ≤ L ^ 2hh_pos:0 < hhh_def:h = 7 / 20 * S * L ^ 2h_rpow_34:(x + h) ^ (3 / 4) ≤ 26 / 171 * S ^ 2h_sin:1 / 2 < π / 6⊢ 3 ≤ π
linarith x:ℝh:ℝS:ℝL:ℝhS_pos:0 < ShL_pos:0 < LhL_sq:7242 / 100 ≤ L ^ 2hh_pos:0 < hhh_def:h = 7 / 20 * S * L ^ 2h_rpow_34:(x + h) ^ (3 / 4) ≤ 26 / 171 * S ^ 2hpi_gt:3 ≤ π⊢ 32 * (2 * 1 + 85) * (x + h) ^ (3 / 4) ≤ 8 / 100 * S * L ^ 2 * (π * h)
have h_num : 32 * (2 * (1 : ℝ) + 85) * (x + h) ^ (3 / 4 : ℝ) ≤ (24128 / 57 : ℝ) * S ^ 2 := by x:ℝh:ℝS:ℝL:ℝhS_pos:0 < ShL_pos:0 < LhL_sq:7242 / 100 ≤ L ^ 2hh_pos:0 < hhh_def:h = 7 / 20 * S * L ^ 2h_rpow_34:(x + h) ^ (3 / 4) ≤ 26 / 171 * S ^ 2⊢ 32 * (2 * 1 + 85) / (π * h) * (x + h) ^ (3 / 4) ≤ 8 / 100 * S * L ^ 2
linarith x:ℝh:ℝS:ℝL:ℝhS_pos:0 < ShL_pos:0 < LhL_sq:7242 / 100 ≤ L ^ 2hh_pos:0 < hhh_def:h = 7 / 20 * S * L ^ 2h_rpow_34:(x + h) ^ (3 / 4) ≤ 26 / 171 * S ^ 2hpi_gt:3 ≤ πh_num:32 * (2 * 1 + 85) * (x + h) ^ (3 / 4) ≤ 24128 / 57 * S ^ 2⊢ 32 * (2 * 1 + 85) * (x + h) ^ (3 / 4) ≤ 8 / 100 * S * L ^ 2 * (π * h)
have h1 : (3 : ℝ) * h ≤ Real.pi * h :=
mul_le_mul_of_nonneg_right hpi_gt hh_pos.le x:ℝh:ℝS:ℝL:ℝhS_pos:0 < ShL_pos:0 < LhL_sq:7242 / 100 ≤ L ^ 2hh_pos:0 < hhh_def:h = 7 / 20 * S * L ^ 2h_rpow_34:(x + h) ^ (3 / 4) ≤ 26 / 171 * S ^ 2hpi_gt:3 ≤ πh_num:32 * (2 * 1 + 85) * (x + h) ^ (3 / 4) ≤ 24128 / 57 * S ^ 2h1:3 * h ≤ π * h⊢ 32 * (2 * 1 + 85) * (x + h) ^ (3 / 4) ≤ 8 / 100 * S * L ^ 2 * (π * h)
have h2 : (7242 / 100 : ℝ) ^ 2 ≤ (L ^ 2) ^ 2 :=
sq_le_sq' (by x:ℝh:ℝS:ℝL:ℝhS_pos:0 < ShL_pos:0 < LhL_sq:7242 / 100 ≤ L ^ 2hh_pos:0 < hhh_def:h = 7 / 20 * S * L ^ 2h_rpow_34:(x + h) ^ (3 / 4) ≤ 26 / 171 * S ^ 2hpi_gt:3 ≤ πh_num:32 * (2 * 1 + 85) * (x + h) ^ (3 / 4) ≤ 24128 / 57 * S ^ 2h1:3 * h ≤ π * h⊢ -L ^ 2 ≤ 7242 / 100 linarith All goals completed! 🐙) hL_sq x:ℝh:ℝS:ℝL:ℝhS_pos:0 < ShL_pos:0 < LhL_sq:7242 / 100 ≤ L ^ 2hh_pos:0 < hhh_def:h = 7 / 20 * S * L ^ 2h_rpow_34:(x + h) ^ (3 / 4) ≤ 26 / 171 * S ^ 2hpi_gt:3 ≤ πh_num:32 * (2 * 1 + 85) * (x + h) ^ (3 / 4) ≤ 24128 / 57 * S ^ 2h1:3 * h ≤ π * hh2:(7242 / 100) ^ 2 ≤ (L ^ 2) ^ 2⊢ 32 * (2 * 1 + 85) * (x + h) ^ (3 / 4) ≤ 8 / 100 * S * L ^ 2 * (π * h)
have h3 : (24128 / 57 : ℝ) * S ^ 2 ≤
(8 / 100 : ℝ) * S * L ^ 2 * ((3 : ℝ) * h) := by x:ℝh:ℝS:ℝL:ℝhS_pos:0 < ShL_pos:0 < LhL_sq:7242 / 100 ≤ L ^ 2hh_pos:0 < hhh_def:h = 7 / 20 * S * L ^ 2h_rpow_34:(x + h) ^ (3 / 4) ≤ 26 / 171 * S ^ 2⊢ 32 * (2 * 1 + 85) / (π * h) * (x + h) ^ (3 / 4) ≤ 8 / 100 * S * L ^ 2
rw [hh_def x:ℝh:ℝS:ℝL:ℝhS_pos:0 < ShL_pos:0 < LhL_sq:7242 / 100 ≤ L ^ 2hh_pos:0 < hhh_def:h = 7 / 20 * S * L ^ 2h_rpow_34:(x + h) ^ (3 / 4) ≤ 26 / 171 * S ^ 2hpi_gt:3 ≤ πh_num:32 * (2 * 1 + 85) * (x + h) ^ (3 / 4) ≤ 24128 / 57 * S ^ 2h1:3 * h ≤ π * hh2:(7242 / 100) ^ 2 ≤ (L ^ 2) ^ 2⊢ 24128 / 57 * S ^ 2 ≤ 8 / 100 * S * L ^ 2 * (3 * (7 / 20 * S * L ^ 2))] x:ℝh:ℝS:ℝL:ℝhS_pos:0 < ShL_pos:0 < LhL_sq:7242 / 100 ≤ L ^ 2hh_pos:0 < hhh_def:h = 7 / 20 * S * L ^ 2h_rpow_34:(x + h) ^ (3 / 4) ≤ 26 / 171 * S ^ 2hpi_gt:3 ≤ πh_num:32 * (2 * 1 + 85) * (x + h) ^ (3 / 4) ≤ 24128 / 57 * S ^ 2h1:3 * h ≤ π * hh2:(7242 / 100) ^ 2 ≤ (L ^ 2) ^ 2⊢ 24128 / 57 * S ^ 2 ≤ 8 / 100 * S * L ^ 2 * (3 * (7 / 20 * S * L ^ 2))
have h_diff :
(8 / 100 : ℝ) * S * L ^ 2 * ((3 : ℝ) * ((7 / 20 : ℝ) * S * L ^ 2)) -
(24128 / 57 : ℝ) * S ^ 2 =
S ^ 2 * ((21 / 250 : ℝ) * (L ^ 2) ^ 2 - 24128 / 57) := by x:ℝh:ℝS:ℝL:ℝhS_pos:0 < ShL_pos:0 < LhL_sq:7242 / 100 ≤ L ^ 2hh_pos:0 < hhh_def:h = 7 / 20 * S * L ^ 2h_rpow_34:(x + h) ^ (3 / 4) ≤ 26 / 171 * S ^ 2⊢ 32 * (2 * 1 + 85) / (π * h) * (x + h) ^ (3 / 4) ≤ 8 / 100 * S * L ^ 2 ring x:ℝh:ℝS:ℝL:ℝhS_pos:0 < ShL_pos:0 < LhL_sq:7242 / 100 ≤ L ^ 2hh_pos:0 < hhh_def:h = 7 / 20 * S * L ^ 2h_rpow_34:(x + h) ^ (3 / 4) ≤ 26 / 171 * S ^ 2hpi_gt:3 ≤ πh_num:32 * (2 * 1 + 85) * (x + h) ^ (3 / 4) ≤ 24128 / 57 * S ^ 2h1:3 * h ≤ π * hh2:(7242 / 100) ^ 2 ≤ (L ^ 2) ^ 2h_diff:8 / 100 * S * L ^ 2 * (3 * (7 / 20 * S * L ^ 2)) - 24128 / 57 * S ^ 2 = S ^ 2 * (21 / 250 * (L ^ 2) ^ 2 - 24128 / 57)⊢ 24128 / 57 * S ^ 2 ≤ 8 / 100 * S * L ^ 2 * (3 * (7 / 20 * S * L ^ 2))
have : 0 ≤ S ^ 2 * ((21 / 250 : ℝ) * (L ^ 2) ^ 2 - 24128 / 57) := by x:ℝh:ℝS:ℝL:ℝhS_pos:0 < ShL_pos:0 < LhL_sq:7242 / 100 ≤ L ^ 2hh_pos:0 < hhh_def:h = 7 / 20 * S * L ^ 2h_rpow_34:(x + h) ^ (3 / 4) ≤ 26 / 171 * S ^ 2⊢ 32 * (2 * 1 + 85) / (π * h) * (x + h) ^ (3 / 4) ≤ 8 / 100 * S * L ^ 2
have : 0 ≤ (21 / 250 : ℝ) * (L ^ 2) ^ 2 - 24128 / 57 := by x:ℝh:ℝS:ℝL:ℝhS_pos:0 < ShL_pos:0 < LhL_sq:7242 / 100 ≤ L ^ 2hh_pos:0 < hhh_def:h = 7 / 20 * S * L ^ 2h_rpow_34:(x + h) ^ (3 / 4) ≤ 26 / 171 * S ^ 2⊢ 32 * (2 * 1 + 85) / (π * h) * (x + h) ^ (3 / 4) ≤ 8 / 100 * S * L ^ 2 linarith x:ℝh:ℝS:ℝL:ℝhS_pos:0 < ShL_pos:0 < LhL_sq:7242 / 100 ≤ L ^ 2hh_pos:0 < hhh_def:h = 7 / 20 * S * L ^ 2h_rpow_34:(x + h) ^ (3 / 4) ≤ 26 / 171 * S ^ 2hpi_gt:3 ≤ πh_num:32 * (2 * 1 + 85) * (x + h) ^ (3 / 4) ≤ 24128 / 57 * S ^ 2h1:3 * h ≤ π * hh2:(7242 / 100) ^ 2 ≤ (L ^ 2) ^ 2h_diff:8 / 100 * S * L ^ 2 * (3 * (7 / 20 * S * L ^ 2)) - 24128 / 57 * S ^ 2 = S ^ 2 * (21 / 250 * (L ^ 2) ^ 2 - 24128 / 57)this:0 ≤ 21 / 250 * (L ^ 2) ^ 2 - 24128 / 57⊢ 0 ≤ S ^ 2 * (21 / 250 * (L ^ 2) ^ 2 - 24128 / 57)
positivity x:ℝh:ℝS:ℝL:ℝhS_pos:0 < ShL_pos:0 < LhL_sq:7242 / 100 ≤ L ^ 2hh_pos:0 < hhh_def:h = 7 / 20 * S * L ^ 2h_rpow_34:(x + h) ^ (3 / 4) ≤ 26 / 171 * S ^ 2hpi_gt:3 ≤ πh_num:32 * (2 * 1 + 85) * (x + h) ^ (3 / 4) ≤ 24128 / 57 * S ^ 2h1:3 * h ≤ π * hh2:(7242 / 100) ^ 2 ≤ (L ^ 2) ^ 2h_diff:8 / 100 * S * L ^ 2 * (3 * (7 / 20 * S * L ^ 2)) - 24128 / 57 * S ^ 2 = S ^ 2 * (21 / 250 * (L ^ 2) ^ 2 - 24128 / 57)this:0 ≤ S ^ 2 * (21 / 250 * (L ^ 2) ^ 2 - 24128 / 57)⊢ 24128 / 57 * S ^ 2 ≤ 8 / 100 * S * L ^ 2 * (3 * (7 / 20 * S * L ^ 2))
linarith x:ℝh:ℝS:ℝL:ℝhS_pos:0 < ShL_pos:0 < LhL_sq:7242 / 100 ≤ L ^ 2hh_pos:0 < hhh_def:h = 7 / 20 * S * L ^ 2h_rpow_34:(x + h) ^ (3 / 4) ≤ 26 / 171 * S ^ 2hpi_gt:3 ≤ πh_num:32 * (2 * 1 + 85) * (x + h) ^ (3 / 4) ≤ 24128 / 57 * S ^ 2h1:3 * h ≤ π * hh2:(7242 / 100) ^ 2 ≤ (L ^ 2) ^ 2h3:24128 / 57 * S ^ 2 ≤ 8 / 100 * S * L ^ 2 * (3 * h)⊢ 32 * (2 * 1 + 85) * (x + h) ^ (3 / 4) ≤ 8 / 100 * S * L ^ 2 * (π * h)
have h4 :
(8 / 100 : ℝ) * S * L ^ 2 * ((3 : ℝ) * h) ≤
(8 / 100 : ℝ) * S * L ^ 2 * (Real.pi * h) :=
mul_le_mul_of_nonneg_left h1 (by x:ℝh:ℝS:ℝL:ℝhS_pos:0 < ShL_pos:0 < LhL_sq:7242 / 100 ≤ L ^ 2hh_pos:0 < hhh_def:h = 7 / 20 * S * L ^ 2h_rpow_34:(x + h) ^ (3 / 4) ≤ 26 / 171 * S ^ 2hpi_gt:3 ≤ πh_num:32 * (2 * 1 + 85) * (x + h) ^ (3 / 4) ≤ 24128 / 57 * S ^ 2h1:3 * h ≤ π * hh2:(7242 / 100) ^ 2 ≤ (L ^ 2) ^ 2h3:24128 / 57 * S ^ 2 ≤ 8 / 100 * S * L ^ 2 * (3 * h)⊢ 0 ≤ 8 / 100 * S * L ^ 2 positivity All goals completed! 🐙) x:ℝh:ℝS:ℝL:ℝhS_pos:0 < ShL_pos:0 < LhL_sq:7242 / 100 ≤ L ^ 2hh_pos:0 < hhh_def:h = 7 / 20 * S * L ^ 2h_rpow_34:(x + h) ^ (3 / 4) ≤ 26 / 171 * S ^ 2hpi_gt:3 ≤ πh_num:32 * (2 * 1 + 85) * (x + h) ^ (3 / 4) ≤ 24128 / 57 * S ^ 2h1:3 * h ≤ π * hh2:(7242 / 100) ^ 2 ≤ (L ^ 2) ^ 2h3:24128 / 57 * S ^ 2 ≤ 8 / 100 * S * L ^ 2 * (3 * h)h4:8 / 100 * S * L ^ 2 * (3 * h) ≤ 8 / 100 * S * L ^ 2 * (π * h)⊢ 32 * (2 * 1 + 85) * (x + h) ^ (3 / 4) ≤ 8 / 100 * S * L ^ 2 * (π * h)
linarith All goals completed! 🐙
Main Large-x Inequality (x ≥ 5000):
For all x ≥ 5000, the explicit parameters h = (7 / 20) * √x * (log x)^2 and
T = (3 / 2) * √x / log x satisfy 1 ≤ x - h, 0 < h, 6 ≤ T, and the full explicit bound
is at most (7 / 8) * √x * (log x)^2.
theorem explicit_rhs_le_seven_eighths_of_five_thousand_le
{x : ℝ} (hx : 5000 ≤ x) :
let h := (7 / 20 : ℝ) * Real.sqrt x * (Real.log x) ^ 2
let T := (3 / 2 : ℝ) * Real.sqrt x / Real.log x
let a_rvM := (16 / 5 : ℝ)
let C := (11 / 5 : ℝ)
let D := (0 : ℝ)
let A := (1 : ℝ)
let B := (85 : ℝ)
(1 ≤ x - h ∧ 0 < h ∧ 6 ≤ T) ∧
h / 2 + Real.log (2 * Real.pi) +
Real.sqrt (x + h) *
(a_rvM / 2 * (Real.log T) ^ 2 + (a_rvM + C) * Real.log T + C + D / 6 -
a_rvM / 2 * (Real.log 6) ^ 2 - C * Real.log 6) +
(2 * (x + h) ^ (3 / 2 : ℝ) / h) *
((2 * a_rvM * Real.log T + 2 * a_rvM + 2 * C) / T + 2 * D / T ^ 2) +
32 * (2 * A + B) / (Real.pi * h) * (x + h) ^ (3 / 4 : ℝ) ≤
(7 / 8 : ℝ) * Real.sqrt x * (Real.log x) ^ 2 := by x:ℝhx:5000 ≤ x⊢ let h := 7 / 20 * √x * log x ^ 2;
let T := 3 / 2 * √x / log x;
let a_rvM := 16 / 5;
let C := 11 / 5;
let D := 0;
let A := 1;
let B := 85;
(1 ≤ x - h ∧ 0 < h ∧ 6 ≤ T) ∧
h / 2 + log (2 * π) +
√(x + h) * (a_rvM / 2 * log T ^ 2 + (a_rvM + C) * log T + C + D / 6 - a_rvM / 2 * log 6 ^ 2 - C * log 6) +
2 * (x + h) ^ (3 / 2) / h * ((2 * a_rvM * log T + 2 * a_rvM + 2 * C) / T + 2 * D / T ^ 2) +
32 * (2 * A + B) / (π * h) * (x + h) ^ (3 / 4) ≤
7 / 8 * √x * log x ^ 2
intro h T a_rvM C D A B x:ℝhx:5000 ≤ xh:ℝ := 7 / 20 * √x * log x ^ 2T:ℝ := 3 / 2 * √x / log xa_rvM:ℝ := 16 / 5C:ℝ := 11 / 5D:ℝ := 0A:ℝ := 1B:ℝ := 85⊢ (1 ≤ x - h ∧ 0 < h ∧ 6 ≤ T) ∧
h / 2 + log (2 * π) +
√(x + h) * (a_rvM / 2 * log T ^ 2 + (a_rvM + C) * log T + C + D / 6 - a_rvM / 2 * log 6 ^ 2 - C * log 6) +
2 * (x + h) ^ (3 / 2) / h * ((2 * a_rvM * log T + 2 * a_rvM + 2 * C) / T + 2 * D / T ^ 2) +
32 * (2 * A + B) / (π * h) * (x + h) ^ (3 / 4) ≤
7 / 8 * √x * log x ^ 2
set L : ℝ := Real.log x x:ℝhx:5000 ≤ xh:ℝ := 7 / 20 * √x * log x ^ 2T:ℝ := 3 / 2 * √x / log xa_rvM:ℝ := 16 / 5C:ℝ := 11 / 5D:ℝ := 0A:ℝ := 1B:ℝ := 85L:ℝ := log x⊢ (1 ≤ x - h ∧ 0 < h ∧ 6 ≤ T) ∧
h / 2 + log (2 * π) +
√(x + h) * (a_rvM / 2 * log T ^ 2 + (a_rvM + C) * log T + C + D / 6 - a_rvM / 2 * log 6 ^ 2 - C * log 6) +
2 * (x + h) ^ (3 / 2) / h * ((2 * a_rvM * log T + 2 * a_rvM + 2 * C) / T + 2 * D / T ^ 2) +
32 * (2 * A + B) / (π * h) * (x + h) ^ (3 / 4) ≤
7 / 8 * √x * L ^ 2
set S : ℝ := Real.sqrt x x:ℝhx:5000 ≤ xh:ℝ := 7 / 20 * √x * log x ^ 2T:ℝ := 3 / 2 * √x / log xa_rvM:ℝ := 16 / 5C:ℝ := 11 / 5D:ℝ := 0A:ℝ := 1B:ℝ := 85L:ℝ := log xS:ℝ := √x⊢ (1 ≤ x - h ∧ 0 < h ∧ 6 ≤ T) ∧
h / 2 + log (2 * π) +
√(x + h) * (a_rvM / 2 * log T ^ 2 + (a_rvM + C) * log T + C + D / 6 - a_rvM / 2 * log 6 ^ 2 - C * log 6) +
2 * (x + h) ^ (3 / 2) / h * ((2 * a_rvM * log T + 2 * a_rvM + 2 * C) / T + 2 * D / T ^ 2) +
32 * (2 * A + B) / (π * h) * (x + h) ^ (3 / 4) ≤
7 / 8 * S * L ^ 2
have hL : (851 / 100 : ℝ) ≤ L := log_ge_851_div_100 hx x:ℝhx:5000 ≤ xh:ℝ := 7 / 20 * √x * log x ^ 2T:ℝ := 3 / 2 * √x / log xa_rvM:ℝ := 16 / 5C:ℝ := 11 / 5D:ℝ := 0A:ℝ := 1B:ℝ := 85L:ℝ := log xS:ℝ := √xhL:851 / 100 ≤ L⊢ (1 ≤ x - h ∧ 0 < h ∧ 6 ≤ T) ∧
h / 2 + log (2 * π) +
√(x + h) * (a_rvM / 2 * log T ^ 2 + (a_rvM + C) * log T + C + D / 6 - a_rvM / 2 * log 6 ^ 2 - C * log 6) +
2 * (x + h) ^ (3 / 2) / h * ((2 * a_rvM * log T + 2 * a_rvM + 2 * C) / T + 2 * D / T ^ 2) +
32 * (2 * A + B) / (π * h) * (x + h) ^ (3 / 4) ≤
7 / 8 * S * L ^ 2
have hL_pos : 0 < L := by x:ℝhx:5000 ≤ x⊢ let h := 7 / 20 * √x * log x ^ 2;
let T := 3 / 2 * √x / log x;
let a_rvM := 16 / 5;
let C := 11 / 5;
let D := 0;
let A := 1;
let B := 85;
(1 ≤ x - h ∧ 0 < h ∧ 6 ≤ T) ∧
h / 2 + log (2 * π) +
√(x + h) * (a_rvM / 2 * log T ^ 2 + (a_rvM + C) * log T + C + D / 6 - a_rvM / 2 * log 6 ^ 2 - C * log 6) +
2 * (x + h) ^ (3 / 2) / h * ((2 * a_rvM * log T + 2 * a_rvM + 2 * C) / T + 2 * D / T ^ 2) +
32 * (2 * A + B) / (π * h) * (x + h) ^ (3 / 4) ≤
7 / 8 * √x * log x ^ 2 linarith x:ℝhx:5000 ≤ xh:ℝ := 7 / 20 * √x * log x ^ 2T:ℝ := 3 / 2 * √x / log xa_rvM:ℝ := 16 / 5C:ℝ := 11 / 5D:ℝ := 0A:ℝ := 1B:ℝ := 85L:ℝ := log xS:ℝ := √xhL:851 / 100 ≤ LhL_pos:0 < L⊢ (1 ≤ x - h ∧ 0 < h ∧ 6 ≤ T) ∧
h / 2 + log (2 * π) +
√(x + h) * (a_rvM / 2 * log T ^ 2 + (a_rvM + C) * log T + C + D / 6 - a_rvM / 2 * log 6 ^ 2 - C * log 6) +
2 * (x + h) ^ (3 / 2) / h * ((2 * a_rvM * log T + 2 * a_rvM + 2 * C) / T + 2 * D / T ^ 2) +
32 * (2 * A + B) / (π * h) * (x + h) ^ (3 / 4) ≤
7 / 8 * S * L ^ 2
have hL_sq : (7242 / 100 : ℝ) ≤ L ^ 2 := by x:ℝhx:5000 ≤ x⊢ let h := 7 / 20 * √x * log x ^ 2;
let T := 3 / 2 * √x / log x;
let a_rvM := 16 / 5;
let C := 11 / 5;
let D := 0;
let A := 1;
let B := 85;
(1 ≤ x - h ∧ 0 < h ∧ 6 ≤ T) ∧
h / 2 + log (2 * π) +
√(x + h) * (a_rvM / 2 * log T ^ 2 + (a_rvM + C) * log T + C + D / 6 - a_rvM / 2 * log 6 ^ 2 - C * log 6) +
2 * (x + h) ^ (3 / 2) / h * ((2 * a_rvM * log T + 2 * a_rvM + 2 * C) / T + 2 * D / T ^ 2) +
32 * (2 * A + B) / (π * h) * (x + h) ^ (3 / 4) ≤
7 / 8 * √x * log x ^ 2 nlinarith x:ℝhx:5000 ≤ xh:ℝ := 7 / 20 * √x * log x ^ 2T:ℝ := 3 / 2 * √x / log xa_rvM:ℝ := 16 / 5C:ℝ := 11 / 5D:ℝ := 0A:ℝ := 1B:ℝ := 85L:ℝ := log xS:ℝ := √xhL:851 / 100 ≤ LhL_pos:0 < LhL_sq:7242 / 100 ≤ L ^ 2⊢ (1 ≤ x - h ∧ 0 < h ∧ 6 ≤ T) ∧
h / 2 + log (2 * π) +
√(x + h) * (a_rvM / 2 * log T ^ 2 + (a_rvM + C) * log T + C + D / 6 - a_rvM / 2 * log 6 ^ 2 - C * log 6) +
2 * (x + h) ^ (3 / 2) / h * ((2 * a_rvM * log T + 2 * a_rvM + 2 * C) / T + 2 * D / T ^ 2) +
32 * (2 * A + B) / (π * h) * (x + h) ^ (3 / 4) ≤
7 / 8 * S * L ^ 2
have hS : (70 : ℝ) ≤ S := sqrt_ge_seventy hx x:ℝhx:5000 ≤ xh:ℝ := 7 / 20 * √x * log x ^ 2T:ℝ := 3 / 2 * √x / log xa_rvM:ℝ := 16 / 5C:ℝ := 11 / 5D:ℝ := 0A:ℝ := 1B:ℝ := 85L:ℝ := log xS:ℝ := √xhL:851 / 100 ≤ LhL_pos:0 < LhL_sq:7242 / 100 ≤ L ^ 2hS:70 ≤ S⊢ (1 ≤ x - h ∧ 0 < h ∧ 6 ≤ T) ∧
h / 2 + log (2 * π) +
√(x + h) * (a_rvM / 2 * log T ^ 2 + (a_rvM + C) * log T + C + D / 6 - a_rvM / 2 * log 6 ^ 2 - C * log 6) +
2 * (x + h) ^ (3 / 2) / h * ((2 * a_rvM * log T + 2 * a_rvM + 2 * C) / T + 2 * D / T ^ 2) +
32 * (2 * A + B) / (π * h) * (x + h) ^ (3 / 4) ≤
7 / 8 * S * L ^ 2
have hS_pos : 0 < S := by x:ℝhx:5000 ≤ x⊢ let h := 7 / 20 * √x * log x ^ 2;
let T := 3 / 2 * √x / log x;
let a_rvM := 16 / 5;
let C := 11 / 5;
let D := 0;
let A := 1;
let B := 85;
(1 ≤ x - h ∧ 0 < h ∧ 6 ≤ T) ∧
h / 2 + log (2 * π) +
√(x + h) * (a_rvM / 2 * log T ^ 2 + (a_rvM + C) * log T + C + D / 6 - a_rvM / 2 * log 6 ^ 2 - C * log 6) +
2 * (x + h) ^ (3 / 2) / h * ((2 * a_rvM * log T + 2 * a_rvM + 2 * C) / T + 2 * D / T ^ 2) +
32 * (2 * A + B) / (π * h) * (x + h) ^ (3 / 4) ≤
7 / 8 * √x * log x ^ 2 linarith x:ℝhx:5000 ≤ xh:ℝ := 7 / 20 * √x * log x ^ 2T:ℝ := 3 / 2 * √x / log xa_rvM:ℝ := 16 / 5C:ℝ := 11 / 5D:ℝ := 0A:ℝ := 1B:ℝ := 85L:ℝ := log xS:ℝ := √xhL:851 / 100 ≤ LhL_pos:0 < LhL_sq:7242 / 100 ≤ L ^ 2hS:70 ≤ ShS_pos:0 < S⊢ (1 ≤ x - h ∧ 0 < h ∧ 6 ≤ T) ∧
h / 2 + log (2 * π) +
√(x + h) * (a_rvM / 2 * log T ^ 2 + (a_rvM + C) * log T + C + D / 6 - a_rvM / 2 * log 6 ^ 2 - C * log 6) +
2 * (x + h) ^ (3 / 2) / h * ((2 * a_rvM * log T + 2 * a_rvM + 2 * C) / T + 2 * D / T ^ 2) +
32 * (2 * A + B) / (π * h) * (x + h) ^ (3 / 4) ≤
7 / 8 * S * L ^ 2
have hS_sq : S ^ 2 = x := Real.sq_sqrt (by x:ℝhx:5000 ≤ xh:ℝ := 7 / 20 * √x * log x ^ 2T:ℝ := 3 / 2 * √x / log xa_rvM:ℝ := 16 / 5C:ℝ := 11 / 5D:ℝ := 0A:ℝ := 1B:ℝ := 85L:ℝ := log xS:ℝ := √xhL:851 / 100 ≤ LhL_pos:0 < LhL_sq:7242 / 100 ≤ L ^ 2hS:70 ≤ ShS_pos:0 < S⊢ 0 ≤ x linarith All goals completed! 🐙) x:ℝhx:5000 ≤ xh:ℝ := 7 / 20 * √x * log x ^ 2T:ℝ := 3 / 2 * √x / log xa_rvM:ℝ := 16 / 5C:ℝ := 11 / 5D:ℝ := 0A:ℝ := 1B:ℝ := 85L:ℝ := log xS:ℝ := √xhL:851 / 100 ≤ LhL_pos:0 < LhL_sq:7242 / 100 ≤ L ^ 2hS:70 ≤ ShS_pos:0 < ShS_sq:S ^ 2 = x⊢ (1 ≤ x - h ∧ 0 < h ∧ 6 ≤ T) ∧
h / 2 + log (2 * π) +
√(x + h) * (a_rvM / 2 * log T ^ 2 + (a_rvM + C) * log T + C + D / 6 - a_rvM / 2 * log 6 ^ 2 - C * log 6) +
2 * (x + h) ^ (3 / 2) / h * ((2 * a_rvM * log T + 2 * a_rvM + 2 * C) / T + 2 * D / T ^ 2) +
32 * (2 * A + B) / (π * h) * (x + h) ^ (3 / 4) ≤
7 / 8 * S * L ^ 2
have hL2_le_S : L ^ 2 ≤ (20 / 19 : ℝ) * S := sq_log_le_twenty_nineteenths_sqrt hx x:ℝhx:5000 ≤ xh:ℝ := 7 / 20 * √x * log x ^ 2T:ℝ := 3 / 2 * √x / log xa_rvM:ℝ := 16 / 5C:ℝ := 11 / 5D:ℝ := 0A:ℝ := 1B:ℝ := 85L:ℝ := log xS:ℝ := √xhL:851 / 100 ≤ LhL_pos:0 < LhL_sq:7242 / 100 ≤ L ^ 2hS:70 ≤ ShS_pos:0 < ShS_sq:S ^ 2 = xhL2_le_S:L ^ 2 ≤ 20 / 19 * S⊢ (1 ≤ x - h ∧ 0 < h ∧ 6 ≤ T) ∧
h / 2 + log (2 * π) +
√(x + h) * (a_rvM / 2 * log T ^ 2 + (a_rvM + C) * log T + C + D / 6 - a_rvM / 2 * log 6 ^ 2 - C * log 6) +
2 * (x + h) ^ (3 / 2) / h * ((2 * a_rvM * log T + 2 * a_rvM + 2 * C) / T + 2 * D / T ^ 2) +
32 * (2 * A + B) / (π * h) * (x + h) ^ (3 / 4) ≤
7 / 8 * S * L ^ 2
have hh_def : h = (7 / 20 : ℝ) * S * L ^ 2 := rfl x:ℝhx:5000 ≤ xh:ℝ := 7 / 20 * √x * log x ^ 2T:ℝ := 3 / 2 * √x / log xa_rvM:ℝ := 16 / 5C:ℝ := 11 / 5D:ℝ := 0A:ℝ := 1B:ℝ := 85L:ℝ := log xS:ℝ := √xhL:851 / 100 ≤ LhL_pos:0 < LhL_sq:7242 / 100 ≤ L ^ 2hS:70 ≤ ShS_pos:0 < ShS_sq:S ^ 2 = xhL2_le_S:L ^ 2 ≤ 20 / 19 * Shh_def:h = 7 / 20 * S * L ^ 2⊢ (1 ≤ x - h ∧ 0 < h ∧ 6 ≤ T) ∧
h / 2 + log (2 * π) +
√(x + h) * (a_rvM / 2 * log T ^ 2 + (a_rvM + C) * log T + C + D / 6 - a_rvM / 2 * log 6 ^ 2 - C * log 6) +
2 * (x + h) ^ (3 / 2) / h * ((2 * a_rvM * log T + 2 * a_rvM + 2 * C) / T + 2 * D / T ^ 2) +
32 * (2 * A + B) / (π * h) * (x + h) ^ (3 / 4) ≤
7 / 8 * S * L ^ 2
have hT_def : T = (3 / 2 : ℝ) * S / L := rfl x:ℝhx:5000 ≤ xh:ℝ := 7 / 20 * √x * log x ^ 2T:ℝ := 3 / 2 * √x / log xa_rvM:ℝ := 16 / 5C:ℝ := 11 / 5D:ℝ := 0A:ℝ := 1B:ℝ := 85L:ℝ := log xS:ℝ := √xhL:851 / 100 ≤ LhL_pos:0 < LhL_sq:7242 / 100 ≤ L ^ 2hS:70 ≤ ShS_pos:0 < ShS_sq:S ^ 2 = xhL2_le_S:L ^ 2 ≤ 20 / 19 * Shh_def:h = 7 / 20 * S * L ^ 2hT_def:T = 3 / 2 * S / L⊢ (1 ≤ x - h ∧ 0 < h ∧ 6 ≤ T) ∧
h / 2 + log (2 * π) +
√(x + h) * (a_rvM / 2 * log T ^ 2 + (a_rvM + C) * log T + C + D / 6 - a_rvM / 2 * log 6 ^ 2 - C * log 6) +
2 * (x + h) ^ (3 / 2) / h * ((2 * a_rvM * log T + 2 * a_rvM + 2 * C) / T + 2 * D / T ^ 2) +
32 * (2 * A + B) / (π * h) * (x + h) ^ (3 / 4) ≤
7 / 8 * S * L ^ 2
have hh_pos : 0 < h := by x:ℝhx:5000 ≤ x⊢ let h := 7 / 20 * √x * log x ^ 2;
let T := 3 / 2 * √x / log x;
let a_rvM := 16 / 5;
let C := 11 / 5;
let D := 0;
let A := 1;
let B := 85;
(1 ≤ x - h ∧ 0 < h ∧ 6 ≤ T) ∧
h / 2 + log (2 * π) +
√(x + h) * (a_rvM / 2 * log T ^ 2 + (a_rvM + C) * log T + C + D / 6 - a_rvM / 2 * log 6 ^ 2 - C * log 6) +
2 * (x + h) ^ (3 / 2) / h * ((2 * a_rvM * log T + 2 * a_rvM + 2 * C) / T + 2 * D / T ^ 2) +
32 * (2 * A + B) / (π * h) * (x + h) ^ (3 / 4) ≤
7 / 8 * √x * log x ^ 2 rw [hh_def x:ℝhx:5000 ≤ xh:ℝ := 7 / 20 * √x * log x ^ 2T:ℝ := 3 / 2 * √x / log xa_rvM:ℝ := 16 / 5C:ℝ := 11 / 5D:ℝ := 0A:ℝ := 1B:ℝ := 85L:ℝ := log xS:ℝ := √xhL:851 / 100 ≤ LhL_pos:0 < LhL_sq:7242 / 100 ≤ L ^ 2hS:70 ≤ ShS_pos:0 < ShS_sq:S ^ 2 = xhL2_le_S:L ^ 2 ≤ 20 / 19 * Shh_def:h = 7 / 20 * S * L ^ 2hT_def:T = 3 / 2 * S / L⊢ 0 < 7 / 20 * S * L ^ 2] x:ℝhx:5000 ≤ xh:ℝ := 7 / 20 * √x * log x ^ 2T:ℝ := 3 / 2 * √x / log xa_rvM:ℝ := 16 / 5C:ℝ := 11 / 5D:ℝ := 0A:ℝ := 1B:ℝ := 85L:ℝ := log xS:ℝ := √xhL:851 / 100 ≤ LhL_pos:0 < LhL_sq:7242 / 100 ≤ L ^ 2hS:70 ≤ ShS_pos:0 < ShS_sq:S ^ 2 = xhL2_le_S:L ^ 2 ≤ 20 / 19 * Shh_def:h = 7 / 20 * S * L ^ 2hT_def:T = 3 / 2 * S / L⊢ 0 < 7 / 20 * S * L ^ 2; positivity x:ℝhx:5000 ≤ xh:ℝ := 7 / 20 * √x * log x ^ 2T:ℝ := 3 / 2 * √x / log xa_rvM:ℝ := 16 / 5C:ℝ := 11 / 5D:ℝ := 0A:ℝ := 1B:ℝ := 85L:ℝ := log xS:ℝ := √xhL:851 / 100 ≤ LhL_pos:0 < LhL_sq:7242 / 100 ≤ L ^ 2hS:70 ≤ ShS_pos:0 < ShS_sq:S ^ 2 = xhL2_le_S:L ^ 2 ≤ 20 / 19 * Shh_def:h = 7 / 20 * S * L ^ 2hT_def:T = 3 / 2 * S / Lhh_pos:0 < h⊢ (1 ≤ x - h ∧ 0 < h ∧ 6 ≤ T) ∧
h / 2 + log (2 * π) +
√(x + h) * (a_rvM / 2 * log T ^ 2 + (a_rvM + C) * log T + C + D / 6 - a_rvM / 2 * log 6 ^ 2 - C * log 6) +
2 * (x + h) ^ (3 / 2) / h * ((2 * a_rvM * log T + 2 * a_rvM + 2 * C) / T + 2 * D / T ^ 2) +
32 * (2 * A + B) / (π * h) * (x + h) ^ (3 / 4) ≤
7 / 8 * S * L ^ 2
have hh_le_x : h ≤ (7 / 19 : ℝ) * x := by x:ℝhx:5000 ≤ x⊢ let h := 7 / 20 * √x * log x ^ 2;
let T := 3 / 2 * √x / log x;
let a_rvM := 16 / 5;
let C := 11 / 5;
let D := 0;
let A := 1;
let B := 85;
(1 ≤ x - h ∧ 0 < h ∧ 6 ≤ T) ∧
h / 2 + log (2 * π) +
√(x + h) * (a_rvM / 2 * log T ^ 2 + (a_rvM + C) * log T + C + D / 6 - a_rvM / 2 * log 6 ^ 2 - C * log 6) +
2 * (x + h) ^ (3 / 2) / h * ((2 * a_rvM * log T + 2 * a_rvM + 2 * C) / T + 2 * D / T ^ 2) +
32 * (2 * A + B) / (π * h) * (x + h) ^ (3 / 4) ≤
7 / 8 * √x * log x ^ 2
calc h = (7 / 20 : ℝ) * S * L ^ 2 := hh_def
_ ≤ (7 / 20 : ℝ) * S * ((20 / 19 : ℝ) * S) := by x:ℝhx:5000 ≤ xh:ℝ := 7 / 20 * √x * log x ^ 2T:ℝ := 3 / 2 * √x / log xa_rvM:ℝ := 16 / 5C:ℝ := 11 / 5D:ℝ := 0A:ℝ := 1B:ℝ := 85L:ℝ := log xS:ℝ := √xhL:851 / 100 ≤ LhL_pos:0 < LhL_sq:7242 / 100 ≤ L ^ 2hS:70 ≤ ShS_pos:0 < ShS_sq:S ^ 2 = xhL2_le_S:L ^ 2 ≤ 20 / 19 * Shh_def:h = 7 / 20 * S * L ^ 2hT_def:T = 3 / 2 * S / Lhh_pos:0 < h⊢ 7 / 20 * S * L ^ 2 ≤ 7 / 20 * S * (20 / 19 * S) nlinarith All goals completed! 🐙
_ = (7 / 19 : ℝ) * S ^ 2 := by x:ℝhx:5000 ≤ xh:ℝ := 7 / 20 * √x * log x ^ 2T:ℝ := 3 / 2 * √x / log xa_rvM:ℝ := 16 / 5C:ℝ := 11 / 5D:ℝ := 0A:ℝ := 1B:ℝ := 85L:ℝ := log xS:ℝ := √xhL:851 / 100 ≤ LhL_pos:0 < LhL_sq:7242 / 100 ≤ L ^ 2hS:70 ≤ ShS_pos:0 < ShS_sq:S ^ 2 = xhL2_le_S:L ^ 2 ≤ 20 / 19 * Shh_def:h = 7 / 20 * S * L ^ 2hT_def:T = 3 / 2 * S / Lhh_pos:0 < h⊢ 7 / 20 * S * (20 / 19 * S) = 7 / 19 * S ^ 2 ring All goals completed! 🐙
_ = (7 / 19 : ℝ) * x := by x:ℝhx:5000 ≤ xh:ℝ := 7 / 20 * √x * log x ^ 2T:ℝ := 3 / 2 * √x / log xa_rvM:ℝ := 16 / 5C:ℝ := 11 / 5D:ℝ := 0A:ℝ := 1B:ℝ := 85L:ℝ := log xS:ℝ := √xhL:851 / 100 ≤ LhL_pos:0 < LhL_sq:7242 / 100 ≤ L ^ 2hS:70 ≤ ShS_pos:0 < ShS_sq:S ^ 2 = xhL2_le_S:L ^ 2 ≤ 20 / 19 * Shh_def:h = 7 / 20 * S * L ^ 2hT_def:T = 3 / 2 * S / Lhh_pos:0 < h⊢ 7 / 19 * S ^ 2 = 7 / 19 * x rw [hS_sq x:ℝhx:5000 ≤ xh:ℝ := 7 / 20 * √x * log x ^ 2T:ℝ := 3 / 2 * √x / log xa_rvM:ℝ := 16 / 5C:ℝ := 11 / 5D:ℝ := 0A:ℝ := 1B:ℝ := 85L:ℝ := log xS:ℝ := √xhL:851 / 100 ≤ LhL_pos:0 < LhL_sq:7242 / 100 ≤ L ^ 2hS:70 ≤ ShS_pos:0 < ShS_sq:S ^ 2 = xhL2_le_S:L ^ 2 ≤ 20 / 19 * Shh_def:h = 7 / 20 * S * L ^ 2hT_def:T = 3 / 2 * S / Lhh_pos:0 < h⊢ 7 / 19 * x = 7 / 19 * x] x:ℝhx:5000 ≤ xh:ℝ := 7 / 20 * √x * log x ^ 2T:ℝ := 3 / 2 * √x / log xa_rvM:ℝ := 16 / 5C:ℝ := 11 / 5D:ℝ := 0A:ℝ := 1B:ℝ := 85L:ℝ := log xS:ℝ := √xhL:851 / 100 ≤ LhL_pos:0 < LhL_sq:7242 / 100 ≤ L ^ 2hS:70 ≤ ShS_pos:0 < ShS_sq:S ^ 2 = xhL2_le_S:L ^ 2 ≤ 20 / 19 * Shh_def:h = 7 / 20 * S * L ^ 2hT_def:T = 3 / 2 * S / Lhh_pos:0 < hhh_le_x:h ≤ 7 / 19 * x⊢ (1 ≤ x - h ∧ 0 < h ∧ 6 ≤ T) ∧
h / 2 + log (2 * π) +
√(x + h) * (a_rvM / 2 * log T ^ 2 + (a_rvM + C) * log T + C + D / 6 - a_rvM / 2 * log 6 ^ 2 - C * log 6) +
2 * (x + h) ^ (3 / 2) / h * ((2 * a_rvM * log T + 2 * a_rvM + 2 * C) / T + 2 * D / T ^ 2) +
32 * (2 * A + B) / (π * h) * (x + h) ^ (3 / 4) ≤
7 / 8 * S * L ^ 2
have hx_sub_h : 1 ≤ x - h := by x:ℝhx:5000 ≤ x⊢ let h := 7 / 20 * √x * log x ^ 2;
let T := 3 / 2 * √x / log x;
let a_rvM := 16 / 5;
let C := 11 / 5;
let D := 0;
let A := 1;
let B := 85;
(1 ≤ x - h ∧ 0 < h ∧ 6 ≤ T) ∧
h / 2 + log (2 * π) +
√(x + h) * (a_rvM / 2 * log T ^ 2 + (a_rvM + C) * log T + C + D / 6 - a_rvM / 2 * log 6 ^ 2 - C * log 6) +
2 * (x + h) ^ (3 / 2) / h * ((2 * a_rvM * log T + 2 * a_rvM + 2 * C) / T + 2 * D / T ^ 2) +
32 * (2 * A + B) / (π * h) * (x + h) ^ (3 / 4) ≤
7 / 8 * √x * log x ^ 2 linarith x:ℝhx:5000 ≤ xh:ℝ := 7 / 20 * √x * log x ^ 2T:ℝ := 3 / 2 * √x / log xa_rvM:ℝ := 16 / 5C:ℝ := 11 / 5D:ℝ := 0A:ℝ := 1B:ℝ := 85L:ℝ := log xS:ℝ := √xhL:851 / 100 ≤ LhL_pos:0 < LhL_sq:7242 / 100 ≤ L ^ 2hS:70 ≤ ShS_pos:0 < ShS_sq:S ^ 2 = xhL2_le_S:L ^ 2 ≤ 20 / 19 * Shh_def:h = 7 / 20 * S * L ^ 2hT_def:T = 3 / 2 * S / Lhh_pos:0 < hhh_le_x:h ≤ 7 / 19 * xhx_sub_h:1 ≤ x - h⊢ (1 ≤ x - h ∧ 0 < h ∧ 6 ≤ T) ∧
h / 2 + log (2 * π) +
√(x + h) * (a_rvM / 2 * log T ^ 2 + (a_rvM + C) * log T + C + D / 6 - a_rvM / 2 * log 6 ^ 2 - C * log 6) +
2 * (x + h) ^ (3 / 2) / h * ((2 * a_rvM * log T + 2 * a_rvM + 2 * C) / T + 2 * D / T ^ 2) +
32 * (2 * A + B) / (π * h) * (x + h) ^ (3 / 4) ≤
7 / 8 * S * L ^ 2
have h6_le_T : 6 ≤ T := by x:ℝhx:5000 ≤ x⊢ let h := 7 / 20 * √x * log x ^ 2;
let T := 3 / 2 * √x / log x;
let a_rvM := 16 / 5;
let C := 11 / 5;
let D := 0;
let A := 1;
let B := 85;
(1 ≤ x - h ∧ 0 < h ∧ 6 ≤ T) ∧
h / 2 + log (2 * π) +
√(x + h) * (a_rvM / 2 * log T ^ 2 + (a_rvM + C) * log T + C + D / 6 - a_rvM / 2 * log 6 ^ 2 - C * log 6) +
2 * (x + h) ^ (3 / 2) / h * ((2 * a_rvM * log T + 2 * a_rvM + 2 * C) / T + 2 * D / T ^ 2) +
32 * (2 * A + B) / (π * h) * (x + h) ^ (3 / 4) ≤
7 / 8 * √x * log x ^ 2
rw [hT_def, x:ℝhx:5000 ≤ xh:ℝ := 7 / 20 * √x * log x ^ 2T:ℝ := 3 / 2 * √x / log xa_rvM:ℝ := 16 / 5C:ℝ := 11 / 5D:ℝ := 0A:ℝ := 1B:ℝ := 85L:ℝ := log xS:ℝ := √xhL:851 / 100 ≤ LhL_pos:0 < LhL_sq:7242 / 100 ≤ L ^ 2hS:70 ≤ ShS_pos:0 < ShS_sq:S ^ 2 = xhL2_le_S:L ^ 2 ≤ 20 / 19 * Shh_def:h = 7 / 20 * S * L ^ 2hT_def:T = 3 / 2 * S / Lhh_pos:0 < hhh_le_x:h ≤ 7 / 19 * xhx_sub_h:1 ≤ x - h⊢ 6 ≤ 3 / 2 * S / L le_div_iff₀ hL_pos x:ℝhx:5000 ≤ xh:ℝ := 7 / 20 * √x * log x ^ 2T:ℝ := 3 / 2 * √x / log xa_rvM:ℝ := 16 / 5C:ℝ := 11 / 5D:ℝ := 0A:ℝ := 1B:ℝ := 85L:ℝ := log xS:ℝ := √xhL:851 / 100 ≤ LhL_pos:0 < LhL_sq:7242 / 100 ≤ L ^ 2hS:70 ≤ ShS_pos:0 < ShS_sq:S ^ 2 = xhL2_le_S:L ^ 2 ≤ 20 / 19 * Shh_def:h = 7 / 20 * S * L ^ 2hT_def:T = 3 / 2 * S / Lhh_pos:0 < hhh_le_x:h ≤ 7 / 19 * xhx_sub_h:1 ≤ x - h⊢ 6 * L ≤ 3 / 2 * S] x:ℝhx:5000 ≤ xh:ℝ := 7 / 20 * √x * log x ^ 2T:ℝ := 3 / 2 * √x / log xa_rvM:ℝ := 16 / 5C:ℝ := 11 / 5D:ℝ := 0A:ℝ := 1B:ℝ := 85L:ℝ := log xS:ℝ := √xhL:851 / 100 ≤ LhL_pos:0 < LhL_sq:7242 / 100 ≤ L ^ 2hS:70 ≤ ShS_pos:0 < ShS_sq:S ^ 2 = xhL2_le_S:L ^ 2 ≤ 20 / 19 * Shh_def:h = 7 / 20 * S * L ^ 2hT_def:T = 3 / 2 * S / Lhh_pos:0 < hhh_le_x:h ≤ 7 / 19 * xhx_sub_h:1 ≤ x - h⊢ 6 * L ≤ 3 / 2 * S
nlinarith x:ℝhx:5000 ≤ xh:ℝ := 7 / 20 * √x * log x ^ 2T:ℝ := 3 / 2 * √x / log xa_rvM:ℝ := 16 / 5C:ℝ := 11 / 5D:ℝ := 0A:ℝ := 1B:ℝ := 85L:ℝ := log xS:ℝ := √xhL:851 / 100 ≤ LhL_pos:0 < LhL_sq:7242 / 100 ≤ L ^ 2hS:70 ≤ ShS_pos:0 < ShS_sq:S ^ 2 = xhL2_le_S:L ^ 2 ≤ 20 / 19 * Shh_def:h = 7 / 20 * S * L ^ 2hT_def:T = 3 / 2 * S / Lhh_pos:0 < hhh_le_x:h ≤ 7 / 19 * xhx_sub_h:1 ≤ x - hh6_le_T:6 ≤ T⊢ (1 ≤ x - h ∧ 0 < h ∧ 6 ≤ T) ∧
h / 2 + log (2 * π) +
√(x + h) * (a_rvM / 2 * log T ^ 2 + (a_rvM + C) * log T + C + D / 6 - a_rvM / 2 * log 6 ^ 2 - C * log 6) +
2 * (x + h) ^ (3 / 2) / h * ((2 * a_rvM * log T + 2 * a_rvM + 2 * C) / T + 2 * D / T ^ 2) +
32 * (2 * A + B) / (π * h) * (x + h) ^ (3 / 4) ≤
7 / 8 * S * L ^ 2
have hT_pos : 0 < T := by x:ℝhx:5000 ≤ x⊢ let h := 7 / 20 * √x * log x ^ 2;
let T := 3 / 2 * √x / log x;
let a_rvM := 16 / 5;
let C := 11 / 5;
let D := 0;
let A := 1;
let B := 85;
(1 ≤ x - h ∧ 0 < h ∧ 6 ≤ T) ∧
h / 2 + log (2 * π) +
√(x + h) * (a_rvM / 2 * log T ^ 2 + (a_rvM + C) * log T + C + D / 6 - a_rvM / 2 * log 6 ^ 2 - C * log 6) +
2 * (x + h) ^ (3 / 2) / h * ((2 * a_rvM * log T + 2 * a_rvM + 2 * C) / T + 2 * D / T ^ 2) +
32 * (2 * A + B) / (π * h) * (x + h) ^ (3 / 4) ≤
7 / 8 * √x * log x ^ 2 linarith x:ℝhx:5000 ≤ xh:ℝ := 7 / 20 * √x * log x ^ 2T:ℝ := 3 / 2 * √x / log xa_rvM:ℝ := 16 / 5C:ℝ := 11 / 5D:ℝ := 0A:ℝ := 1B:ℝ := 85L:ℝ := log xS:ℝ := √xhL:851 / 100 ≤ LhL_pos:0 < LhL_sq:7242 / 100 ≤ L ^ 2hS:70 ≤ ShS_pos:0 < ShS_sq:S ^ 2 = xhL2_le_S:L ^ 2 ≤ 20 / 19 * Shh_def:h = 7 / 20 * S * L ^ 2hT_def:T = 3 / 2 * S / Lhh_pos:0 < hhh_le_x:h ≤ 7 / 19 * xhx_sub_h:1 ≤ x - hh6_le_T:6 ≤ ThT_pos:0 < T⊢ (1 ≤ x - h ∧ 0 < h ∧ 6 ≤ T) ∧
h / 2 + log (2 * π) +
√(x + h) * (a_rvM / 2 * log T ^ 2 + (a_rvM + C) * log T + C + D / 6 - a_rvM / 2 * log 6 ^ 2 - C * log 6) +
2 * (x + h) ^ (3 / 2) / h * ((2 * a_rvM * log T + 2 * a_rvM + 2 * C) / T + 2 * D / T ^ 2) +
32 * (2 * A + B) / (π * h) * (x + h) ^ (3 / 4) ≤
7 / 8 * S * L ^ 2
refine ⟨⟨hx_sub_h, hh_pos, h6_le_T⟩, ?_⟩ x:ℝhx:5000 ≤ xh:ℝ := 7 / 20 * √x * log x ^ 2T:ℝ := 3 / 2 * √x / log xa_rvM:ℝ := 16 / 5C:ℝ := 11 / 5D:ℝ := 0A:ℝ := 1B:ℝ := 85L:ℝ := log xS:ℝ := √xhL:851 / 100 ≤ LhL_pos:0 < LhL_sq:7242 / 100 ≤ L ^ 2hS:70 ≤ ShS_pos:0 < ShS_sq:S ^ 2 = xhL2_le_S:L ^ 2 ≤ 20 / 19 * Shh_def:h = 7 / 20 * S * L ^ 2hT_def:T = 3 / 2 * S / Lhh_pos:0 < hhh_le_x:h ≤ 7 / 19 * xhx_sub_h:1 ≤ x - hh6_le_T:6 ≤ ThT_pos:0 < T⊢ h / 2 + log (2 * π) +
√(x + h) * (a_rvM / 2 * log T ^ 2 + (a_rvM + C) * log T + C + D / 6 - a_rvM / 2 * log 6 ^ 2 - C * log 6) +
2 * (x + h) ^ (3 / 2) / h * ((2 * a_rvM * log T + 2 * a_rvM + 2 * C) / T + 2 * D / T ^ 2) +
32 * (2 * A + B) / (π * h) * (x + h) ^ (3 / 4) ≤
7 / 8 * S * L ^ 2
obtain ⟨h_sqrt_ge, h_sqrt_xh, h_rpow_32, h_rpow_34⟩ :=
rpow_xh_bounds hx hS hS_sq hL_sq hh_def hh_le_x x:ℝhx:5000 ≤ xh:ℝ := 7 / 20 * √x * log x ^ 2T:ℝ := 3 / 2 * √x / log xa_rvM:ℝ := 16 / 5C:ℝ := 11 / 5D:ℝ := 0A:ℝ := 1B:ℝ := 85L:ℝ := log xS:ℝ := √xhL:851 / 100 ≤ LhL_pos:0 < LhL_sq:7242 / 100 ≤ L ^ 2hS:70 ≤ ShS_pos:0 < ShS_sq:S ^ 2 = xhL2_le_S:L ^ 2 ≤ 20 / 19 * Shh_def:h = 7 / 20 * S * L ^ 2hT_def:T = 3 / 2 * S / Lhh_pos:0 < hhh_le_x:h ≤ 7 / 19 * xhx_sub_h:1 ≤ x - hh6_le_T:6 ≤ ThT_pos:0 < Th_sqrt_ge:S ≤ √(x + h)h_sqrt_xh:√(x + h) ≤ 34 / 29 * Sh_rpow_32:(x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3h_rpow_34:(x + h) ^ (3 / 4) ≤ 26 / 171 * S ^ 2⊢ h / 2 + log (2 * π) +
√(x + h) * (a_rvM / 2 * log T ^ 2 + (a_rvM + C) * log T + C + D / 6 - a_rvM / 2 * log 6 ^ 2 - C * log 6) +
2 * (x + h) ^ (3 / 2) / h * ((2 * a_rvM * log T + 2 * a_rvM + 2 * C) / T + 2 * D / T ^ 2) +
32 * (2 * A + B) / (π * h) * (x + h) ^ (3 / 4) ≤
7 / 8 * S * L ^ 2
obtain ⟨h_logT_nonneg, h_logT_le, h_log6_ge⟩ :=
log_T_and_six_bounds hL hS_pos (Real.log_sqrt (by x:ℝhx:5000 ≤ xh:ℝ := 7 / 20 * √x * log x ^ 2T:ℝ := 3 / 2 * √x / log xa_rvM:ℝ := 16 / 5C:ℝ := 11 / 5D:ℝ := 0A:ℝ := 1B:ℝ := 85L:ℝ := log xS:ℝ := √xhL:851 / 100 ≤ LhL_pos:0 < LhL_sq:7242 / 100 ≤ L ^ 2hS:70 ≤ ShS_pos:0 < ShS_sq:S ^ 2 = xhL2_le_S:L ^ 2 ≤ 20 / 19 * Shh_def:h = 7 / 20 * S * L ^ 2hT_def:T = 3 / 2 * S / Lhh_pos:0 < hhh_le_x:h ≤ 7 / 19 * xhx_sub_h:1 ≤ x - hh6_le_T:6 ≤ ThT_pos:0 < Th_sqrt_ge:S ≤ √(x + h)h_sqrt_xh:√(x + h) ≤ 34 / 29 * Sh_rpow_32:(x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3h_rpow_34:(x + h) ^ (3 / 4) ≤ 26 / 171 * S ^ 2⊢ 0 ≤ x linarith All goals completed! 🐙)) h6_le_T hT_def x:ℝhx:5000 ≤ xh:ℝ := 7 / 20 * √x * log x ^ 2T:ℝ := 3 / 2 * √x / log xa_rvM:ℝ := 16 / 5C:ℝ := 11 / 5D:ℝ := 0A:ℝ := 1B:ℝ := 85L:ℝ := log xS:ℝ := √xhL:851 / 100 ≤ LhL_pos:0 < LhL_sq:7242 / 100 ≤ L ^ 2hS:70 ≤ ShS_pos:0 < ShS_sq:S ^ 2 = xhL2_le_S:L ^ 2 ≤ 20 / 19 * Shh_def:h = 7 / 20 * S * L ^ 2hT_def:T = 3 / 2 * S / Lhh_pos:0 < hhh_le_x:h ≤ 7 / 19 * xhx_sub_h:1 ≤ x - hh6_le_T:6 ≤ ThT_pos:0 < Th_sqrt_ge:S ≤ √(x + h)h_sqrt_xh:√(x + h) ≤ 34 / 29 * Sh_rpow_32:(x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3h_rpow_34:(x + h) ^ (3 / 4) ≤ 26 / 171 * S ^ 2h_logT_nonneg:0 ≤ log Th_logT_le:log T ≤ L / 2 - 429 / 250h_log6_ge:89 / 50 ≤ log 6⊢ h / 2 + log (2 * π) +
√(x + h) * (a_rvM / 2 * log T ^ 2 + (a_rvM + C) * log T + C + D / 6 - a_rvM / 2 * log 6 ^ 2 - C * log 6) +
2 * (x + h) ^ (3 / 2) / h * ((2 * a_rvM * log T + 2 * a_rvM + 2 * C) / T + 2 * D / T ^ 2) +
32 * (2 * A + B) / (π * h) * (x + h) ^ (3 / 4) ≤
7 / 8 * S * L ^ 2
have h_term1 : h / 2 = (7 / 40 : ℝ) * S * L ^ 2 := by x:ℝhx:5000 ≤ x⊢ let h := 7 / 20 * √x * log x ^ 2;
let T := 3 / 2 * √x / log x;
let a_rvM := 16 / 5;
let C := 11 / 5;
let D := 0;
let A := 1;
let B := 85;
(1 ≤ x - h ∧ 0 < h ∧ 6 ≤ T) ∧
h / 2 + log (2 * π) +
√(x + h) * (a_rvM / 2 * log T ^ 2 + (a_rvM + C) * log T + C + D / 6 - a_rvM / 2 * log 6 ^ 2 - C * log 6) +
2 * (x + h) ^ (3 / 2) / h * ((2 * a_rvM * log T + 2 * a_rvM + 2 * C) / T + 2 * D / T ^ 2) +
32 * (2 * A + B) / (π * h) * (x + h) ^ (3 / 4) ≤
7 / 8 * √x * log x ^ 2 rw [hh_def x:ℝhx:5000 ≤ xh:ℝ := 7 / 20 * √x * log x ^ 2T:ℝ := 3 / 2 * √x / log xa_rvM:ℝ := 16 / 5C:ℝ := 11 / 5D:ℝ := 0A:ℝ := 1B:ℝ := 85L:ℝ := log xS:ℝ := √xhL:851 / 100 ≤ LhL_pos:0 < LhL_sq:7242 / 100 ≤ L ^ 2hS:70 ≤ ShS_pos:0 < ShS_sq:S ^ 2 = xhL2_le_S:L ^ 2 ≤ 20 / 19 * Shh_def:h = 7 / 20 * S * L ^ 2hT_def:T = 3 / 2 * S / Lhh_pos:0 < hhh_le_x:h ≤ 7 / 19 * xhx_sub_h:1 ≤ x - hh6_le_T:6 ≤ ThT_pos:0 < Th_sqrt_ge:S ≤ √(x + h)h_sqrt_xh:√(x + h) ≤ 34 / 29 * Sh_rpow_32:(x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3h_rpow_34:(x + h) ^ (3 / 4) ≤ 26 / 171 * S ^ 2h_logT_nonneg:0 ≤ log Th_logT_le:log T ≤ L / 2 - 429 / 250h_log6_ge:89 / 50 ≤ log 6⊢ 7 / 20 * S * L ^ 2 / 2 = 7 / 40 * S * L ^ 2] x:ℝhx:5000 ≤ xh:ℝ := 7 / 20 * √x * log x ^ 2T:ℝ := 3 / 2 * √x / log xa_rvM:ℝ := 16 / 5C:ℝ := 11 / 5D:ℝ := 0A:ℝ := 1B:ℝ := 85L:ℝ := log xS:ℝ := √xhL:851 / 100 ≤ LhL_pos:0 < LhL_sq:7242 / 100 ≤ L ^ 2hS:70 ≤ ShS_pos:0 < ShS_sq:S ^ 2 = xhL2_le_S:L ^ 2 ≤ 20 / 19 * Shh_def:h = 7 / 20 * S * L ^ 2hT_def:T = 3 / 2 * S / Lhh_pos:0 < hhh_le_x:h ≤ 7 / 19 * xhx_sub_h:1 ≤ x - hh6_le_T:6 ≤ ThT_pos:0 < Th_sqrt_ge:S ≤ √(x + h)h_sqrt_xh:√(x + h) ≤ 34 / 29 * Sh_rpow_32:(x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3h_rpow_34:(x + h) ^ (3 / 4) ≤ 26 / 171 * S ^ 2h_logT_nonneg:0 ≤ log Th_logT_le:log T ≤ L / 2 - 429 / 250h_log6_ge:89 / 50 ≤ log 6⊢ 7 / 20 * S * L ^ 2 / 2 = 7 / 40 * S * L ^ 2; ring x:ℝhx:5000 ≤ xh:ℝ := 7 / 20 * √x * log x ^ 2T:ℝ := 3 / 2 * √x / log xa_rvM:ℝ := 16 / 5C:ℝ := 11 / 5D:ℝ := 0A:ℝ := 1B:ℝ := 85L:ℝ := log xS:ℝ := √xhL:851 / 100 ≤ LhL_pos:0 < LhL_sq:7242 / 100 ≤ L ^ 2hS:70 ≤ ShS_pos:0 < ShS_sq:S ^ 2 = xhL2_le_S:L ^ 2 ≤ 20 / 19 * Shh_def:h = 7 / 20 * S * L ^ 2hT_def:T = 3 / 2 * S / Lhh_pos:0 < hhh_le_x:h ≤ 7 / 19 * xhx_sub_h:1 ≤ x - hh6_le_T:6 ≤ ThT_pos:0 < Th_sqrt_ge:S ≤ √(x + h)h_sqrt_xh:√(x + h) ≤ 34 / 29 * Sh_rpow_32:(x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3h_rpow_34:(x + h) ^ (3 / 4) ≤ 26 / 171 * S ^ 2h_logT_nonneg:0 ≤ log Th_logT_le:log T ≤ L / 2 - 429 / 250h_log6_ge:89 / 50 ≤ log 6h_term1:h / 2 = 7 / 40 * S * L ^ 2⊢ h / 2 + log (2 * π) +
√(x + h) * (a_rvM / 2 * log T ^ 2 + (a_rvM + C) * log T + C + D / 6 - a_rvM / 2 * log 6 ^ 2 - C * log 6) +
2 * (x + h) ^ (3 / 2) / h * ((2 * a_rvM * log T + 2 * a_rvM + 2 * C) / T + 2 * D / T ^ 2) +
32 * (2 * A + B) / (π * h) * (x + h) ^ (3 / 4) ≤
7 / 8 * S * L ^ 2
have h_term2 : Real.log (2 * Real.pi) ≤ (1 / 500 : ℝ) * S * L ^ 2 :=
term2_bound hS hL_sq x:ℝhx:5000 ≤ xh:ℝ := 7 / 20 * √x * log x ^ 2T:ℝ := 3 / 2 * √x / log xa_rvM:ℝ := 16 / 5C:ℝ := 11 / 5D:ℝ := 0A:ℝ := 1B:ℝ := 85L:ℝ := log xS:ℝ := √xhL:851 / 100 ≤ LhL_pos:0 < LhL_sq:7242 / 100 ≤ L ^ 2hS:70 ≤ ShS_pos:0 < ShS_sq:S ^ 2 = xhL2_le_S:L ^ 2 ≤ 20 / 19 * Shh_def:h = 7 / 20 * S * L ^ 2hT_def:T = 3 / 2 * S / Lhh_pos:0 < hhh_le_x:h ≤ 7 / 19 * xhx_sub_h:1 ≤ x - hh6_le_T:6 ≤ ThT_pos:0 < Th_sqrt_ge:S ≤ √(x + h)h_sqrt_xh:√(x + h) ≤ 34 / 29 * Sh_rpow_32:(x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3h_rpow_34:(x + h) ^ (3 / 4) ≤ 26 / 171 * S ^ 2h_logT_nonneg:0 ≤ log Th_logT_le:log T ≤ L / 2 - 429 / 250h_log6_ge:89 / 50 ≤ log 6h_term1:h / 2 = 7 / 40 * S * L ^ 2h_term2:log (2 * π) ≤ 1 / 500 * S * L ^ 2⊢ h / 2 + log (2 * π) +
√(x + h) * (a_rvM / 2 * log T ^ 2 + (a_rvM + C) * log T + C + D / 6 - a_rvM / 2 * log 6 ^ 2 - C * log 6) +
2 * (x + h) ^ (3 / 2) / h * ((2 * a_rvM * log T + 2 * a_rvM + 2 * C) / T + 2 * D / T ^ 2) +
32 * (2 * A + B) / (π * h) * (x + h) ^ (3 / 4) ≤
7 / 8 * S * L ^ 2
have h_term34 := term3_add_term4_bound hS_pos hL hL_sq hh_pos hT_pos hh_def hT_def
h_sqrt_ge h_sqrt_xh h_rpow_32 h_logT_nonneg h_logT_le h_log6_ge x:ℝhx:5000 ≤ xh:ℝ := 7 / 20 * √x * log x ^ 2T:ℝ := 3 / 2 * √x / log xa_rvM:ℝ := 16 / 5C:ℝ := 11 / 5D:ℝ := 0A:ℝ := 1B:ℝ := 85L:ℝ := log xS:ℝ := √xhL:851 / 100 ≤ LhL_pos:0 < LhL_sq:7242 / 100 ≤ L ^ 2hS:70 ≤ ShS_pos:0 < ShS_sq:S ^ 2 = xhL2_le_S:L ^ 2 ≤ 20 / 19 * Shh_def:h = 7 / 20 * S * L ^ 2hT_def:T = 3 / 2 * S / Lhh_pos:0 < hhh_le_x:h ≤ 7 / 19 * xhx_sub_h:1 ≤ x - hh6_le_T:6 ≤ ThT_pos:0 < Th_sqrt_ge:S ≤ √(x + h)h_sqrt_xh:√(x + h) ≤ 34 / 29 * Sh_rpow_32:(x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3h_rpow_34:(x + h) ^ (3 / 4) ≤ 26 / 171 * S ^ 2h_logT_nonneg:0 ≤ log Th_logT_le:log T ≤ L / 2 - 429 / 250h_log6_ge:89 / 50 ≤ log 6h_term1:h / 2 = 7 / 40 * S * L ^ 2h_term2:log (2 * π) ≤ 1 / 500 * S * L ^ 2h_term34:√(x + h) *
(16 / 5 / 2 * log T ^ 2 + (16 / 5 + 11 / 5) * log T + 11 / 5 + 0 / 6 - 16 / 5 / 2 * log 6 ^ 2 - 11 / 5 * log 6) +
2 * (x + h) ^ (3 / 2) / h * ((2 * (16 / 5) * log T + 2 * (16 / 5) + 2 * (11 / 5)) / T + 2 * 0 / T ^ 2) ≤
59 / 100 * S * L ^ 2⊢ h / 2 + log (2 * π) +
√(x + h) * (a_rvM / 2 * log T ^ 2 + (a_rvM + C) * log T + C + D / 6 - a_rvM / 2 * log 6 ^ 2 - C * log 6) +
2 * (x + h) ^ (3 / 2) / h * ((2 * a_rvM * log T + 2 * a_rvM + 2 * C) / T + 2 * D / T ^ 2) +
32 * (2 * A + B) / (π * h) * (x + h) ^ (3 / 4) ≤
7 / 8 * S * L ^ 2
have h_term5 := term5_bound hS_pos hL_pos hL_sq hh_pos hh_def h_rpow_34 x:ℝhx:5000 ≤ xh:ℝ := 7 / 20 * √x * log x ^ 2T:ℝ := 3 / 2 * √x / log xa_rvM:ℝ := 16 / 5C:ℝ := 11 / 5D:ℝ := 0A:ℝ := 1B:ℝ := 85L:ℝ := log xS:ℝ := √xhL:851 / 100 ≤ LhL_pos:0 < LhL_sq:7242 / 100 ≤ L ^ 2hS:70 ≤ ShS_pos:0 < ShS_sq:S ^ 2 = xhL2_le_S:L ^ 2 ≤ 20 / 19 * Shh_def:h = 7 / 20 * S * L ^ 2hT_def:T = 3 / 2 * S / Lhh_pos:0 < hhh_le_x:h ≤ 7 / 19 * xhx_sub_h:1 ≤ x - hh6_le_T:6 ≤ ThT_pos:0 < Th_sqrt_ge:S ≤ √(x + h)h_sqrt_xh:√(x + h) ≤ 34 / 29 * Sh_rpow_32:(x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3h_rpow_34:(x + h) ^ (3 / 4) ≤ 26 / 171 * S ^ 2h_logT_nonneg:0 ≤ log Th_logT_le:log T ≤ L / 2 - 429 / 250h_log6_ge:89 / 50 ≤ log 6h_term1:h / 2 = 7 / 40 * S * L ^ 2h_term2:log (2 * π) ≤ 1 / 500 * S * L ^ 2h_term34:√(x + h) *
(16 / 5 / 2 * log T ^ 2 + (16 / 5 + 11 / 5) * log T + 11 / 5 + 0 / 6 - 16 / 5 / 2 * log 6 ^ 2 - 11 / 5 * log 6) +
2 * (x + h) ^ (3 / 2) / h * ((2 * (16 / 5) * log T + 2 * (16 / 5) + 2 * (11 / 5)) / T + 2 * 0 / T ^ 2) ≤
59 / 100 * S * L ^ 2h_term5:32 * (2 * 1 + 85) / (π * h) * (x + h) ^ (3 / 4) ≤ 8 / 100 * S * L ^ 2⊢ h / 2 + log (2 * π) +
√(x + h) * (a_rvM / 2 * log T ^ 2 + (a_rvM + C) * log T + C + D / 6 - a_rvM / 2 * log 6 ^ 2 - C * log 6) +
2 * (x + h) ^ (3 / 2) / h * ((2 * a_rvM * log T + 2 * a_rvM + 2 * C) / T + 2 * D / T ^ 2) +
32 * (2 * A + B) / (π * h) * (x + h) ^ (3 / 4) ≤
7 / 8 * S * L ^ 2
dsimp [a_rvM, C, D, A, B] x:ℝhx:5000 ≤ xh:ℝ := 7 / 20 * √x * log x ^ 2T:ℝ := 3 / 2 * √x / log xa_rvM:ℝ := 16 / 5C:ℝ := 11 / 5D:ℝ := 0A:ℝ := 1B:ℝ := 85L:ℝ := log xS:ℝ := √xhL:851 / 100 ≤ LhL_pos:0 < LhL_sq:7242 / 100 ≤ L ^ 2hS:70 ≤ ShS_pos:0 < ShS_sq:S ^ 2 = xhL2_le_S:L ^ 2 ≤ 20 / 19 * Shh_def:h = 7 / 20 * S * L ^ 2hT_def:T = 3 / 2 * S / Lhh_pos:0 < hhh_le_x:h ≤ 7 / 19 * xhx_sub_h:1 ≤ x - hh6_le_T:6 ≤ ThT_pos:0 < Th_sqrt_ge:S ≤ √(x + h)h_sqrt_xh:√(x + h) ≤ 34 / 29 * Sh_rpow_32:(x + h) ^ (3 / 2) ≤ 161 / 100 * S ^ 3h_rpow_34:(x + h) ^ (3 / 4) ≤ 26 / 171 * S ^ 2h_logT_nonneg:0 ≤ log Th_logT_le:log T ≤ L / 2 - 429 / 250h_log6_ge:89 / 50 ≤ log 6h_term1:h / 2 = 7 / 40 * S * L ^ 2h_term2:log (2 * π) ≤ 1 / 500 * S * L ^ 2h_term34:√(x + h) *
(16 / 5 / 2 * log T ^ 2 + (16 / 5 + 11 / 5) * log T + 11 / 5 + 0 / 6 - 16 / 5 / 2 * log 6 ^ 2 - 11 / 5 * log 6) +
2 * (x + h) ^ (3 / 2) / h * ((2 * (16 / 5) * log T + 2 * (16 / 5) + 2 * (11 / 5)) / T + 2 * 0 / T ^ 2) ≤
59 / 100 * S * L ^ 2h_term5:32 * (2 * 1 + 85) / (π * h) * (x + h) ^ (3 / 4) ≤ 8 / 100 * S * L ^ 2⊢ h / 2 + log (2 * π) +
√(x + h) *
(16 / 5 / 2 * log T ^ 2 + (16 / 5 + 11 / 5) * log T + 11 / 5 + 0 / 6 - 16 / 5 / 2 * log 6 ^ 2 -
11 / 5 * log 6) +
2 * (x + h) ^ (3 / 2) / h * ((2 * (16 / 5) * log T + 2 * (16 / 5) + 2 * (11 / 5)) / T + 2 * 0 / T ^ 2) +
32 * (2 * 1 + 85) / (π * h) * (x + h) ^ (3 / 4) ≤
7 / 8 * S * L ^ 2
linarith All goals completed! 🐙end ConjectureMachines.Semantics.Riemann.ExplicitLarge