IncrementLpLarge

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

e.kl.bounds.large: the unconditional head-plus-gain estimate

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

for every l, with no relation between l and m: the printed binder n < m <= l is not needed, and neither is the partition-regime binder m + c <= l of the existing Provider/Stream/IncrementLpGain.lean. The l-window split is internal to the proof.

The two ingredients

The existing IncrementLpGain.streamIncrementLpMass_head_tail provides the partition-regime estimate m + c <= l conditionally on one abstract input, hX0: a Gamma_sigma bound for the restriction-centered unit-cube observable of the partition-normalized law. This module proves that input and assembles both regimes.

The centering bookkeeping

hX0 comes from the existing e.kmn.bounds provider at the single scale l = m + c, centered. The passage from the raw bound to the centered bound costs nothing:

isBigO_sub_const_of_isBigOWith_of_nonneg — if X >= 0 obeys X <= O_Psi(K) and c ∈ [0, K], then X - c = O_Psi(K), with the same constant K.

The honest constant is 1, not 2: for t >= 1 the shifted tail event {|X - c| > K t} is contained in the raw tail event {X > K t}, because (i) upward, X - c > K t forces X > K t + c >= K t as c >= 0, and (ii) downward, c - X <= c <= K <= K t, so the downward branch of the absolute value is empty. No Gamma-constant absorption and no monotonicity of Psi is used; the lemma holds for an arbitrary tail function Psi. The hypothesis c <= K is supplied by integral_streamIncrementLpMass_le — the mean of a nonnegative observable never exceeds its own Gamma scale.

The transport

isBigOWith_map_of_isBigOWith_comp is the push-forward transport in the direction opposite to the existing isBigOWith_comp_of_isBigO_map: a tail bound for g ∘ F on the sample space is a tail bound for g under F_* mu. Both are the same preimage identity; the two directions are needed at the two ends of the argument (hX0 is stated on the law, e.kmn.bounds is proved on ShellSeq).

The two regimes and the enlarged C(d)

• m + c <= l (the partition regime). streamIncrementLpMass_head_tail gives mass <= E[mass_{m+c}] + |mass_l - E[mass_{m+c}]| with the second term in O_{Gamma_{2/p}} of gammaSigmaDescendantsAtScaleConst d 0 (2/p) * 3^{-(d/2)(l-m-c)} * K. The identity partitionCardinalityScale_originCube_zero evaluates CoarseGraining's cardinality scale as 3^{-(d/2)(l-m-c)} = 3^{(d/2)c} 3^{-(d/2)(l-m)}, i.e. the printed gain times a dimensional constant.
• l < m + c (the complementary regime). Here the partition is not available, and the estimate uses the existing l-uniform e.kmn.bounds with head 0: since l - m < c, the printed gain 3^{-(d/2)(l-m)} exceeds 3^{-(d/2)c}, so the ungained amplitude is dominated by the gained one after the same enlargement 3^{(d/2)c} of C(d).

The tail observable is defined by the same case split, streamIncrementLpTail; it is an explicit function of the sample, not an existential.

Disclosed conventions and limitations

• The head streamIncrementLpMassHead is literally the right-hand side of the existing integral_streamIncrementLpMass_le, i.e. (gammaMomentConst 2 · C_d · A^{1/2} · p^{1/2})^p = ((gammaMomentConst 2 · C_d)^2 p)^{p/2} A^{p/2}, the corrected head with the source's C(d) read as (2e · C_d)^2. The p^{p/2} that the printed display drops is carried.
• The Orlicz exponent is 2/p, as printed; the norm-level corollary is its 1/p-th root, so the mass gain 3^{-(d/2)(l-m)} becomes the norm gain 3^{-(d/(2p))(l-m)} — at p = 4 the 3^{-(d/8)(l-m)} of e.wave.influence.bound. The mass-level gain exponent is d/2 for every p ≥ 1 (the partition fluctuation is the square root of the cell count, and p enters only through the Orlicz class and the amplitude).
• The complementary regime carries no improvement. For l < m + c the conclusion is the existing l-uniform e.kmn.bounds rewritten at the larger amplitude, with the whole mass in the random part; the genuine geometric gain exists only in the partition regime m + c ≤ l, which is the regime the source's binder m ≤ l was aiming at. Stating the theorem for every l costs only the constant 3^{(d/2)c} and removes a binder; it does not claim decay where none is available.
• |·| is Book.Ch02.matrixOperatorNorm throughout, as in the existing e.kmn.bounds.

Main definitions

• streamIncrementLpMassHead — the corrected deterministic head.
• streamIncrementLpTail — the random part, defined by the internal window split.
• streamIncrementLpGainConst, streamIncrementLpGainScale — the uniform amplitude of the random part.

