MinkowskiLp

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

Countable Minkowski in L^q, on ℝ≥0∞

Nothing here imports that file, and nothing here claims the anchor. Everything below is abstract measure theory on ℝ≥0∞: no model, no carrier, no cube occurs.

What is here

Mathlib supplies Minkowski's inequality in L^q on ℝ≥0∞ for TWO functions (ENNReal.lintegral_Lp_add_le). This module supplies exactly that, and nothing else:

• lintegral_rpow_finsetSum_le — the finite-sum form, by induction on the index Finset from Mathlib's two-function inequality;
• lintegral_rpow_tsum_le_tsum_rpow — the countable form, by monotone convergence (lintegral_iSup') along the partial sums;
• lintegral_rpow_tsum_le_rpow_tsum — the same with both sides raised to the q-th power, which is the shape the transport consumes.

No sign or summability side condition is needed anywhere: on ℝ≥0∞ a tsum is the supremum of its partial sums, so a divergent family simply makes both sides ⊤.

References

• ABK26, l.bounds.mathcal.E.aL, Step 5.

theorem Algsuperdiff.Section4.Provider.BoundsEaL.iSup_rpow_of_pos {iota : Sort u_2} (f : iota → ENNReal) {q : ℝ} (hq : 0 < q) : (⨆ (i : iota), f i) ^ q = ⨆ (i : iota), f i ^ q

A positive ℝ≥0∞ power commutes with suprema. Disclosed re-derivation of AeMeasurableTransport.lean's private iSup_rpow_of_pos', made public here because the Minkowski-ordered transport consumes it at the anchor's sup_L.

theorem Algsuperdiff.Section4.Provider.BoundsEaL.lintegral_rpow_finsetSum_le {Omega : Type u_1} [MeasurableSpace Omega] {iota : Type u_2} {mu : MeasureTheory.Measure Omega} {q : ℝ} (hq : 1 ≤ q) (F : iota → Omega → ENNReal) (hF : ∀ (i : iota), AEMeasurable (F i) mu) (t : Finset iota) : (∫⁻ (omega : Omega), (∑ i ∈ t, F i omega) ^ q ∂mu) ^ (1 / q) ≤ ∑ i ∈ t, (∫⁻ (omega : Omega), F i omega ^ q ∂mu) ^ (1 / q)

Minkowski in L^q for a finite family of ℝ≥0∞-valued functions.

For q ≥ 1 and a.e. measurable F i,

( ∫⁻ (∑_{i ∈ t} F i)^q )^{1/q}  ≤  ∑_{i ∈ t} ( ∫⁻ (F i)^q )^{1/q} .

The induction step is Mathlib's two-function ENNReal.lintegral_Lp_add_le.

theorem Algsuperdiff.Section4.Provider.BoundsEaL.lintegral_rpow_tsum_le_tsum_rpow {Omega : Type u_1} [MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} {q : ℝ} (hq : 1 ≤ q) (F : ℕ → Omega → ENNReal) (hF : ∀ (l : ℕ), AEMeasurable (F l) mu) : (∫⁻ (omega : Omega), (∑' (l : ℕ), F l omega) ^ q ∂mu) ^ (1 / q) ≤ ∑' (l : ℕ), (∫⁻ (omega : Omega), F l omega ^ q ∂mu) ^ (1 / q)

For q ≥ 1 and a.e. measurable F l,

( ∫⁻ (∑'_l F l)^q )^{1/q}  ≤  ∑'_l ( ∫⁻ (F l)^q )^{1/q} .

Both sides are suprema of their partial-sum truncations -- the left one by monotone convergence, the right one by the ℝ≥0∞ tsum -- so the finite form above passes to the limit with no summability hypothesis.

theorem Algsuperdiff.Section4.Provider.BoundsEaL.lintegral_rpow_tsum_le_rpow_tsum {Omega : Type u_1} [MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} {q : ℝ} (hq : 1 ≤ q) (F : ℕ → Omega → ENNReal) (hF : ∀ (l : ℕ), AEMeasurable (F l) mu) : ∫⁻ (omega : Omega), (∑' (l : ℕ), F l omega) ^ q ∂mu ≤ (∑' (l : ℕ), (∫⁻ (omega : Omega), F l omega ^ q ∂mu) ^ (1 / q)) ^ q

The countable Minkowski inequality, in the shape the Step-5 transport consumes: both sides raised to the q-th power.