UpperFiniteQLtTwo

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

Finite upper coarse ellipticity below exponent two

This module keeps the finite upper observable in its defining weighted ell^(q / 2) aggregate when 1 <= q < 2. At that exponent the inner power is concave, while the outer power is convex. Each random depth remainder is therefore normalized by its own deterministic amplitude before countable weak-Orlicz summation. In particular, no comparison between a finite carrier and the q = infinity carrier is used.

The final theorem accepts an almost-everywhere per-depth split of the actual Chapter 4 descendant maximum into a deterministic profile and two normalized random lanes. It returns the everywhere-defined three-term witness consumed by UpperLeg.lean; the null-set defect is absorbed inside the ordinary lane.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.perDescendantSplit_choice_properties {d : ℕ} {Omega : Type u_1} [MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} {m : ℤ} {block : HCPolySupport.TriadicCube d → Omega → ℝ} {deterministicBound sigma : ℝ} {ordinaryAmplitude rareAmplitude : ℕ → ℝ} (hblockNonneg : ∀ (k : ℕ), ∀ R ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d m) (m - 1 - ↑k), ∀ (omega : Omega), 0 ≤ block R omega) (hper : ∀ (k : ℕ), ∀ R ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d m) (m - 1 - ↑k), ∃ (Uone : Omega → ℝ) (Uexp : Omega → ℝ), (∀ (omega : Omega), 0 ≤ Uone omega) ∧ Measurable Uone ∧ (∀ (omega : Omega), 0 ≤ Uexp omega) ∧ Measurable Uexp ∧ (∀ (omega : Omega), block R omega ≤ deterministicBound + Uone omega + Uexp omega) ∧ HCPolySupport.IndependentSums.IsBigOWith mu (HCPolySupport.IndependentSums.gammaSigma 1) Uone (ordinaryAmplitude k) ∧ HCPolySupport.IndependentSums.IsBigOWith mu (HCPolySupport.IndependentSums.gammaSigma sigma) Uexp (rareAmplitude k)) : have UoneCube := fun (k : ℕ) (R : HCPolySupport.TriadicCube d) => if hR : R ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d m) (m - 1 - ↑k) then Classical.choose ⋯ else fun (x : Omega) => 0; have UexpCube := fun (k : ℕ) (R : HCPolySupport.TriadicCube d) => if hR : R ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d m) (m - 1 - ↑k) then Classical.choose ⋯ else fun (x : Omega) => 0; (∀ (k : ℕ) (R : HCPolySupport.TriadicCube d) (omega : Omega), 0 ≤ UoneCube k R omega) ∧ (∀ (k : ℕ) (R : HCPolySupport.TriadicCube d) (omega : Omega), 0 ≤ UexpCube k R omega) ∧ (∀ (k : ℕ) (R : HCPolySupport.TriadicCube d), Measurable (UoneCube k R)) ∧ (∀ (k : ℕ) (R : HCPolySupport.TriadicCube d), Measurable (UexpCube k R)) ∧ (∀ (k : ℕ), ∀ R ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d m) (m - 1 - ↑k), HCPolySupport.IndependentSums.IsBigOWith mu (HCPolySupport.IndependentSums.gammaSigma 1) (UoneCube k R) (ordinaryAmplitude k)) ∧ (∀ (k : ℕ), ∀ R ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d m) (m - 1 - ↑k), HCPolySupport.IndependentSums.IsBigOWith mu (HCPolySupport.IndependentSums.gammaSigma sigma) (UexpCube k R) (rareAmplitude k)) ∧ ∀ (k : ℕ), ∀ R ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d m) (m - 1 - ↑k), ∀ (omega : Omega), |block R omega| ≤ deterministicBound + UoneCube k R omega + UexpCube k R omega

Canonical per-descendant choices preserve nonnegativity, measurability, both Orlicz estimates and domination, with zero values outside the descendant row.

