IncrementMassRepresentative

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

A measurable local representative of the cube L^p mass

Provider/Stream/IncrementConcentration.lean reduced the concentration step of e.kl.bounds.large (ABK26) to a single missing input: the measurability of the cube observable regFieldLpMass p U for the canonical carrier σ-algebra of RegCoeffField d.

• is measurable and local by construction (a limsup over triadic scales of a countable sum of scalar multiples of the linear entry-test generators entryTestR i j (1_{cubeSet R})), and
• agrees with regFieldLpMass at every continuous field, which is all the application needs: the stream increments k_m - k_n are continuous (continuous_finiteShellIncrement_entry), so the identification is a pointwise identity on the image of the increment law and no a.e. bookkeeping is needed.

The shape of the representative

regFieldLpMassRep p U a is the limsup over k : ℕ of the scale-(-k) grid mass

(vol U)⁻¹ * ∑_{R : scale(R) = -k, cubeSet R ⊆ U} vol(cubeSet R) · |⨍_R a|^p,

where ⨍_R a = avgMat (cubeSet R) a is CoarseGraining's matrix of entry averages. The grid at a nonpositive scale is invariant under integer translations, which is exactly what makes the resulting set-indexed observable translation covariant in CoarseGraining's restriction-lane sense (Ch04.IsRestrictionTranslationCovariant) for every observation set U — the cube family itself is not, since the integer translate of a triadic cube of positive scale is not a triadic cube.

What is proved

• gridMass_cubeSet_toReal_eq_descendantsAverage — on a triadic cube the grid mass is CoarseGraining's descendantsAverage of the cube-average norms.
• measurable_regFieldLpMassRep, isLocalRandomVariable_regFieldLpMassRep — the two restriction-lane measurability hypotheses of the centered descendant average estimate.
• isTranslationCovariantR_regFieldLpMassRep — its hX_cov hypothesis.
• regFieldLpMassRep_cubeSet_eq_regFieldLpMass_of_continuous — the identification: on continuous fields the representative is the genuine volume-normalized L^p mass. This is the Riemann-sum convergence of the triadic cube averages of a continuous field.
• regFieldLpMassRep_cubeSet_smulReg_finiteShellIncrement — its reading at a rescaled stream increment, the form the concentration step consumes.

References

• ABK26, e.kl.bounds.large; p.concentration.
• Provider/Stream/IncrementConcentration.lean, "The remaining gap for e.kl.bounds.large", which specifies exactly this representative.
• CoarseGraining Homogenization/Probability/RegCoeffField/Sigma.lean (the carrier σ-algebra and its entry-test generators), Homogenization/Probability/RegCoeffField/Differentiation.lean (avgMat).

Elementary triadic-cube geometry

theorem Algsuperdiff.Section3.Provider.Stream.cubeCenter_mem_cubeSet {d : ℕ} (Q : HCPolySupport.TriadicCube d) : HCPolySupport.cubeCenter Q ∈ HCPolySupport.cubeSet Q

The centre of a triadic cube belongs to its half-open realization.

theorem Algsuperdiff.Section3.Provider.Stream.cubeSet_nonempty {d : ℕ} (Q : HCPolySupport.TriadicCube d) : (HCPolySupport.cubeSet Q).Nonempty

Every triadic cube is nonempty.

theorem Algsuperdiff.Section3.Provider.Stream.dist_lt_cubeScaleFactor_of_mem_cubeSet {d : ℕ} {Q : HCPolySupport.TriadicCube d} {x y : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.cubeSet Q) (hy : y ∈ HCPolySupport.cubeSet Q) : dist x y < HCPolySupport.cubeScaleFactor Q

Two points of a triadic cube are at distance strictly less than its side length.

theorem Algsuperdiff.Section3.Provider.Stream.mem_descendantsAtDepth_of_scale_eq_of_cubeSet_subset {d : ℕ} {Q R : HCPolySupport.TriadicCube d} {j : ℕ} (hscale : R.scale = Q.scale - ↑j) (hsub : HCPolySupport.cubeSet R ⊆ HCPolySupport.cubeSet Q) : R ∈ HCPolySupport.descendantsAtDepth Q j

A same-scale subcube is a descendant. A triadic cube of scale Q.scale - j contained in Q is one of the depth-j descendants of Q: it meets the (unique) descendant containing any of its points, and distinct cubes of the same scale are disjoint.

The triadic grid at nonpositive scales