Main results

• isBigO_sub_const_of_isBigOWith_of_nonneg — the centering bookkeeping.
• isBigOWith_map_of_isBigOWith_comp — the push-forward transport.
• isBigO_gammaSigma_centeredOriginObservable_regFieldLpMassRep — the local Provider for hX0.
• partitionCardinalityScale_originCube_zero — CoarseGraining's cardinality scale as the printed geometric gain.
• streamIncrementLpMass_head_tail_gain — the local Provider estimate corresponding to corrected e.kl.bounds.large, unconditional in l.
• streamIncrementLpNorm_head_tail_gain — the unsquared Γ₂ of the corrected e.km.kn.Lp, unconditional in l (the squared Γ₁ form is proved in IncrementLpSquared.lean; no node status is assigned here).

References

• ABK26, e.kl.bounds.large; e.kmn.bounds; e.km.kn.Lp; p.concentration; a.j.frd.
• Provider/Stream/IncrementLp.lean (e.kmn.bounds and the mass-to-norm interface), Provider/Stream/IncrementLpGain.lean (the partition-regime head/tail package), Provider/Stream/IncrementMassRepresentative.lean (the measurable local representative).

theorem Algsuperdiff.Section3.Provider.Stream.measurable_streamIncrementLpMass {d : ℕ} {p : ℝ} (hp : 0 < p) (l n m : ℤ) : Measurable (streamIncrementLpMass p l n m)

The volume-normalized cube L^p mass is a measurable shell observable.

Centering a nonnegative weak-Orlicz observable

theorem Algsuperdiff.Section3.Provider.Stream.isBigO_sub_const_of_isBigOWith_of_nonneg {Omega : Type u_1} [MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} [MeasureTheory.IsFiniteMeasure mu] {Psi : ℝ → ℝ} {X : Omega → ℝ} {K c : ℝ} (hc0 : 0 ≤ c) (hcK : c ≤ K) (hX0 : ∀ (omega : Omega), 0 ≤ X omega) (hX : HCPolySupport.IndependentSums.IsBigOWith mu Psi X K) : HCPolySupport.IndependentSums.IsBigO mu Psi (fun (omega : Omega) => X omega - c) K

The centering bookkeeping, at constant 1. Subtracting a constant c ∈ [0, K] from a nonnegative observable with a Psi tail at scale K leaves the tail at the same scale K.

The downward branch of the absolute value contributes nothing: c - X ≤ c ≤ K never exceeds K t for t ≥ 1; the upward branch is contained in the raw tail because c ≥ 0. No property of Psi is used.

Transport along a push-forward

theorem Algsuperdiff.Section3.Provider.Stream.isBigOWith_map_of_isBigOWith_comp {d : ℕ} {Omega : Type u_1} [MeasurableSpace Omega] (mu : MeasureTheory.Measure Omega) {F : Omega → HCPolySupport.RegCoeffField d} (hF : Measurable F) {g : HCPolySupport.RegCoeffField d → ℝ} (hg : Measurable g) {Psi : ℝ → ℝ} {A : ℝ} (h : HCPolySupport.IndependentSums.IsBigOWith mu Psi (fun (omega : Omega) => g (F omega)) A) : HCPolySupport.IndependentSums.IsBigOWith (MeasureTheory.Measure.map F mu) Psi g A

A Psi tail bound for a composition g ∘ F on the sample space is the same bound for g under the push-forward law. This is the direction opposite to the existing isBigOWith_comp_of_isBigO_map.

The deterministic head

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

The corrected head of e.kl.bounds.large: the right-hand side of the existing integral_streamIncrementLpMass_le, i.e. (C(d) p)^{p/2} A^{p/2} with A = min{gamma^{-1}, m-n} 3^{2 gamma m}.

Equations

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

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

theorem Algsuperdiff.Section3.Provider.Stream.streamIncrementLpMassScale_eq_exp_mul_head {d : ℕ} (M : ABKModel d) {p : ℝ} (hp : 1 ≤ p) {n m : ℤ} (hnm : n < m) : streamIncrementLpMassScale M p n m = Real.exp 1 * streamIncrementLpMassHead M p n m

The existing Gamma_{2/p} scale of e.kmn.bounds is the head times the universal e of the moment-to-tail conversion.

theorem Algsuperdiff.Section3.Provider.Stream.integral_streamIncrementLpMass_le_head {d : ℕ} (M : ABKModel d) {p : ℝ} (hp : 1 ≤ p) {n m : ℤ} (hnm : n < m) (l : ℤ) : ∫ (omega : Cutoff.ShellSeq d), streamIncrementLpMass p l n m omega ∂↑M.P ≤ streamIncrementLpMassHead M p n m

