MomentHolder

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

Step 5's Hölder bookkeeping, in the anchor's lintegral normal form

What this module supplies

Step 5 of the proof of l.bounds.mathcal.E.aL reads:

Using these estimates, the restrictions m − n ≤ γ^{-1} and p ≤ C^{-1}γ^{-1}s and Hölder's inequality, it is straightforward to see that the p-th root of the sum over j ≤ n of the p/2-th moment of the first and third terms ... is bounded by the right side.

Each term of e.apply.sensitivity.J.aL is a PRODUCT of the Step-4 bullets, and each bullet is available at EVERY moment q ∈ [1,∞) (that is exactly what the hence, for every q sentences of Step 4 deliver). Hölder therefore costs nothing except a uniform boost of the exponent by the number of factors.

• lintegral_rpow_prod_le_of_moments — an N-factor product whose factors each obey the normal form at the boosted exponent N q obeys it at q, with the product of the majorants. This is the reconstruction of the source's "Hölder's inequality" for the four terms.
• lintegral_rpow_mul_le_of_moments — the two-factor instance, spelled out.
• lintegral_rpow_sum_le_of_moments — the companion ℝ≥0∞ Minkowski step for a finite SUM of terms (the three summands of e.apply.sensitivity.J.aL, and the primal/adjoint pair of lFreeStep3Majorant), at q ≥ 1.

Both engines are exponent-neutral: no γ-power and no s-power is moved, and no constant beyond the product/sum of the caller's own majorants is introduced.

References

• Mathlib: ENNReal.lintegral_prod_norm_pow_le, ENNReal.lintegral_Lp_add_le.

1. Two ℝ≥0∞ product identities

2. Hölder for a finite product, in the anchor's normal form

theorem Algsuperdiff.Section4.Provider.BoundsEaL.lintegral_rpow_mul_le_of_moments {Omega : Type u_1} [MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} {X Y : Omega → ENNReal} {RX RY q : ℝ} (hq : 0 < q) (hXm : AEMeasurable X mu) (hYm : AEMeasurable Y mu) (hRX : 0 ≤ RX) (hX : ∫⁻ (omega : Omega), X omega ^ (2 * q) ∂mu ≤ ENNReal.ofReal RX ^ (2 * q)) (hY : ∫⁻ (omega : Omega), Y omega ^ (2 * q) ∂mu ≤ ENNReal.ofReal RY ^ (2 * q)) : ∫⁻ (omega : Omega), (X omega * Y omega) ^ q ∂mu ≤ ENNReal.ofReal (RX * RY) ^ q

The two-factor Hölder step, spelled out: a product of two observables, each controlled at the doubled exponent 2q.

3. The companion Minkowski step for a finite sum