def Algsuperdiff.Section3.Provider.Stream.gridCubesIn {d : ℕ} (U : Set (HCPolySupport.Vec d)) (k : ℕ) : Set (HCPolySupport.TriadicCube d)

The scale-(-k) triadic cubes contained in the observation set U. For k : ℕ this family is invariant under integer translations of U, which is what makes the grid mass below translation covariant on every set.

Equations

• Algsuperdiff.Section3.Provider.Stream.gridCubesIn U k = {R : HCPolySupport.TriadicCube d | R.scale = -↑k ∧ HCPolySupport.cubeSet R ⊆ U}

theorem Algsuperdiff.Section3.Provider.Stream.gridCubesIn_cubeSet_eq_descendantsAtDepth {d : ℕ} (Q : HCPolySupport.TriadicCube d) {k : ℕ} (hk : -↑k ≤ Q.scale) : gridCubesIn (HCPolySupport.cubeSet Q) k = ↑(HCPolySupport.descendantsAtDepth Q (Q.scale + ↑k).toNat)

On a triadic cube the grid family is exactly the corresponding family of descendants.

Probes and averages on a triadic cube

theorem Algsuperdiff.Section3.Provider.Stream.isProbeR_indicator_cubeSet {d : ℕ} (R : HCPolySupport.TriadicCube d) : HCPolySupport.IsProbeR ((HCPolySupport.cubeSet R).indicator fun (x : HCPolySupport.Vec d) => 1)

The constant-one indicator of a triadic cube is an enriched CoarseGraining probe: it is bounded and measurable, and its support has compact closure because the cube is contained in a closed ball.

theorem Algsuperdiff.Section3.Provider.Stream.measurable_avgMat_cubeSet_localSigmaR {d : ℕ} {U : Set (HCPolySupport.Vec d)} (R : HCPolySupport.TriadicCube d) (hRU : HCPolySupport.cubeSet R ⊆ U) : Measurable (HCPolySupport.avgMat (HCPolySupport.cubeSet R))

The cube average matrix is a local carrier observable. Each entry of avgMat (cubeSet R) is a scalar multiple of the localized entry-test generator against the cube indicator, hence LocalSigmaR U-measurable as soon as the cube lies in U.

The grid mass

noncomputable def Algsuperdiff.Section3.Provider.Stream.gridMassTerm {d : ℕ} (p : ℝ) (U : Set (HCPolySupport.Vec d)) (k : ℕ) (R : HCPolySupport.TriadicCube d) (a : HCPolySupport.RegCoeffField d) : ENNReal

One term of the scale-(-k) grid mass of a on U.

Equations

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

theorem Algsuperdiff.Section3.Provider.Stream.gridMassTerm_of_mem {d : ℕ} {p : ℝ} {U : Set (HCPolySupport.Vec d)} {k : ℕ} {R : HCPolySupport.TriadicCube d} (hR : R ∈ gridCubesIn U k) (a : HCPolySupport.RegCoeffField d) : gridMassTerm p U k R a = MeasureTheory.volume (HCPolySupport.cubeSet R) * ENNReal.ofReal (HCPolySupport.Book.Ch02.matrixOperatorNorm (HCPolySupport.avgMat (HCPolySupport.cubeSet R) a) ^ p)

theorem Algsuperdiff.Section3.Provider.Stream.gridMassTerm_of_notMem {d : ℕ} {p : ℝ} {U : Set (HCPolySupport.Vec d)} {k : ℕ} {R : HCPolySupport.TriadicCube d} (hR : R ∉ gridCubesIn U k) (a : HCPolySupport.RegCoeffField d) : gridMassTerm p U k R a = 0

noncomputable def Algsuperdiff.Section3.Provider.Stream.gridMass {d : ℕ} (p : ℝ) (U : Set (HCPolySupport.Vec d)) (k : ℕ) (a : HCPolySupport.RegCoeffField d) : ENNReal

The scale-(-k) grid mass of a on U: the countable sum, over the scale-(-k) triadic cubes contained in U, of the cube volume times the p-th power of the operator norm of the cube average.

Equations

• Algsuperdiff.Section3.Provider.Stream.gridMass p U k a = ∑' (R : HCPolySupport.TriadicCube d), Algsuperdiff.Section3.Provider.Stream.gridMassTerm p U k R a

noncomputable def Algsuperdiff.Section3.Provider.Stream.regFieldLpMassRep {d : ℕ} (p : ℝ) (U : Set (HCPolySupport.Vec d)) (a : HCPolySupport.RegCoeffField d) : ℝ

The countably generated representative of the cube L^p mass.

