IncrementLp

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

e.kmn.bounds: the volume-normalized L^p mass of a stream increment

This module provides the volume-normalized L^p estimate e.kmn.bounds used in l.km.kn.Lp.estimates (ABK26),

  ⨍_{cu_l} |(k_m - k_n)(x)|^p dx
      <= O_{Gamma_{2/p}}( (C p)^{p/2} min{gamma^{-p/2}, (m-n)^{p/2}} 3^{gamma p m} ) ,

together with the norm-level estimate it supports and the exact algebraic interface through which the next node, e.kl.bounds.large, upgrades that estimate to the printed e.km.kn.Lp. The exact frozen all-p export now has a sorry-free proof term supplied by the later moment-boosted provider; that separate export, not the precursor declarations in this file, is the source-facing object.

The route

The manuscript derives e.kmn.bounds from the pointwise e.k.ell.upscales "by R^d-stationarity and Lemma l.Gamma.sigma.triangle".

1. the proved isBigOWith_gammaSigma_incrementAt gives, at every point x with one and the same amplitude A = C_d min{gamma^{-1/2},(m-n)^{1/2}} 3^{gamma m}, the tail bound |(k_m - k_n)(x)| = O_{Gamma_2}(A);
2. CoarseGraining's hasGammaMomentGrowthWith_of_isBigOWith_gammaSigma converts it to E|(k_m-k_n)(x)|^q <= ( q^{1/2})^q for every q >= 1, uniformly in x;
3. Jensen on the cube (streamIncrementLpMass_rpow_le, the cube average being a probability average) and Fubini give the same growth for the mass: E[(⨍|k_m-k_n|^p)^r] <= ( (pr)^{1/2})^{pr} = (^p p^{p/2} r^{p/2})^r;
4. CoarseGraining's isBigOWith_gammaSigma_of_hasGammaMomentGrowthWith_of_nonneg converts back, at Orlicz exponent 2/p.

This module's constants carry it, so no adjustment is needed downstream.

Historical scope and the later large-cube providers

The printed e.km.kn.Lp has two terms: a deterministic head and a random part carrying the large-scale gain 3^{-(d/p)(l-m)}. That gain is the content of e.kl.bounds.large, whose proof uses a.j.frd (finite range) and p.concentration on the average of the mass over the scale-m subcubes of cu_l. This precursor proves only the l-uniform estimate and supplies the transfer used by the later files IncrementLpGain.lean, IncrementLpLarge.lean, IncrementLpSquared.lean, and the translated-provider chain. Those later providers now implement the finite-range/stationarity route. The exact frozen all-p theorem is now wired to the ordinary provider in MomentBoostedLargeAllP.lean; this precursor itself makes no source-node status claim:

• isBigOWith_gammaSigma_two_rpow_inv — a Gamma_{2/p} mass tail at scale K has a Gamma_2 norm tail at scale K^{1/p}; every geometric gain in K has its exponent divided by p, so the mass gain 3^{-(d/2)(l-m)} of e.kl.bounds.large becomes the norm gain 3^{-(d/(2p))(l-m)}, i.e. 3^{-(d/8)(l-m)} at p = 4;
• streamIncrementLpNorm_head_tail_of_mass_head_tail — the packaged "deterministic head + geometrically decaying Gamma_2 tail" form, which is what the wave-oscillations step of p.bfA.multiscalebound needs for the third term O_{Gamma_{2(1+sigma)^{-1}}}(sigma^{-1} 3^{-(d/8)k_0}) of e.wave.influence.bound.

Disclosed conventions

