PrincipalResponseLegsHolder

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Provider: sub-step (iv) of the principal response, the Hoelder leg

Source displays in ABK26:

• The first moment of Step 3's bad-event estimate,

  E[ | bfAhom_{m-1}^{-1/2} bfA_m(cu_n) bfAhom_{m-1}^{-1/2} |^8 ]^{1/8} <= C gamma^{-1} ,
  

• The second moment,

  ( avsum_{z} E[ | bfAhom_{m-1}^{1/2} P_z |^4 ] )^{1/4} <= C ,
  

• The conclusion

  avsum_z E[ P_z . bfA_m(z+cu_n) P_z 1_{not Q_z} ] <= C gamma^{-2} exp(-gamma^{-1})
                                                  <= (1/2) gamma^6 .
  

This module supplies the Hoelder arithmetic of that chain and nothing else. Write B for the normalized matrix size of the first display and V for the normalized load length of the second, so that the energy observable obeys the pointwise domination X <= B . V^2 used in the conclusion display. Then the printed four-way split 1/8 + 1/4 + 1/4 + 3/8 = 1 is realized here as two nested two-factor Hoelder inequalities: an inner one at the conjugate pair (8, 2) bounding ‖B V^2‖_{8/5} by ‖B‖_8 ‖V‖_4^2, and an outer one at the conjugate pair (8/5, 8/3) separating the energy from the indicator of the bad event.

The tail exponent is 3/8, not 1

Every statement below carries the honest exponent 3/8; the printed exponent 1 occurs nowhere.

Main results

• holderConjugate_eightFifths_eightThirds, holderTriple_eight_two_eightFifths
• eLpNorm_energy_le_of_moments -- the inner split's energy factor.
• integral_rpow_le_of_eLpNorm_le -- descent from the seminorm to the source's own real moment root.
• integral_mul_indicator_le_of_moment -- the outer split at the exponent 3/8.

The two conjugate pairs

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.holderConjugate_eightFifths_eightThirds : (8 / 5).HolderConjugate (8 / 3)

The outer conjugate pair: 1/(8/5) + 1/(8/3) = 1.

instance Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.holderTriple_eight_two_eightFifths : ENNReal.HolderTriple 8 2 (8 / 5)

The inner conjugate pair: 1/8 + 1/2 = 1/(8/5), which is the printed `1/8

• 1/4 + 1/4with the two load factors kept together asV^2`.

The inner split: the energy factor

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.eLpNorm_energy_le_of_moments {Omega : Type u_1} {mOmega : MeasurableSpace Omega} {mu : MeasureTheory.Measure Omega} {B V X : Omega → ℝ} (hB0 : ∀ (omega : Omega), 0 ≤ B omega) (hV0 : ∀ (omega : Omega), 0 ≤ V omega) (hX0 : ∀ (omega : Omega), 0 ≤ X omega) (hdom : ∀ (omega : Omega), X omega ≤ B omega * V omega ^ 2) (hXm : MeasureTheory.AEStronglyMeasurable X mu) (hBm : MeasureTheory.AEStronglyMeasurable B mu) (hVm : MeasureTheory.AEStronglyMeasurable V mu) {Cb Cv : ℝ} (hCb0 : 0 ≤ Cb) (hCv0 : 0 ≤ Cv) (hBn : MeasureTheory.eLpNorm B 8 mu ≤ ENNReal.ofReal Cb) (hVn : MeasureTheory.eLpNorm V 4 mu ≤ ENNReal.ofReal Cv) : MeasureTheory.eLpNorm X (8 / 5) mu ≤ ENNReal.ofReal (Cb * Cv ^ 2)

The energy factor. If the energy observable X is dominated pointwise by B . V^2, then its L^{8/5} seminorm is at most the product ‖B‖_8 ‖V‖_4^2 of the two moments printed.

This is the manuscript's four-way Hoelder 1/8 + 1/4 + 1/4 + 3/8 = 1 with the two load factors kept together, so that only the two-factor inequality at the pair (8, 2) is needed.

Descent to the source's real moment root

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.integral_rpow_le_of_eLpNorm_le {Omega : Type u_1} {mOmega : MeasurableSpace Omega} {mu : MeasureTheory.Measure Omega} {X : Omega → ℝ} (hX0 : ∀ (omega : Omega), 0 ≤ X omega) {p : ℝ} (hp : 0 < p) (hmem : MeasureTheory.MemLp X (ENNReal.ofReal p) mu) {R : ℝ} (hR : 0 ≤ R) (h : MeasureTheory.eLpNorm X (ENNReal.ofReal p) mu ≤ ENNReal.ofReal R) : (∫ (omega : Omega), X omega ^ p ∂mu) ^ (1 / p) ≤ R

The source writes its moments as real moment roots (E[X^p])^{1/p}. A seminorm bound descends to that form; when the moment fails to be integrable the real integral takes its junk value and the bound is vacuous, so no integrability hypothesis beyond MemLp is needed.

The outer split at the exponent 3/8

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.integral_mul_indicator_le_moment_mul_measure {Omega : Type u_1} {mOmega : MeasurableSpace Omega} {mu : MeasureTheory.Measure Omega} [MeasureTheory.IsFiniteMeasure mu] {X : Omega → ℝ} {E : Set Omega} (hX0 : 0 ≤ᵐ[mu] X) (hmem : MeasureTheory.MemLp X (ENNReal.ofReal (8 / 5)) mu) (hE : MeasurableSet E) : ∫ (omega : Omega), X omega * E.indicator (fun (x : Omega) => 1) omega ∂mu ≤ (∫ (omega : Omega), X omega ^ (8 / 5) ∂mu) ^ (5 / 8) * mu.real E ^ (3 / 8)

The outer Hoelder split, at the honest tail exponent. For a nonnegative energy observable in L^{8/5} and a measurable bad event E,

  E[ X 1_E ]  <=  ( E[ X^{8/5} ] )^{5/8} . P[E]^{3/8} .

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.integral_mul_indicator_le_of_moment {Omega : Type u_1} {mOmega : MeasurableSpace Omega} {mu : MeasureTheory.Measure Omega} [MeasureTheory.IsFiniteMeasure mu] {X : Omega → ℝ} {E : Set Omega} (hX0 : 0 ≤ᵐ[mu] X) (hmem : MeasureTheory.MemLp X (ENNReal.ofReal (8 / 5)) mu) (hE : MeasurableSet E) {Emom tail : ℝ} (hmom : (∫ (omega : Omega), X omega ^ (8 / 5) ∂mu) ^ (5 / 8) ≤ Emom) (hEmom0 : 0 ≤ Emom) (htail : mu.real E ≤ tail) : ∫ (omega : Omega), X omega * E.indicator (fun (x : Omega) => 1) omega ∂mu ≤ Emom * tail ^ (3 / 8)

The one-cube bad-event energy bound. Composing the outer split with a moment budget Emom and a probability tail tail gives

  E[ X 1_E ]  <=  Emom . tail^{3/8} .