Equations

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

Measurability and locality of the representative

theorem Algsuperdiff.Section3.Provider.Stream.measurable_gridMassTerm_localSigmaR {d : ℕ} (p : ℝ) (U : Set (HCPolySupport.Vec d)) (k : ℕ) (R : HCPolySupport.TriadicCube d) : Measurable (gridMassTerm p U k R)

theorem Algsuperdiff.Section3.Provider.Stream.measurable_gridMass_localSigmaR {d : ℕ} (p : ℝ) (U : Set (HCPolySupport.Vec d)) (k : ℕ) : Measurable (gridMass p U k)

theorem Algsuperdiff.Section3.Provider.Stream.measurable_regFieldLpMassRep_localSigmaR {d : ℕ} (p : ℝ) (U : Set (HCPolySupport.Vec d)) : Measurable (regFieldLpMassRep p U)

The representative is a local carrier observable. It is generated by countably many entry tests against probes supported in U.

theorem Algsuperdiff.Section3.Provider.Stream.measurable_regFieldLpMassRep {d : ℕ} (p : ℝ) (U : Set (HCPolySupport.Vec d)) : Measurable (regFieldLpMassRep p U)

The representative is measurable for the canonical carrier σ-algebra. This is the hX0_meas/hX_desc_meas hypothesis of the restriction-lane centered descendant average estimate.

theorem Algsuperdiff.Section3.Provider.Stream.isLocalRandomVariable_regFieldLpMassRep {d : ℕ} (p : ℝ) {U : Set (HCPolySupport.Vec d)} (hU : MeasurableSet U) : HCPolySupport.Book.Ch04.IsRestrictionLocalRandomVariable U hU (regFieldLpMassRep p U)

CoarseGraining locality of the representative. This is the hX_local hypothesis of isBigO_gammaSigma_restrictionCenteredDescendantAverage_of_restrictionUnitRangeDependentLaw.

Translation covariance of the representative

def Algsuperdiff.Section3.Provider.Stream.translateCubeEquiv {d : ℕ} (s : Fin d → ℤ) : HCPolySupport.TriadicCube d ≃ HCPolySupport.TriadicCube d

Index translation of triadic cubes is a bijection of the cube type.

Equations

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

@[simp]

theorem Algsuperdiff.Section3.Provider.Stream.translateCubeEquiv_apply {d : ℕ} (s : Fin d → ℤ) (R : HCPolySupport.TriadicCube d) : (translateCubeEquiv s) R = HCPolySupport.translateCube s R

@[simp]

theorem Algsuperdiff.Section3.Provider.Stream.scale_translateCube {d : ℕ} (s : Fin d → ℤ) (R : HCPolySupport.TriadicCube d) : (HCPolySupport.translateCube s R).scale = R.scale

theorem Algsuperdiff.Section3.Provider.Stream.cubeSet_translateCube_descendantTranslationShift {d : ℕ} (z : Fin d → ℤ) (k : ℕ) {R : HCPolySupport.TriadicCube d} (hR : R.scale = -↑k) : HCPolySupport.cubeSet (HCPolySupport.translateCube (HCPolySupport.descendantTranslationShift k z) R) = HCPolySupport.translateSet (HCPolySupport.intVecToRealVec z) (HCPolySupport.cubeSet R)

The nonpositive triadic grid is integer-translation invariant. At scale -k the index shift 3^k z implements exactly the spatial translation by the integer vector z.

theorem Algsuperdiff.Section3.Provider.Stream.translateSet_subset_translateSet_iff {d : ℕ} (w : HCPolySupport.Vec d) (A B : Set (HCPolySupport.Vec d)) : HCPolySupport.translateSet w A ⊆ HCPolySupport.translateSet w B ↔ A ⊆ B

Translation transports set inclusion both ways.

theorem Algsuperdiff.Section3.Provider.Stream.avgMat_translateSet {d : ℕ} (w : HCPolySupport.Vec d) (B : Set (HCPolySupport.Vec d)) (a : HCPolySupport.RegCoeffField d) : HCPolySupport.avgMat (HCPolySupport.translateSet w B) a = HCPolySupport.avgMat B (HCPolySupport.translateReg w a)

The cube-average matrix is translation covariant. Translating the observation set is the same as translating the field.

theorem Algsuperdiff.Section3.Provider.Stream.gridCubesIn_translateSet {d : ℕ} (U : Set (HCPolySupport.Vec d)) (k : ℕ) (z : Fin d → ℤ) {R : HCPolySupport.TriadicCube d} : (translateCubeEquiv (HCPolySupport.descendantTranslationShift k z)) R ∈ gridCubesIn (HCPolySupport.translateSet (HCPolySupport.intVecToRealVec z) U) k ↔ R ∈ gridCubesIn U k

