PrincipalResponseMomentsCloseOrlicz

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

Binder descriptions below are an informal inventory only, NOT a source certification; certification vocabulary is reserved for frozen source-facing declarations.

Provider: the eighth moment of a shifted three-lane weak-Orlicz bound

This module is the p = 8 analogue of the p = 2 engine integral_sq_le_of_isTwoTermBigOWith_gammaSigma (PrincipalResponseBudgetMoment.lean). What it proves is the elementary probabilistic fact that a nonnegative random variable dominated by a deterministic shift plus three stretched-exponential lanes,

  0 <= X <= b + Y_1 + Y_2 + Y_3 ,   Y_i = O_{Gamma_{sigma_i}}(A_i) ,

has eighth moment inside (4 (b + sum_i c(sigma_i) A_i))^8, with c(sigma) = gammaMomentConst sigma * 8^{1/sigma} the class constant supplied by CoarseGraining's layer-cake bound integral_rpow_le_of_isBigOWith_gammaSigma at p = 8.

Why three lanes and a shift

The consumer is the second inequality of the moment display at ABK26. Its integrand is a sum of two multiscale ellipticity endpoints, each of which the coarse-graining ellipticity proposition controls by a deterministic profile plus weak-Orlicz lanes: two lanes for the upper endpoint (the deterministic-shift two-term one-sided form) and one lane, uniform in the family index, for the lower endpoint. Adding the two endpoints gives exactly one shift and three lanes.

How the witnesses are handled

The lane witnesses are not assumed nonnegative, so, exactly as at p = 2, the layer-cake moment bound is applied to the positive parts max(Y_i, 0), which carry the same one-sided upper tails because the tail threshold A t is positive for t >= 1 and A > 0. The passage from X <= b + sum_i max(Y_i,0) to the eighth moment then uses only the crude elementary inequality (u+v)^8 <= 256 (u^8 + v^8) twice, which is why the final envelope carries the harmless factor 4. No sharp Minkowski constant is attempted: every consumer's constant is a free dimensional constant.

Portability

The probability engine mentions no ABK26 model, cutoff law, cube, scale or anchor. It is therefore a candidate for relocation into CoarseGraining beside the p-th moment layer-cake bound it consumes.

Main results

• orliczEighthMomentScale, orliczEighthMomentScale_pos: the class constant at p = 8.
• integral_rpow_eight_le_of_shift_add_three_orlicz: MemLp at exponent 8 together with the eighth moment bound. The membership travels with the bound because Mathlib's Bochner integral is 0 off the integrable locus, so the bound alone constrains nothing.
• orliczSecondMomentScale, orliczSecondMomentScale_pos: the class constant at p = 2.
• integral_rpow_two_le_of_shift_add_one_orlicz: the one-lane shifted second moment. The two-lane engine PrincipalResponseBudgetMoment.integral_sq_le_of_isTwoTermBigOWith_gammaSigma cannot consume a single-lane observable carrying a deterministic shift (it has no shift and needs two admissible tails), which is the shape produced by the fresh-shell L^8 gradient bound; this supplies exactly that shape.

Elementary eighth powers

The class constant at p = 8

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.orliczEighthMomentScale (sigma : ℝ) : ℝ

The eighth-moment scale of the stretched-exponential class Gamma_sigma: a variable which is O_{Gamma_sigma}(A) has eighth moment at most (orliczEighthMomentScale sigma * A)^8. It depends on nothing but sigma.

Equations

• Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.orliczEighthMomentScale sigma = HCPolySupport.IndependentSums.gammaMomentConst sigma * 8 ^ sigma⁻¹

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.orliczEighthMomentScale_pos {sigma : ℝ} (hsigma : 0 < sigma) : 0 < orliczEighthMomentScale sigma

Positive parts

The eighth moment of a shifted three-lane weak-Orlicz bound

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.integral_rpow_eight_le_of_shift_add_three_orlicz {Omega : Type u_1} [MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} [MeasureTheory.IsProbabilityMeasure mu] {X Y1 Y2 Y3 : Omega → ℝ} {b A1 A2 A3 s1 s2 s3 : ℝ} (hs1 : 0 < s1) (hs2 : 0 < s2) (hs3 : 0 < s3) (hA1 : 0 < A1) (hA2 : 0 < A2) (hA3 : 0 < A3) (hb : 0 ≤ b) (hY1m : Measurable Y1) (hY2m : Measurable Y2) (hY3m : Measurable Y3) (hT1 : HCPolySupport.IndependentSums.IsBigOWith mu (HCPolySupport.IndependentSums.gammaSigma s1) Y1 A1) (hT2 : HCPolySupport.IndependentSums.IsBigOWith mu (HCPolySupport.IndependentSums.gammaSigma s2) Y2 A2) (hT3 : HCPolySupport.IndependentSums.IsBigOWith mu (HCPolySupport.IndependentSums.gammaSigma s3) Y3 A3) (hXm : MeasureTheory.AEStronglyMeasurable X mu) (hX0 : ∀ (omega : Omega), 0 ≤ X omega) (hdom : ∀ (omega : Omega), X omega ≤ b + Y1 omega + Y2 omega + Y3 omega) : MeasureTheory.MemLp X 8 mu ∧ ∫ (omega : Omega), X omega ^ 8 ∂mu ≤ (4 * (b + orliczEighthMomentScale s1 * A1 + orliczEighthMomentScale s2 * A2 + orliczEighthMomentScale s3 * A3)) ^ 8