• |·| is the exact Euclidean matrix operator norm Book.Ch02.matrixOperatorNorm, the same reading the proved e.k.ell.upscales, e.k.ell.upscales.infty and e.km.kn.Linfty use. (The L² display e.km.kn.L2.exact is a Frobenius statement, since it is an identity for j_k : j_{k'}; the two are related by matrixOperatorNorm_le_matrixFrobeniusNorm.)
• The resulting Gamma_{2/p} scale is e · (gammaMomentConst 2 · C_d · min{gamma^{-1/2},(m-n)^{1/2}} 3^{gamma m})^p · p^{p/2} — NOTE the gammaMomentConst 2 = 2e inside the p-th power. This implies the printed (Cp)^{p/2} min{.}^p 3^{gamma p m} with the source's generic C read as C:= e^2 · (2e · C_d)^2 (C^{p/2} ≥ e·(2e·C_d)^p for all p ≥ 1), a p-uniform dimension-only constant. C_d is the proved amplitude of e.k.ell.upscales (streamPointScale).
• No relation between l and m is used: e.kmn.bounds is stated in the source for every l, and the proof here is uniform in l.

Main definitions

• streamIncrementLpDensity, streamIncrementLpMass, streamIncrementLpNorm.
• streamPointScale: the proved Gamma_2 amplitude of e.k.ell.upscales.
• streamIncrementLpMassScale, streamIncrementLpNormScale.

Main results

• streamIncrementLpMass_rpow_le: Jensen on the cube.
• integral_streamIncrementLpMass_le, integrable_streamIncrementLpMass: the Fubini step.
• hasGammaMomentGrowthWith_streamIncrementLpMass, isBigOWith_gammaSigma_streamIncrementLpMass: e.kmn.bounds.
• isBigOWith_gammaSigma_streamIncrementLpNorm: its norm form.
• isBigOWith_gammaSigma_two_rpow_inv, streamIncrementLpNorm_head_tail_of_mass_head_tail: the additive interface for e.kl.bounds.large.

References

• ABK26, l.km.kn.Lp.estimates; e.kmn.bounds; e.kl.bounds.large; e.km.kn.Lp; e.k.ell.upscales.

The L^p density, mass and norm of a stream increment

noncomputable def Algsuperdiff.Section3.Provider.Stream.streamIncrementLpDensity {d : ℕ} (p : ℝ) (n m : ℤ) (omega : Cutoff.ShellSeq d) (x : HCPolySupport.Vec d) : ℝ

The p-th power of the pointwise size of the stream increment k_m - k_n, measured in the exact Euclidean matrix operator norm (the |·| of e.k.ell.upscales).

Equations

• Algsuperdiff.Section3.Provider.Stream.streamIncrementLpDensity p n m omega x = HCPolySupport.Book.Ch02.matrixOperatorNorm ((Algsuperdiff.Section3.Cutoff.finiteShellIncrement omega n m).toFun x) ^ p

noncomputable def Algsuperdiff.Section3.Provider.Stream.streamIncrementLpMass {d : ℕ} (p : ℝ) (l n m : ℤ) (omega : Cutoff.ShellSeq d) : ℝ

The volume-normalized L^p mass ⨍_{cu_l} |k_m - k_n|^p of a stream increment on the origin cube cu_l.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Algsuperdiff.Section3.Provider.Stream.streamIncrementLpNorm {d : ℕ} (p : ℝ) (l n m : ℤ) (omega : Cutoff.ShellSeq d) : ℝ

The volume-normalized L^p norm ‖k_m - k_n‖_{L^p(cu_l)} of a stream increment on the origin cube cu_l.

Equations

• Algsuperdiff.Section3.Provider.Stream.streamIncrementLpNorm p l n m omega = Algsuperdiff.Section3.Provider.Stream.streamIncrementLpMass p l n m omega ^ p⁻¹

theorem Algsuperdiff.Section3.Provider.Stream.streamIncrementLpDensity_nonneg {d : ℕ} (p : ℝ) (n m : ℤ) (omega : Cutoff.ShellSeq d) (x : HCPolySupport.Vec d) : 0 ≤ streamIncrementLpDensity p n m omega x

Continuity, measurability and integrability of the density

theorem Algsuperdiff.Section3.Provider.Stream.continuous_streamIncrementLpDensity {d : ℕ} {p : ℝ} (hp : 0 < p) (n m : ℤ) (omega : Cutoff.ShellSeq d) : Continuous (streamIncrementLpDensity p n m omega)

The L^p density is continuous in the point.

theorem Algsuperdiff.Section3.Provider.Stream.measurable_streamIncrementLpDensity {d : ℕ} (p : ℝ) (n m : ℤ) (x : HCPolySupport.Vec d) : Measurable fun (omega : Cutoff.ShellSeq d) => streamIncrementLpDensity p n m omega x

The L^p density at a fixed point is measurable in the sample.

theorem Algsuperdiff.Section3.Provider.Stream.measurable_uncurry_streamIncrementLpDensity {d : ℕ} {p : ℝ} (hp : 0 < p) (n m : ℤ) : Measurable (Function.uncurry fun (x : HCPolySupport.Vec d) (omega : Cutoff.ShellSeq d) => streamIncrementLpDensity p n m omega x)

Carathéodory joint measurability of the L^p density.

theorem Algsuperdiff.Section3.Provider.Stream.integrableOn_streamIncrementLpDensity {d : ℕ} {p : ℝ} (hp : 0 < p) (l n m : ℤ) (omega : Cutoff.ShellSeq d) : MeasureTheory.IntegrableOn (streamIncrementLpDensity p n m omega) (HCPolySupport.openCubeSet (HCPolySupport.originCube d l)) MeasureTheory.volume

The L^p density is integrable on every origin cube: it is continuous and the cube is bounded.

The cube average as a Mathlib set average

theorem Algsuperdiff.Section3.Provider.Stream.streamIncrementLpMass_nonneg {d : ℕ} (p : ℝ) (l n m : ℤ) (omega : Cutoff.ShellSeq d) : 0 ≤ streamIncrementLpMass p l n m omega

The volume-normalized L^p mass is nonnegative.

theorem Algsuperdiff.Section3.Provider.Stream.streamIncrementLpNorm_nonneg {d : ℕ} (p : ℝ) (l n m : ℤ) (omega : Cutoff.ShellSeq d) : 0 ≤ streamIncrementLpNorm p l n m omega

The volume-normalized L^p norm is nonnegative.

Jensen's inequality on the cube

theorem Algsuperdiff.Section3.Provider.Stream.streamIncrementLpMass_rpow_le {d : ℕ} {p r : ℝ} (hp : 0 < p) (hr : 1 ≤ r) (l n m : ℤ) (omega : Cutoff.ShellSeq d) : streamIncrementLpMass p l n m omega ^ r ≤ streamIncrementLpMass (p * r) l n m omega

Jensen's inequality for the cube mass. Raising the L^p mass to a power r ≥ 1 is dominated by the L^{pr} mass, because the cube average is a probability average.

The pointwise moment growth of e.k.ell.upscales

noncomputable def Algsuperdiff.Section3.Provider.Stream.streamPointScale {d : ℕ} (M : ABKModel d) (n m : ℤ) : ℝ

The Γ₂ amplitude of the proved e.k.ell.upscales at a point (isBigOWith_gammaSigma_incrementAt).

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section3.Provider.Stream.streamPointScale_pos {d : ℕ} (M : ABKModel d) {n m : ℤ} (hnm : n < m) : 0 < streamPointScale M n m

theorem Algsuperdiff.Section3.Provider.Stream.hasGammaMomentGrowthWith_incrementAt {d : ℕ} (M : ABKModel d) {n m : ℤ} (hnm : n < m) (x : HCPolySupport.Vec d) : HCPolySupport.IndependentSums.HasGammaMomentGrowthWith (↑M.P) 2 (fun (omega : Cutoff.ShellSeq d) => HCPolySupport.Book.Ch02.matrixOperatorNorm ((Cutoff.finiteShellIncrement omega n m).toFun x)) (HCPolySupport.IndependentSums.gammaMomentConst 2 * streamPointScale M n m)

Absolute moment growth of the pointwise increment size, uniform in the point. This is the moment form of the proved e.k.ell.upscales.

Fubini on the cube

theorem Algsuperdiff.Section3.Provider.Stream.integrable_streamIncrementLpMass {d : ℕ} (M : ABKModel d) {q : ℝ} (hq : 1 ≤ q) {n m : ℤ} (hnm : n < m) (l : ℤ) : MeasureTheory.Integrable (streamIncrementLpMass q l n m) ↑M.P

The cube L^q mass of the increment is integrable.

theorem Algsuperdiff.Section3.Provider.Stream.integral_streamIncrementLpMass_le {d : ℕ} (M : ABKModel d) {q : ℝ} (hq : 1 ≤ q) {n m : ℤ} (hnm : n < m) (l : ℤ) : ∫ (omega : Cutoff.ShellSeq d), streamIncrementLpMass q l n m omega ∂↑M.P ≤ (HCPolySupport.IndependentSums.gammaMomentConst 2 * streamPointScale M n m * q ^ 2⁻¹) ^ q

The cube L^q mass inherits the pointwise moment bound. Fubini turns the uniform-in-x moment estimate of e.k.ell.upscales into the same estimate for the volume-normalized mass.

Numeric preliminaries

The one real-power identity behind the passage from the L^{pr} moment bound to Γ_{2/p} moment growth, isolated from every probabilistic statement.

e.kmn.bounds

theorem Algsuperdiff.Section3.Provider.Stream.hasGammaMomentGrowthWith_streamIncrementLpMass {d : ℕ} (M : ABKModel d) {p : ℝ} (hp : 1 ≤ p) {n m : ℤ} (hnm : n < m) (l : ℤ) : HCPolySupport.IndependentSums.HasGammaMomentGrowthWith (↑M.P) (2 / p) (streamIncrementLpMass p l n m) ((HCPolySupport.IndependentSums.gammaMomentConst 2 * streamPointScale M n m) ^ p * p ^ (p / 2))

The Γ_{2/p} moment growth of the cube L^p mass: Jensen on the cube plus the uniform pointwise moment bound.

noncomputable def Algsuperdiff.Section3.Provider.Stream.streamIncrementLpMassScale {d : ℕ} (M : ABKModel d) (p : ℝ) (n m : ℤ) : ℝ

The Γ_{2/p} scale of e.kmn.bounds: the p-th power of the pointwise e.k.ell.upscales amplitude, times the moment factor p^{p/2}, times the universal e of the moment-to-tail conversion.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section3.Provider.Stream.streamIncrementLpMassScale_pos {d : ℕ} (M : ABKModel d) {p : ℝ} (hp : 1 ≤ p) {n m : ℤ} (hnm : n < m) : 0 < streamIncrementLpMassScale M p n m

theorem Algsuperdiff.Section3.Provider.Stream.isBigOWith_gammaSigma_streamIncrementLpMass {d : ℕ} (M : ABKModel d) {p : ℝ} (hp : 1 ≤ p) {n m : ℤ} (hnm : n < m) (l : ℤ) : HCPolySupport.IndependentSums.IsBigOWith (↑M.P) (HCPolySupport.IndependentSums.gammaSigma (2 / p)) (streamIncrementLpMass p l n m) (streamIncrementLpMassScale M p n m)

ABK26's e.kmn.bounds:

⨍_{cu_l} |(k_m - k_n)(x)|^p dx ≤ O_{Γ_{2/p}}( (C p)^{p/2} min{γ^{-p/2}, (m-n)^{p/2}} 3^{γ p m} ),

for every p ≥ 1 and every l, m, n ∈ ℤ with n < m (no relation between l and m is used). The resulting scale is e · (C_d min{γ^{-1/2},(m-n)^{1/2}} 3^{γ m})^p · p^{p/2}, which is the printed right-hand side with the source's generic C read as C_d^2.

The mass-to-norm transfer

theorem Algsuperdiff.Section3.Provider.Stream.isBigOWith_gammaSigma_two_rpow_inv {Omega : Type u_1} [MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} [MeasureTheory.IsFiniteMeasure mu] {T : Omega → ℝ} {p K : ℝ} (hp : 0 < p) (hK : 0 ≤ K) (hT_nonneg : ∀ (omega : Omega), 0 ≤ T omega) (hT : HCPolySupport.IndependentSums.IsBigOWith mu (HCPolySupport.IndependentSums.gammaSigma (2 / p)) T K) : HCPolySupport.IndependentSums.IsBigOWith mu (HCPolySupport.IndependentSums.gammaSigma 2) (fun (omega : Omega) => T omega ^ p⁻¹) (K ^ p⁻¹)

The Γ bookkeeping of the 1/p-th root. A nonnegative O_{Γ_{2/p}}(K) mass-level quantity has an O_{Γ₂}(K^{1/p}) 1/p-th root.

Every geometric gain carried by K therefore has its exponent divided by p; at p = 4 a mass gain 3^{-(d/2)(l-m)} becomes the norm gain 3^{-(d/8)(l-m)}, which is the 3^{-(d/8)k₀} of e.wave.influence.bound.

theorem Algsuperdiff.Section3.Provider.Stream.rpow_inv_le_add_rpow_inv_of_le_add {p H T z : ℝ} (hp : 1 ≤ p) (hH : 0 ≤ H) (hT : 0 ≤ T) (hz : 0 ≤ z) (hle : z ≤ H + T) : z ^ p⁻¹ ≤ H ^ p⁻¹ + T ^ p⁻¹

The deterministic half of the mass-to-norm transfer. Subadditivity of t ↦ t^{1/p} splits a mass bound mass ≤ H + T into the norm bound mass^{1/p} ≤ H^{1/p} + T^{1/p}, keeping the deterministic head deterministic.

The norm-level estimate available from e.kmn.bounds alone

noncomputable def Algsuperdiff.Section3.Provider.Stream.streamIncrementLpNormScale {d : ℕ} (M : ABKModel d) (p : ℝ) (n m : ℤ) : ℝ

The Γ₂ scale of the L^p norm delivered by e.kmn.bounds, before the finite-range improvement e.kl.bounds.large.

Equations

• Algsuperdiff.Section3.Provider.Stream.streamIncrementLpNormScale M p n m = Algsuperdiff.Section3.Provider.Stream.streamIncrementLpMassScale M p n m ^ p⁻¹

theorem Algsuperdiff.Section3.Provider.Stream.isBigOWith_gammaSigma_streamIncrementLpNorm {d : ℕ} (M : ABKModel d) {p : ℝ} (hp : 1 ≤ p) {n m : ℤ} (hnm : n < m) (l : ℤ) : HCPolySupport.IndependentSums.IsBigOWith (↑M.P) (HCPolySupport.IndependentSums.gammaSigma 2) (streamIncrementLpNorm p l n m) (streamIncrementLpNormScale M p n m)

The 1/p-th root of e.kmn.bounds:

‖k_m - k_n‖_{L^p(cu_l)} ≤ O_{Γ₂}( (C p)^{1/2} min{γ^{-1/2}, (m-n)^{1/2}} 3^{γ m} ).

This is the norm-level estimate that e.kmn.bounds alone supports: a single Γ₂ envelope, uniform in l, with no large-scale gain. The printed e.km.kn.Lp (in the form corrected) additionally splits off a deterministic head and gains the factor 3^{-(d/(2p))(l-m)} on the random part; that improvement is the content of e.kl.bounds.large, which is not proved in this precursor. It is supplied by the later large-cube provider chain culminating in MomentBoostedLargeAllP.lean. See isBigOWith_gammaSigma_two_rpow_inv for the transfer that turns the improved mass estimate into the improved norm estimate with no restatement. The exact frozen export is maintained separately from this helper theorem.

The wave-facing packaging

theorem Algsuperdiff.Section3.Provider.Stream.streamIncrementLpNorm_head_tail_of_mass_head_tail {d : ℕ} (M : ABKModel d) {p : ℝ} (hp : 1 ≤ p) (l n m : ℤ) {H K : ℝ} {T : Cutoff.ShellSeq d → ℝ} (hH : 0 ≤ H) (hK : 0 ≤ K) (hT_nonneg : ∀ (omega : Cutoff.ShellSeq d), 0 ≤ T omega) (hmass : ∀ (omega : Cutoff.ShellSeq d), streamIncrementLpMass p l n m omega ≤ H + T omega) (hT : HCPolySupport.IndependentSums.IsBigOWith (↑M.P) (HCPolySupport.IndependentSums.gammaSigma (2 / p)) T K) : (∀ (omega : Cutoff.ShellSeq d), streamIncrementLpNorm p l n m omega ≤ H ^ p⁻¹ + T omega ^ p⁻¹) ∧ HCPolySupport.IndependentSums.IsBigOWith (↑M.P) (HCPolySupport.IndependentSums.gammaSigma 2) (fun (omega : ℤ → Frozen.Assumptions.ShellField d) => T omega ^ p⁻¹) (K ^ p⁻¹)

The shape the wave-oscillations step of p.bfA.multiscalebound consumes.

Whenever the cube L^p mass of a stream increment is dominated by a deterministic head H plus a nonnegative tail T obeying a Γ_{2/p} bound at scale K, the L^p norm is dominated by the deterministic head H^{1/p} plus a tail obeying a Γ₂ bound at scale K^{1/p}.

This is the exact interface for e.kl.bounds.large: with H = (Cp)^{p/2} A^{p/2} and K = (Cp)^{p/2} A^{p/2} 3^{-(d/2)(l-m)}, A = min{γ^{-1}, m-n} 3^{2γm}, the conclusion is the corrected e.km.kn.Lp in the form (Cp)^{1/2} A^{1/2} + O_{Γ₂}((Cp)^{1/2} A^{1/2} 3^{-(d/(2p))(l-m)}), whose p = 4 instance carries the 3^{-(d/8)(l-m)} gain of the third term of e.wave.influence.bound.