The grid family transports along an integer translation.

theorem Algsuperdiff.Section3.Provider.Stream.gridMassTerm_translateSet {d : ℕ} (p : ℝ) (U : Set (HCPolySupport.Vec d)) (k : ℕ) (z : Fin d → ℤ) (R : HCPolySupport.TriadicCube d) (a : HCPolySupport.RegCoeffField d) : gridMassTerm p (HCPolySupport.translateSet (HCPolySupport.intVecToRealVec z) U) k ((translateCubeEquiv (HCPolySupport.descendantTranslationShift k z)) R) a = gridMassTerm p U k R (HCPolySupport.translateReg (HCPolySupport.intVecToRealVec z) a)

theorem Algsuperdiff.Section3.Provider.Stream.gridMass_translateSet {d : ℕ} (p : ℝ) (U : Set (HCPolySupport.Vec d)) (k : ℕ) (z : Fin d → ℤ) (a : HCPolySupport.RegCoeffField d) : gridMass p (HCPolySupport.translateSet (HCPolySupport.intVecToRealVec z) U) k a = gridMass p U k (HCPolySupport.translateReg (HCPolySupport.intVecToRealVec z) a)

theorem Algsuperdiff.Section3.Provider.Stream.isTranslationCovariantR_regFieldLpMassRep {d : ℕ} (p : ℝ) : HCPolySupport.Book.Ch04.IsRestrictionTranslationCovariant (regFieldLpMassRep p)

CoarseGraining's exact translation-covariance predicate for the representative. This is the hX_cov hypothesis of the restriction-lane centered descendant average estimate. It holds for every observation set because the grid used by the representative sits at nonpositive scales, where integer translations act by index shifts.

The grid mass on a triadic cube

theorem Algsuperdiff.Section3.Provider.Stream.volume_cubeSet_ne_top {d : ℕ} (R : HCPolySupport.TriadicCube d) : MeasureTheory.volume (HCPolySupport.cubeSet R) ≠ ⊤

theorem Algsuperdiff.Section3.Provider.Stream.gridMass_cubeSet {d : ℕ} (p : ℝ) (Q : HCPolySupport.TriadicCube d) {k : ℕ} (hk : -↑k ≤ Q.scale) (a : HCPolySupport.RegCoeffField d) : gridMass p (HCPolySupport.cubeSet Q) k a = ∑ R ∈ HCPolySupport.descendantsAtDepth Q (Q.scale + ↑k).toNat, MeasureTheory.volume (HCPolySupport.cubeSet R) * ENNReal.ofReal (HCPolySupport.Book.Ch02.matrixOperatorNorm (HCPolySupport.avgMat (HCPolySupport.cubeSet R) a) ^ p)

On a triadic cube of scale at least -k the grid mass is the finite sum over the scale-(-k) descendants.

theorem Algsuperdiff.Section3.Provider.Stream.gridMass_cubeSet_toReal_eq_descendantsAverage {d : ℕ} (p : ℝ) (Q : HCPolySupport.TriadicCube d) {k : ℕ} (hk : -↑k ≤ Q.scale) (a : HCPolySupport.RegCoeffField d) : (MeasureTheory.volume (HCPolySupport.cubeSet Q)).toReal⁻¹ * (gridMass p (HCPolySupport.cubeSet Q) k a).toReal = HCPolySupport.descendantsAverage Q (Q.scale + ↑k).toNat fun (R : HCPolySupport.TriadicCube d) => HCPolySupport.Book.Ch02.matrixOperatorNorm (HCPolySupport.avgMat (HCPolySupport.cubeSet R) a) ^ p

The grid mass on a triadic cube is CoarseGraining's descendant average of the cube-average norms.

Averaging estimates

theorem Algsuperdiff.Section3.Provider.Stream.abs_cubeAverage_sub_le {d : ℕ} (R : HCPolySupport.TriadicCube d) {g : HCPolySupport.Vec d → ℝ} {c eps : ℝ} (hg : MeasureTheory.IntegrableOn g (HCPolySupport.cubeSet R) MeasureTheory.volume) (hb : ∀ x ∈ HCPolySupport.cubeSet R, |g x - c| ≤ eps) : |HCPolySupport.cubeAverage R g - c| ≤ eps