The eighth-moment engine.

A nonnegative random variable dominated by a deterministic shift b plus three one-sided stretched-exponential lanes has eighth moment inside (4 (b + sum_i c(sigma_i) A_i))^8, where c = orliczEighthMomentScale.

The lane witnesses Y_1, Y_2, Y_3 need not be nonnegative: only their upper tails are used, through their positive parts.

The one-lane shifted second moment

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.orliczSecondMomentScale (sigma : ℝ) : ℝ

The second-moment scale of the stretched-exponential class Gamma_sigma.

Equations

• Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.orliczSecondMomentScale sigma = HCPolySupport.IndependentSums.gammaMomentConst sigma * 2 ^ sigma⁻¹

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.orliczSecondMomentScale_pos {sigma : ℝ} (hsigma : 0 < sigma) : 0 < orliczSecondMomentScale sigma

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.exists_measurable_quadratic_dominator {Omega : Type u_1} [MeasurableSpace Omega] {nu : MeasureTheory.Measure Omega} [MeasureTheory.IsFiniteMeasure nu] {Psi : ℝ → ℝ} {X W Y : Omega → ℝ} {B kappa b A : ℝ} (hkappa : 0 < kappa) (hXm : Measurable X) (hWnn : ∀ (omega : Omega), 0 ≤ W omega) (hXW : ∀ (omega : Omega), X omega ≤ B + kappa * W omega ^ 2) (hWY : ∀ (omega : Omega), W omega ≤ b + Y omega) (hY : HCPolySupport.IndependentSums.IsBigOWith nu Psi Y A) : ∃ (W0 : Omega → ℝ), Measurable W0 ∧ (∀ (omega : Omega), 0 ≤ W0 omega) ∧ (∀ (omega : Omega), W0 omega ≤ W omega) ∧ (∀ (omega : Omega), X omega ≤ B + kappa * W0 omega ^ 2) ∧ HCPolySupport.IndependentSums.IsBigOWith nu Psi (fun (omega : Omega) => W0 omega - b) A

A measurable observable under a quadratic envelope has a measurable, nonnegative dominating proxy below the envelope witness. The proxy inherits the shifted upper tail over a finite measure without measurability assumptions on the original envelope and tail witnesses.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.integrable_sq_of_shift_add_one_orlicz {Omega : Type u_1} [MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} [MeasureTheory.IsProbabilityMeasure mu] {X Y : Omega → ℝ} {b A sigma : ℝ} (hsigma : 0 < sigma) (hA : 0 < A) (hb : 0 ≤ b) (hXm : Measurable X) (hX0 : ∀ (omega : Omega), 0 ≤ X omega) (hdom : ∀ (omega : Omega), X omega ≤ b + Y omega) (hY : HCPolySupport.IndependentSums.IsBigOWith mu (HCPolySupport.IndependentSums.gammaSigma sigma) Y A) : MeasureTheory.Integrable (fun (omega : Omega) => X omega ^ 2) mu

A measurable nonnegative observable below a shifted Gamma-tail witness has an integrable square; the tail witness itself need not be measurable.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.integrable_of_abs_le_quadratic_orlicz_bound {Omega : Type u_1} [MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} [MeasureTheory.IsProbabilityMeasure mu] {f W Y : Omega → ℝ} {B kappa b A sigma : ℝ} (hsigma : 0 < sigma) (hA : 0 < A) (hb : 0 ≤ b) (hkappa : 0 < kappa) (hfm : Measurable f) (hWnn : ∀ (omega : Omega), 0 ≤ W omega) (hfW : ∀ (omega : Omega), |f omega| ≤ B + kappa * W omega ^ 2) (hWY : ∀ (omega : Omega), W omega ≤ b + Y omega) (hY : HCPolySupport.IndependentSums.IsBigOWith mu (HCPolySupport.IndependentSums.gammaSigma sigma) Y A) : MeasureTheory.Integrable f mu

A measurable observable with an absolute quadratic envelope is integrable when the envelope has a shifted Gamma-tail bound. The envelope and tail witnesses need not be measurable.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.integral_rpow_two_le_of_shift_add_one_orlicz {Omega : Type u_1} [MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} [MeasureTheory.IsProbabilityMeasure mu] {X Y : Omega → ℝ} {b A sigma : ℝ} (hsigma : 0 < sigma) (hA : 0 < A) (hb : 0 ≤ b) (hYm : Measurable Y) (hT : HCPolySupport.IndependentSums.IsBigOWith mu (HCPolySupport.IndependentSums.gammaSigma sigma) Y A) (hX0 : ∀ (omega : Omega), 0 ≤ X omega) (hdom : ∀ (omega : Omega), X omega ≤ b + Y omega) : ∫ (omega : Omega), X omega ^ 2 ∂mu ≤ (2 * (b + orliczSecondMomentScale sigma * A)) ^ 2

The one-lane shifted second moment.

A nonnegative random variable dominated by a deterministic shift b plus a single one-sided stretched-exponential lane has second moment inside (2 (b + c(sigma) A))^2, with c = orliczSecondMomentScale.

The lane witness Y need not be nonnegative: only its upper tail is used.