Interpolation and exponent algebra for Lemma r.LeBron (abstract reals)

All Real.rpow algebra used by lebron_step lives here, in statements about plain real numbers.

theorem AVenhance.Infra.FullTheorem.interpolate_holder {μ x A S h : ℝ} (hμ0 : 0 < μ) (hμ1 : μ ≤ 1 / 4) (hS0 : 0 ≤ S) (hx0 : 0 ≤ x) (hh : 0 ≤ h) (hx1 : x ≤ 2 * A) (hx2 : x ≤ S * h ^ (1 / 4)) : x ≤ (2 * A) ^ (1 - 4 * μ) * S ^ (4 * μ) * h ^ μ

Interpolation between a sup bound and a Hölder-1/4 bound: x ≤ 2A and x ≤ S h^{1/4} give x ≤ (2A)^{1-4μ} S^{4μ} h^μ for 0 < μ ≤ 1/4.

noncomputable def AVenhance.Infra.FullTheorem.lebronMu (δ P : ℝ) : ℝ

The Hölder exponent of Lemma r.LeBron: μ = δ/(8δ+4P).

Equations

• AVenhance.Infra.FullTheorem.lebronMu δ P = δ / (8 * δ + 4 * P)

theorem AVenhance.Infra.FullTheorem.lebronMu_pos {δ P : ℝ} (hδ : 0 < δ) (hP : 0 ≤ P) : 0 < lebronMu δ P

theorem AVenhance.Infra.FullTheorem.lebronMu_le {δ P : ℝ} (hδ : 0 < δ) (hP : 0 ≤ P) : lebronMu δ P ≤ 1 / 4

theorem AVenhance.Infra.FullTheorem.lebronMu_exponent {δ P : ℝ} (hδ : 0 < δ) (hP : 0 ≤ P) : δ * (1 - 4 * lebronMu δ P) - 2 * lebronMu δ P * P = δ / 2

The exponent bookkeeping: δ(1-4μ) - 2μP = δ/2.

theorem AVenhance.Infra.FullTheorem.rpow_mix {ε δ P μ : ℝ} (hε : 0 < ε) : (ε ^ δ) ^ (1 - 4 * μ) * (ε ^ (-(P / 2))) ^ (4 * μ) = ε ^ (δ * (1 - 4 * μ) - 2 * μ * P)

Power algebra: (ε^δ)^{1-4μ} (ε^{-P/2})^{4μ} = ε^{δ(1-4μ) - 2μP}.

theorem AVenhance.Infra.FullTheorem.holder_step {ε δ P x C₈ S₀ N h : ℝ} (hε : 0 < ε) (hδ : 0 < δ) (hP : 0 ≤ P) (hC₈ : 0 ≤ C₈) (hS₀ : 0 ≤ S₀) (hN : 0 ≤ N) (hh : 0 ≤ h) (hx0 : 0 ≤ x) (hx1 : x ≤ 2 * (C₈ * ε ^ δ * N)) (hx2 : x ≤ S₀ * ε ^ (-(P / 2)) * N * h ^ (1 / 4)) : x ≤ (2 * C₈) ^ (1 - 4 * lebronMu δ P) * S₀ ^ (4 * lebronMu δ P) * ε ^ (δ / 2) * N * h ^ lebronMu δ P

The assembled real-number step: from a sup bound x ≤ 2 C₈ ε^δ N and a Hölder bound x ≤ S₀ ε^{-P/2} N h^{1/4} conclude x ≤ K ε^{δ/2} N h^μ, K = (2C₈)^{1-4μ} S₀^{4μ}.

theorem AVenhance.Infra.FullTheorem.one_div_sqrt_le {c E P κ : ℝ} (hc : 0 < c) (hE : 0 < E) (hκ : c * E ^ P ≤ κ) : 1 / √κ ≤ 1 / √c * E ^ (-(P / 2))

1/√κ ≤ c^{-1/2} E^{-P/2} from c E^P ≤ κ.