The cube average of a scalar function stays within a uniform bound of any value it is uniformly close to on the cube.

theorem Algsuperdiff.Section3.Provider.Stream.avgMat_cubeSet_entry_eq_cubeAverage {d : ℕ} (R : HCPolySupport.TriadicCube d) (a : HCPolySupport.RegCoeffField d) (i j : Fin d) : HCPolySupport.avgMat (HCPolySupport.cubeSet R) a i j = HCPolySupport.cubeAverage R fun (x : HCPolySupport.Vec d) => a.toFun x i j

Each entry of the cube-average matrix is the corresponding scalar cube average.

theorem Algsuperdiff.Section3.Provider.Stream.integrableOn_cubeSet_entry {d : ℕ} (R : HCPolySupport.TriadicCube d) (a : HCPolySupport.RegCoeffField d) (i j : Fin d) : MeasureTheory.IntegrableOn (fun (x : HCPolySupport.Vec d) => a.toFun x i j) (HCPolySupport.cubeSet R) MeasureTheory.volume

The entries of a carrier field are integrable on every triadic cube.

theorem Algsuperdiff.Section3.Provider.Stream.abs_descendantsAverage_sub_le {d : ℕ} {Q : HCPolySupport.TriadicCube d} {j : ℕ} {G H : HCPolySupport.TriadicCube d → ℝ} {eps : ℝ} (hGH : ∀ R ∈ HCPolySupport.descendantsAtDepth Q j, |G R - H R| ≤ eps) : |HCPolySupport.descendantsAverage Q j G - HCPolySupport.descendantsAverage Q j H| ≤ eps

A descendant average is within eps of another one when all its terms are.

The identification at continuous fields

theorem Algsuperdiff.Section3.Provider.Stream.regFieldLpMassRep_cubeSet_eq_regFieldLpMass_of_continuous {d : ℕ} {p : ℝ} (hp : 0 < p) (Q : HCPolySupport.TriadicCube d) {a : HCPolySupport.RegCoeffField d} (hcont : ∀ (i j : Fin d), Continuous fun (x : HCPolySupport.Vec d) => a.toFun x i j) : regFieldLpMassRep p (HCPolySupport.cubeSet Q) a = regFieldLpMass p (HCPolySupport.cubeSet Q) a

The representative computes the genuine cube L^p mass at every continuous field. This is the Riemann-sum convergence of the triadic cube averages: on the compact closure of the cube the field is uniformly continuous, so each depth-j cube average is uniformly close to the field on that cube, and the descendant average of the p-th powers converges to the cube average of the density.

Reading at a stream increment

theorem Algsuperdiff.Section3.Provider.Stream.continuous_smulReg_entry {d : ℕ} {r : ℝ} (hr : r ≠ 0) {a : HCPolySupport.RegCoeffField d} (hcont : ∀ (i j : Fin d), Continuous fun (x : HCPolySupport.Vec d) => a.toFun x i j) (i j : Fin d) : Continuous fun (x : HCPolySupport.Vec d) => (HCPolySupport.smulReg r hr a).toFun x i j

A spatial rescaling of a continuous field is continuous.

theorem Algsuperdiff.Section3.Provider.Stream.continuous_smulReg_finiteShellIncrement_entry {d : ℕ} (omega : Cutoff.ShellSeq d) (n m : ℤ) {r : ℝ} (hr : r ≠ 0) (i j : Fin d) : Continuous fun (x : HCPolySupport.Vec d) => (HCPolySupport.smulReg r hr (Cutoff.finiteShellIncrement omega n m)).toFun x i j

Every spatial rescaling of a finite stream increment is continuous.

theorem Algsuperdiff.Section3.Provider.Stream.regFieldLpMassRep_cubeSet_smulReg_finiteShellIncrement {d : ℕ} {p : ℝ} (hp : 0 < p) (R : HCPolySupport.TriadicCube d) (omega : Cutoff.ShellSeq d) (n m : ℤ) {r : ℝ} (hr : r ≠ 0) : regFieldLpMassRep p (HCPolySupport.cubeSet R) (HCPolySupport.smulReg r hr (Cutoff.finiteShellIncrement omega n m)) = regFieldLpMass p (HCPolySupport.cubeSet R) (HCPolySupport.smulReg r hr (Cutoff.finiteShellIncrement omega n m))

The representative computes the genuine cube L^p mass at every rescaled stream increment. This is the pointwise identity on the image of the (rescaled) increment law used by the concentration step: no a.e. bookkeeping enters, because every increment field is continuous.