The head dominates the mean. This is integral_streamIncrementLpMass_le read at the head.

theorem Algsuperdiff.Section3.Provider.Stream.integral_streamIncrementLpMass_le_massScale {d : ℕ} (M : ABKModel d) {p : ℝ} (hp : 1 ≤ p) {n m : ℤ} (hnm : n < m) (l : ℤ) : ∫ (omega : Cutoff.ShellSeq d), streamIncrementLpMass p l n m omega ∂↑M.P ≤ streamIncrementLpMassScale M p n m

The mean is below the Gamma_{2/p} scale of e.kmn.bounds: the shift budget of the centering lemma.

Discharging the origin-cube hypothesis hX0

theorem Algsuperdiff.Section3.Provider.Stream.regFieldLpMassRep_originCube_zero_partitionIncrement {d : ℕ} {p : ℝ} (hp : 0 < p) (n m : ℤ) (omega : Cutoff.ShellSeq d) : regFieldLpMassRep p (HCPolySupport.cubeSet (HCPolySupport.originCube d 0)) (HCPolySupport.smulReg (incrementPartitionScale d m) ⋯ (Cutoff.finiteShellIncrement omega n m)) = streamIncrementLpMass p (m + ↑(incrementPartitionShift d)) n m omega

The unit-cube observable of the partition-normalized law, read at a sample, is the cube mass of the increment at the single scale m + c.

This is the pointwise step that the existing integral_regFieldLpMassRep_originCube_zero performs inside its own proof; it is restated here (same two rewrites, no drift) because that file exposes only the integrated form, and the tail argument needs the sample-wise identity.

theorem Algsuperdiff.Section3.Provider.Stream.isBigO_gammaSigma_centeredOriginObservable_regFieldLpMassRep {d : ℕ} (M : ABKModel d) {p : ℝ} (hp : 1 ≤ p) {n m : ℤ} (hnm : n < m) : HCPolySupport.Book.Ch04.IsBigO (partitionStreamIncrementLaw M n m) (HCPolySupport.Book.Ch04.gammaSigma (2 / p)) (HCPolySupport.Book.Ch04.restrictionCenteredOriginObservable (partitionStreamIncrementLaw M n m) 0 (regFieldLpMassRep p)) (streamIncrementLpMassScale M p n m)

The hX0 input of streamIncrementLpMass_head_tail, proved locally.

It applies the existing e.kmn.bounds provider at the single scale l = m + c, restriction-centers by its own mean, and transports to the partition-normalized law. No additional probabilistic input is used.

The geometric partition gain

theorem Algsuperdiff.Section3.Provider.Stream.partitionCardinalityScale_originCube_zero {d : ℕ} {j : ℤ} (hj : 0 ≤ j) : HCPolySupport.Book.Ch04.partitionCardinalityScale 0 j = 3 ^ (-(↑d / 2) * ↑j)

CoarseGraining's cardinality fluctuation scale, evaluated. The scale-0 partition of the origin cube at scale j ≥ 0 has 3^{dj} cells, so its square-root fluctuation factor is the geometric gain 3^{-(d/2)j}.

The uniform amplitude

noncomputable def Algsuperdiff.Section3.Provider.Stream.streamIncrementLpGainConst (d : ℕ) (sigma : ℝ) : ℝ

The gain-amplitude constant: the universal e of the moment-to-tail conversion, the partition-normalization loss 3^{(d/2)c} with 3^c > 2 sqrt d, and CoarseGraining's colouring constant (raised to at least 1, so that the complementary regime l < m + c is covered by the same amplitude). Note that at general p this is not a C(d): the colouring constant gammaSigmaDescendantsAtScaleConst d 0 (2/p) grows like exp(Θ(p²)) (dominated by CoarseGraining's gammaSigmaLogControlConst σ = exp(32/σ²) at σ = 2/p; the p^{Θ(p)} triangle/Γ factors are swamped), so in the printed (C·p)^{p/2} shape the C is e^{Θ(p)} — exponentially p-dependent, outside the node's stated scope C = C(d). At the wave consumer's fixed p = 4 it is a genuine number. A C(d)-uniform tail constant, if the node needs one at general p, is a separate obligation.

Equations

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

theorem Algsuperdiff.Section3.Provider.Stream.streamIncrementLpGainConst_pos (d : ℕ) (sigma : ℝ) : 0 < streamIncrementLpGainConst d sigma

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

The amplitude of the random part: streamIncrementLpGainConst (NOT a C(d) at general p — see its disclosure) times 3^{-(d/2)(l-m)} times the corrected head.

Equations

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

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

