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 x:ℝhx:5000 ≤ xhpow:2 ^ 86 ≤ x ^ 7hlog:log (2 ^ 86) ≤ log (x ^ 7)⊢ 851 / 100 ≤ log x x:ℝhx:5000 ≤ xhpow:2 ^ 86 ≤ x ^ 7hlog:↑86 * log 2 ≤ ↑7 * log x⊢ 851 / 100 ≤ log x x:ℝhx:5000 ≤ xhpow:2 ^ 86 ≤ x ^ 7hlog:↑86 * log 2 ≤ ↑7 * log xhlog2:0.6931471803 < log 2⊢ 851 / 100 ≤ log x x:ℝhx:5000 ≤ xhpow:2 ^ 86 ≤ x ^ 7hlog:86 * log 2 ≤ 7 * log xhlog2:0.6931471803 < log 2⊢ 851 / 100 ≤ log x All goals completed! 🐙

For x ≥ 5000, 70 ≤ Real.sqrt x.

lemma sqrt_ge_seventy {x : ℝ} (hx : 5000 ≤ x) : (70 : ℝ) ≤ Real.sqrt x := x:ℝhx:5000 ≤ x⊢ 70 ≤ √x x:ℝhx:5000 ≤ xh70:70 ^ 2 ≤ x⊢ 70 ≤ √x x:ℝhx:5000 ≤ xh70:70 ^ 2 ≤ xhsqrt:√(70 ^ 2) ≤ √x⊢ 70 ≤ √x rwa [Real.sqrt_sq (x:ℝhx:5000 ≤ xh70:70 ^ 2 ≤ xhsqrt:√(70 ^ 2) ≤ √x⊢ 0 ≤ 70 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 := v:ℝhv:851 / 400 ≤ v⊢ 39 / 10 * v ≤ rexp v v:ℝhv:851 / 400 ≤ vhv_nonneg:0 ≤ v⊢ 39 / 10 * v ≤ rexp v v:ℝhv:851 / 400 ≤ vhv_nonneg:0 ≤ vh_sum:∑ i ∈ Finset.range 7, v ^ i / ↑i.factorial ≤ rexp v⊢ 39 / 10 * v ≤ rexp v 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 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 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 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 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 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 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 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 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 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 := x:ℝhx:5000 ≤ x⊢ log x ^ 2 ≤ 20 / 19 * √x x:ℝhx:5000 ≤ xhL:851 / 100 ≤ log x⊢ log x ^ 2 ≤ 20 / 19 * √x x:ℝhx:5000 ≤ xhL:851 / 100 ≤ log xhv:851 / 400 ≤ log x / 4⊢ log x ^ 2 ≤ 20 / 19 * √x 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 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 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 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 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 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 := 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 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 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 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 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 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 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 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 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 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 := 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 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 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 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 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 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 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 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 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 := S:ℝL:ℝhS:70 ≤ ShL_sq:7242 / 100 ≤ L ^ 2⊢ log (2 * π) ≤ 1 / 500 * S * L ^ 2 S:ℝL:ℝhS:70 ≤ ShL_sq:7242 / 100 ≤ L ^ 2hpi:2 * π ≤ 8⊢ log (2 * π) ≤ 1 / 500 * S * L ^ 2 S:ℝL:ℝhS:70 ≤ ShL_sq:7242 / 100 ≤ L ^ 2hpi:2 * π ≤ 8hlog_2pi:log (2 * π) ≤ 2 * π - 1⊢ log (2 * π) ≤ 1 / 500 * S * L ^ 2 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 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 := 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 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 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 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 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 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 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 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 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 := 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 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 ^ 2hpi_gt:3 ≤ π⊢ 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 ^ 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) 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) 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) 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) 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) 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 := 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 All goals completed! 🐙end ConjectureMachines.Semantics.Riemann.ExplicitLarge