The exact finite upper carrier

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.LambdaSqCoeffField_finite_eq_rpow {d : ℕ} (Q : HCPolySupport.TriadicCube d) (a : HCPolySupport.RegCoeffField d) (s : ℝ) {q : ℝ} (hq : 0 < q) : HCPolySupport.Book.Ch04.LambdaSqCoeffField Q s (HCPolySupport.Book.Ch02.MultiscaleExponent.finite q) a = (∑' (n : ℕ), HCPolySupport.Book.Ch02.geometricWeight s q n * HCPolySupport.Book.Ch04.maxDescendantBMatrixNormCoeffFieldAtScale Q (Q.scale - ↑n) a ^ (q / 2)) ^ (2 / q)

The Chapter 4 finite upper ellipticity is its defining weighted ell^(q / 2) aggregate, including the totalized non-elliptic branch.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.cutoffUpperEllipticity_mul_eq_rpow {d : ℕ} (M : ABKModel d) (m L : ℤ) {s r : ℝ} (hs : 0 < s) {q : CoarseEllipticityExponent} (hqval : ↑q = HCPolySupport.Book.Ch02.MultiscaleExponent.finite r) (hr : 0 < r) {scaling : ℝ} (hscaling : 0 ≤ scaling) (omega : Cutoff.CutoffSample d) : Observable.cutoffUpperEllipticity M m L s hs q omega * scaling = (∑' (n : ℕ), HCPolySupport.Book.Ch02.geometricWeight s r n * (scaling * HCPolySupport.Book.Ch04.maxDescendantBMatrixNormCoeffFieldAtScale (HCPolySupport.originCube d m) (m - ↑n) (Cutoff.coefficientCutoff M.nu L omega)) ^ (r / 2)) ^ (2 / r)

Multiplication of the exported finite upper observable by a nonnegative scalar can be moved inside every depth before taking the outer root.

A normalized random lane

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.exists_normalized_finite_q_lt_two_lane {Omega : Type u_1} [MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} [MeasureTheory.IsFiniteMeasure mu] {r sigma K B : ℝ} {w a : ℕ → ℝ} {V : ℕ → Omega → ℝ} (hr1 : 1 ≤ r) (hr2 : r ≤ 2) (hsigma : 0 < sigma) (hw : ∀ (n : ℕ), 0 < w n) (ha : ∀ (n : ℕ), 0 < a n) (hVnonneg : ∀ (n : ℕ) (omega : Omega), 0 ≤ V n omega) (hVmeas : ∀ (n : ℕ), Measurable (V n)) (hasum : Summable fun (n : ℕ) => w n * a n ^ (r / 2)) (hVlinsum : ∀ (omega : Omega), Summable fun (n : ℕ) => w n * a n ^ (r / 2) * V n omega) (hVO : ∀ (n : ℕ), HCPolySupport.IndependentSums.IsBigOWith mu (HCPolySupport.IndependentSums.gammaSigma sigma) (V n) 1) (hK : 0 ≤ K) (hbudget : K * (∑' (n : ℕ), w n * a n ^ (r / 2)) ^ (2 / r) * HCPolySupport.IndependentSums.gammaTriangleConst sigma ≤ B) : ∃ (Y : Omega → ℝ), (∀ (omega : Omega), Summable fun (n : ℕ) => w n * (a n * V n omega) ^ (r / 2)) ∧ Measurable Y ∧ HCPolySupport.IndependentSums.IsBigOWith mu (HCPolySupport.IndependentSums.gammaSigma sigma) Y B ∧ ∀ (omega : Omega), K * (∑' (n : ℕ), w n * (a n * V n omega) ^ (r / 2)) ^ (2 / r) ≤ Y omega

A normalized family of nonnegative depth remainders produces one measurable weak-Orlicz lane. The returned summability clause is the exact input needed to combine several such lanes before taking the outer root.

The actual upper observable

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.threeTermSplit_cutoffUpperEllipticity_of_finiteQLtTwoPresplit {d : ℕ} (M : ABKModel d) (m L : ℤ) (r : { r : ℝ // 1 ≤ r }) (hr : ↑r < 2) {s scaling Bdet B1 Bexp sigma1 sigmaExp : ℝ} (hs : 0 < s) (hscaling : 0 ≤ scaling) (hsigma1 : 0 < sigma1) (hsigmaExp : 0 < sigmaExp) {D a1 aexp : ℕ → ℝ} {Vone Vexp : ℕ → Cutoff.CutoffSample d → ℝ} (hD : ∀ (n : ℕ), 0 ≤ D n) (ha1 : ∀ (n : ℕ), 0 < a1 n) (haexp : ∀ (n : ℕ), 0 < aexp n) (hVoneNonneg : ∀ (n : ℕ) (omega : Cutoff.CutoffSample d), 0 ≤ Vone n omega) (hVexpNonneg : ∀ (n : ℕ) (omega : Cutoff.CutoffSample d), 0 ≤ Vexp n omega) (hVoneMeas : ∀ (n : ℕ), Measurable (Vone n)) (hVexpMeas : ∀ (n : ℕ), Measurable (Vexp n)) (hDsum : Summable fun (n : ℕ) => HCPolySupport.Book.Ch02.geometricWeight s (↑r) n * D n ^ (↑r / 2)) (ha1sum : Summable fun (n : ℕ) => HCPolySupport.Book.Ch02.geometricWeight s (↑r) n * a1 n ^ (↑r / 2)) (haexpsum : Summable fun (n : ℕ) => HCPolySupport.Book.Ch02.geometricWeight s (↑r) n * aexp n ^ (↑r / 2)) (hVoneLinSum : ∀ (omega : Cutoff.CutoffSample d), Summable fun (n : ℕ) => HCPolySupport.Book.Ch02.geometricWeight s (↑r) n * a1 n ^ (↑r / 2) * Vone n omega) (hVexpLinSum : ∀ (omega : Cutoff.CutoffSample d), Summable fun (n : ℕ) => HCPolySupport.Book.Ch02.geometricWeight s (↑r) n * aexp n ^ (↑r / 2) * Vexp n omega) (hVoneO : ∀ (n : ℕ), HCPolySupport.IndependentSums.IsBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma sigma1) (Vone n) 1) (hVexpO : ∀ (n : ℕ), HCPolySupport.IndependentSums.IsBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma sigmaExp) (Vexp n) 1) (hdetBudget : 4 * (∑' (n : ℕ), HCPolySupport.Book.Ch02.geometricWeight s (↑r) n * D n ^ (↑r / 2)) ^ (2 / ↑r) ≤ Bdet) (honeBudget : 4 * (∑' (n : ℕ), HCPolySupport.Book.Ch02.geometricWeight s (↑r) n * a1 n ^ (↑r / 2)) ^ (2 / ↑r) * HCPolySupport.IndependentSums.gammaTriangleConst sigma1 ≤ B1) (hexpBudget : 4 * (∑' (n : ℕ), HCPolySupport.Book.Ch02.geometricWeight s (↑r) n * aexp n ^ (↑r / 2)) ^ (2 / ↑r) * HCPolySupport.IndependentSums.gammaTriangleConst sigmaExp ≤ Bexp) (hdepth : ∀ (n : ℕ), ∀ᵐ (omega : Cutoff.CutoffSample d) ∂↑(Cutoff.cutoffSampleLaw M), scaling * HCPolySupport.Book.Ch04.maxDescendantBMatrixNormCoeffFieldAtScale (HCPolySupport.originCube d m) (m - ↑n) (Cutoff.coefficientCutoff M.nu L omega) ≤ D n + a1 n * Vone n omega + aexp n * Vexp n omega) : ∃ (Udet : Cutoff.CutoffSample d → ℝ) (Uone : Cutoff.CutoffSample d → ℝ) (Utail : Cutoff.CutoffSample d → ℝ), (∀ (omega : Cutoff.CutoffSample d), Observable.cutoffUpperEllipticity M m L s hs (CoarseEllipticityExponent.finite r) omega * scaling ≤ Udet omega + Uone omega + Utail omega) ∧ (∀ (omega : Cutoff.CutoffSample d), Udet omega ≤ Bdet) ∧ Measurable Uone ∧ Measurable Utail ∧ HCPolySupport.IndependentSums.IsBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma sigma1) Uone B1 ∧ HCPolySupport.IndependentSums.IsBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma sigmaExp) Utail Bexp

An almost-everywhere normalized per-depth split of the actual finite upper carrier yields the everywhere three-term witness required by the upper leg. The factor four is the uniform convexity loss for the three outer-root slots when 1 <= q < 2.