MajorantMeasurability

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

Measurability of the L-free majorant: hGmeas at its honest strength

What this module does

MajorantTransport.lean's transport carries a side condition hGmeas: the per-scale descendant average of G^{p/2} must be measurable in the sample. At the L-free majorant lFreeStep3Majorant that average has five ingredients, and they do NOT all have the same strength:

• the two shell-built slots lFreeGradSlot, lFreeValueSlot are genuinely measurable (finite layer sums, Cutoff.localCubeControl of a stream increment, plus the caller's tail gauge -- and the canonical gauge tailSeriesGauge is itself measurable, a countable sum of measurable nonnegative layer terms);
• the multiscale ellipticity gauge enters only through its inverse λ_{2γ,2}^{-1}, which is genuinely measurable: the transfer BadEvents.unitCubeLambda_unitRescaledCutoffCoeff identifies it with Section 3's literal cubeLowerEllipticityInvLiteral, whose measurability is the proved literal-measurability engine;
• the (2,2) homogenization error 𝓔_{s,2,2} is only almost everywhere measurable. As in Section 3, the literal (p,q) error functional is not measurable by composition; the route used here is Annular.unitCubeHomogenizationError22_unitRescaledCutoffCoeff_ae_eq_annularErrorObservable, the a.e. identification with the measurable 𝒢₂ observable Support.annularErrorObservable read at the translated sample.

Consequently hGmeas is dischargeable at AEMeasurable, not at Measurable. That is not a loss: the transport's own proof uses hGmeas in exactly one place, MeasureTheory.lintegral_tsum, which asks for AEMeasurable. This module proves the AEMeasurable form of the side condition at the L-free majorant (aemeasurable_finsetAverageReal_rpow_lFreeStep3Majorant); the matching weakening of the transport, and the composition with TailSummability's discharged hTae, are AeMeasurableTransport.lean.

The negated leg costs nothing: Cutoff.negateCutoffSample is measurable and preserves the cutoff-sample law (Cutoff.map_negateCutoffSample_cutoffSampleLaw), so it is quasi measure preserving and a.e. measurability composes through it.

References

• ABK26, l.bounds.mathcal.E.aL, (Step 2), (Step 3).

1. The shell-built slots are genuinely measurable

theorem Algsuperdiff.Section4.Provider.BoundsEaL.measurable_tailLayerTerm {d : ℕ} (m k : ℤ) (v : Fin d → ℤ) (i : ℤ) : Measurable fun (omega : Section3.Cutoff.CutoffSample d) => tailLayerTerm m k v omega i

Each ℤ-indexed layer term is measurable in the sample.

theorem Algsuperdiff.Section4.Provider.BoundsEaL.measurable_tailSeriesGauge {d : ℕ} (m k : ℤ) (v : Fin d → ℤ) : Measurable fun (omega : Section3.Cutoff.CutoffSample d) => tailSeriesGauge m k v omega

The canonical tail gauge is measurable.

theorem Algsuperdiff.Section4.Provider.BoundsEaL.measurable_headLayerSum {d : ℕ} (m k : ℤ) (v : Fin d → ℤ) : Measurable fun (omega : Section3.Cutoff.CutoffSample d) => headLayerSum m k v omega

The L-free head block is measurable.

theorem Algsuperdiff.Section4.Provider.BoundsEaL.measurable_lFreeGradSlot {d : ℕ} (m : ℤ) (T : ℤ → (Fin d → ℤ) → Section3.Cutoff.CutoffSample d → ℝ) (hT : ∀ (k : ℤ) (v : Fin d → ℤ), Measurable (T k v)) (R : HCPolySupport.TriadicCube d) : Measurable fun (omega : Section3.Cutoff.CutoffSample d) => lFreeGradSlot m T R omega

The L-free gradient slot is measurable whenever the tail gauge is.

theorem Algsuperdiff.Section4.Provider.BoundsEaL.measurable_lFreeValueSlot {d : ℕ} (m : ℤ) (T : ℤ → (Fin d → ℤ) → Section3.Cutoff.CutoffSample d → ℝ) (hT : ∀ (k : ℤ) (v : Fin d → ℤ), Measurable (T k v)) (R : HCPolySupport.TriadicCube d) : Measurable fun (omega : Section3.Cutoff.CutoffSample d) => lFreeValueSlot m T R omega

The L-free value slot is measurable whenever the tail gauge is.

2. The two unit-cube gauges

def Algsuperdiff.Section4.Provider.BoundsEaL.exponentTwoAdm : Section3.CoarseEllipticityExponent

The admissible finite exponent q = 2 of Section 3's ellipticity carrier, spelled so that its underlying multiscale exponent is literally .finite 2.

Equations

• Algsuperdiff.Section4.Provider.BoundsEaL.exponentTwoAdm = Algsuperdiff.Section3.CoarseEllipticityExponent.finite ⟨2, Algsuperdiff.Section4.Provider.BoundsEaL.exponentTwoAdm._proof_1⟩

theorem Algsuperdiff.Section4.Provider.BoundsEaL.measurable_unitCubeLambda_inv_unitRescaledCutoffCoeff {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (R : HCPolySupport.TriadicCube d) {t : ℝ} (ht : 0 < t) : Measurable fun (omega : Section3.Cutoff.CutoffSample d) => (Frozen.Section24.unitCubeLambda t (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) (Section3.Provider.BadEvents.unitRescaledCutoffCoeff M R (R.scale - 2) omega))⁻¹

The multiscale ellipticity gauge enters only through its inverse, and the inverse is genuinely measurable.

BadEvents.unitCubeLambda_unitRescaledCutoffCoeff identifies λ_{t,2}(unitRescaledCutoffCoeff M R (R.scale−2) ω) with Section 3's Ch02.lambdaSq at the cube R, i.e. with the inverse of the literal cubeLowerEllipticityInvLiteral; the latter is measurable by the proved literal-measurability engine.

theorem Algsuperdiff.Section4.Provider.BoundsEaL.aemeasurable_unitCubeHomogenizationError22_unitRescaledCutoffCoeff {d : ℕ} (M : Section3.ABKModel d) (R : HCPolySupport.TriadicCube d) (s : { s : ℝ // 0 < s }) : AEMeasurable (fun (omega : Section3.Cutoff.CutoffSample d) => Frozen.Section24.unitCubeHomogenizationError (↑s) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) (Section3.Provider.BadEvents.unitRescaledCutoffCoeff M R (R.scale - 2) omega) (Section3.Observable.isotropicComparatorMatrix (Section3.Annealed.sigmaBar M (R.scale - 2)))) ↑(Section3.Cutoff.cutoffSampleLaw M)

The (2,2) homogenization error gauge is almost everywhere measurable.

This is the exact strength available -- as in Section 3, no everywhere-measurable realization of the literal (p,q) error exists by composition.

3. The display, and the majorant

theorem Algsuperdiff.Section4.Provider.BoundsEaL.aemeasurable_step3DisplayAt {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (C : ℝ) (m : ℤ) (s : { s : ℝ // 0 < s }) (hgam : M.gamma ≤ 1 / 8) (GB VB : HCPolySupport.TriadicCube d → Section3.Cutoff.CutoffSample d → ℝ) (R : HCPolySupport.TriadicCube d) (hGB : Measurable fun (omega : Section3.Cutoff.CutoffSample d) => GB R omega) (hVB : Measurable fun (omega : Section3.Cutoff.CutoffSample d) => VB R omega) : AEMeasurable (fun (omega : Section3.Cutoff.CutoffSample d) => step3DisplayAt C M m R omega (↑s) (GB R omega) (VB R omega)) ↑(Section3.Cutoff.cutoffSampleLaw M)

Step 3's display at the two L-free slots is a.e. measurable.

theorem Algsuperdiff.Section4.Provider.BoundsEaL.quasiMeasurePreserving_negateCutoffSample {d : ℕ} (M : Section3.ABKModel d) : MeasureTheory.QuasiMeasurePreserving Section3.Cutoff.negateCutoffSample ↑(Section3.Cutoff.cutoffSampleLaw M) ↑(Section3.Cutoff.cutoffSampleLaw M)

Whole-sequence negation is quasi measure preserving for the cutoff-sample law: it is measurable and preserves the law exactly.

theorem Algsuperdiff.Section4.Provider.BoundsEaL.aemeasurable_lFreeStep3Majorant {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (C : ℝ) (m : ℤ) (s : { s : ℝ // 0 < s }) (hgam : M.gamma ≤ 1 / 8) (T : ℤ → (Fin d → ℤ) → Section3.Cutoff.CutoffSample d → ℝ) (hT : ∀ (k : ℤ) (v : Fin d → ℤ), Measurable (T k v)) (R : HCPolySupport.TriadicCube d) : AEMeasurable (fun (omega : Section3.Cutoff.CutoffSample d) => lFreeStep3Majorant C M m (↑s) (lFreeGradSlot m T) (lFreeValueSlot m T) R omega) ↑(Section3.Cutoff.cutoffSampleLaw M)

The L-free majorant is a.e. measurable. Its two legs are the display at the sample and the display at the negated sample; the second composes through the law-preserving negation.