theorem Algsuperdiff.Section3.Provider.Stream.partitionScale_le_streamIncrementLpGainScale {d : ℕ} (M : ABKModel d) {p : ℝ} (hp : 1 ≤ p) {n m l : ℤ} (hnm : n < m) (hsl : m + ↑(incrementPartitionShift d) ≤ l) : HCPolySupport.Book.Ch04.gammaSigmaDescendantsAtScaleConst d 0 (2 / p) * HCPolySupport.Book.Ch04.partitionCardinalityScale 0 (l - (m + ↑(incrementPartitionShift d))) * streamIncrementLpMassScale M p n m ≤ streamIncrementLpGainScale M p l n m

The partition-regime amplitude of streamIncrementLpMass_head_tail is below the uniform amplitude.

theorem Algsuperdiff.Section3.Provider.Stream.massScale_le_streamIncrementLpGainScale {d : ℕ} (M : ABKModel d) {p : ℝ} (hp : 1 ≤ p) {n m l : ℤ} (hnm : n < m) (hsl : ¬m + ↑(incrementPartitionShift d) ≤ l) : streamIncrementLpMassScale M p n m ≤ streamIncrementLpGainScale M p l n m

The complementary-regime amplitude of e.kmn.bounds is below the uniform amplitude: for l < m + c the printed gain exceeds 3^{-(d/2)c}, which the enlarged constant absorbs.

The random part

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

The random part of e.kl.bounds.large, defined by the internal window split: in the partition regime m + c ≤ l it is the fluctuation of the cube mass about its scale-(m+c) mean; in the complementary regime l < m + c it is the cube mass itself.

Equations

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

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

e.kl.bounds.large

theorem Algsuperdiff.Section3.Provider.Stream.streamIncrementLpMass_head_tail_gain {d : ℕ} (M : ABKModel d) {p : ℝ} (hp : 1 ≤ p) {n m : ℤ} (hnm : n < m) (l : ℤ) : (∀ (omega : Cutoff.ShellSeq d), 0 ≤ streamIncrementLpTail M p l n m omega) ∧ (∀ (omega : Cutoff.ShellSeq d), streamIncrementLpMass p l n m omega ≤ streamIncrementLpMassHead M p n m + streamIncrementLpTail M p l n m omega) ∧ HCPolySupport.IndependentSums.IsBigOWith (↑M.P) (HCPolySupport.IndependentSums.gammaSigma (2 / p)) (streamIncrementLpTail M p l n m) (streamIncrementLpGainScale M p l n m)

ABK26's e.kl.bounds.large in the form corrected:

`⨍_{cu_l} |(k_m - k_n)(x)|^p dx ≤ (C(d)p)^{p/2} A^{p/2}

• O_{Γ_{2/p}}((C(d)p)^{p/2} A^{p/2} 3^{-(d/2)(l-m)}), A = min{γ^{-1}, m-n} 3^{2γm}`,

for every p ≥ 1, every n < m and every l ∈ ℤ (the printed m ≤ l is not used). The three conjuncts are exactly the nonnegativity, the pointwise mass decomposition and the Γ_{2/p} tail bound consumed by streamIncrementLpNorm_head_tail_of_mass_head_tail.

theorem Algsuperdiff.Section3.Provider.Stream.streamIncrementLpNorm_head_tail_gain {d : ℕ} (M : ABKModel d) {p : ℝ} (hp : 1 ≤ p) {n m : ℤ} (hnm : n < m) (l : ℤ) : (∀ (omega : Cutoff.ShellSeq d), streamIncrementLpNorm p l n m omega ≤ streamIncrementLpMassHead M p n m ^ p⁻¹ + streamIncrementLpTail M p l n m omega ^ p⁻¹) ∧ HCPolySupport.IndependentSums.IsBigOWith (↑M.P) (HCPolySupport.IndependentSums.gammaSigma 2) (fun (omega : Cutoff.ShellSeq d) => streamIncrementLpTail M p l n m omega ^ p⁻¹) (streamIncrementLpGainScale M p l n m ^ p⁻¹)

The unsquared Γ₂ precursor of the corrected e.km.kn.Lp (whose printed display is the squared norm at Γ₁; the squaring step is proved in IncrementLpSquared.lean): the 1/p-th root of the mass form,

`‖k_m - k_n‖_{L^p(cu_l)} ≤ (C(d)p)^{1/2} A^{1/2}

• O_{Γ₂}((C(d)p)^{1/2} A^{1/2} 3^{-(d/(2p))(l-m)})`,

for every p ≥ 1, every n < m and every l ∈ ℤ. At p = 4 the gain is the 3^{-(d/8)(l-m)} of e.wave.influence.bound.