OffGridStabilitySubadditivity

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

Countable subadditivity of the response functional

Then, by subadditivity and (e.bound.one.cube.by.lambdas), |σ_*^{-1}(U;a)| ≤ ∑_{n=-∞}^0 ∑_{z ∈ 𝒢_n(U)} (|□_n| / |U|) |σ_*^{-1}(z+□_n;a)|

for an arbitrary domain U ⊆ □_0 and the greedy family 𝒢_n(U). That is a countably infinite subadditivity over a family of cubes of unboundedly many scales inside an arbitrary domain.

CoarseGraining's subadditivity surface stops strictly short of it. Its public form (Ch02.ResponseSubadditivityAndScalingTheory.responseJ_subadditive) is indexed by a Ch02.DomainPartition, whose triadic_realization field forces

• a Fintype cell index, and
• cells enumerating descendantsAtDepth root depth for one root cube and one common depth — an equal-depth exact triadic partition of a grid cube.

Neither the countability nor the multi-scale family nor the off-grid parent can be expressed there. This module proves the missing inequality directly on CoarseGraining's set-level Homogenization.ResponseJ, for an arbitrary countable a.e. partition of an arbitrary open set, and then specialises it to the maximal-cube family of OffGridStabilityGeometry.lean.

The ingredients used, all public in CoarseGraining

• Homogenization.responseJValueSet_nonempty, responseJValueSet_mem;
• Homogenization.scalarResponseIntegrand_integrableOn_of_isEllipticFieldOn;
• Homogenization.AHarmonicFunction.restrictOfIsEllipticFieldOn — restriction of an a-harmonic function to an open subset, which is what makes one admissible field for the big domain admissible for every cell;
• Homogenization.le_responseJ_of_mem_responseJValueSet_of_isEllipticFieldOn;
• Homogenization.IsEllipticFieldOn.mono;
• Mathlib's MeasureTheory.hasSum_integral_iUnion.

The one genuinely new step is that the exact finite partition identity CoarseGraining uses (volumeAverage over descendantsAverage) is replaced by the countable hasSum_integral_iUnion, which needs only pairwise disjointness, measurability and an a.e. cover.

Main results

• responseJ_le_tsum_of_countable_cover — the countable subadditivity.
• responseJ_offGridCube_le_tsum_maximalCubes — the same across the maximal grid cubes of an off-grid cube, in the ∑ |Q|/|V| normalization of the printed display.

References

• ABK26, l.lambdas.stability.
• CoarseGraining, Homogenization/CoarseGraining/Definitions.lean (ResponseJ), Homogenization/CoarseGraining/ResponseIdentities/Foundations/Ellipticity.lean, Homogenization//Harmonic.lean, Homogenization/Book/Ch02/Theorems/SubadditivityScalingDefinitions.lean (the finite-partition ceiling this module lifts).

1. Countable subadditivity of ResponseJ

theorem Algsuperdiff.Section4.Provider.ExcessDecay.responseJ_le_tsum_of_countable_cover {d : ℕ} {ι : Type} [Countable ι] {V : Set (HCPolySupport.Vec d)} {a : HCPolySupport.CoeffField d} {lam Lam : ℝ} {p q : HCPolySupport.Vec d} (hVopen : IsOpen V) (hVtop : MeasureTheory.volume V < ⊤) (hVpos : (MeasureTheory.volume V).toReal ≠ 0) (hEll : HCPolySupport.IsEllipticFieldOn lam Lam V a) (cell : ι → Set (HCPolySupport.Vec d)) (hopen : ∀ (i : ι), IsOpen (cell i)) (hmeas : ∀ (i : ι), MeasurableSet (cell i)) (hsub : ∀ (i : ι), cell i ⊆ V) (hdisj : Pairwise (Function.onFun Disjoint cell)) (hcelltop : ∀ (i : ι), MeasureTheory.volume (cell i) < ⊤) (hcellpos : ∀ (i : ι), (MeasureTheory.volume (cell i)).toReal ≠ 0) (hcover : MeasureTheory.volume (V \ ⋃ (i : ι), cell i) = 0) (B : ι → ℝ) (hB : ∀ (i : ι), HCPolySupport.ResponseJ (cell i) p q a ≤ B i) (hsummable : Summable fun (i : ι) => (MeasureTheory.volume (cell i)).toReal * B i) : HCPolySupport.ResponseJ V p q a ≤ (MeasureTheory.volume V).toReal⁻¹ * ∑' (i : ι), (MeasureTheory.volume (cell i)).toReal * B i

Countable subadditivity of the response functional.

If the open set V is covered, up to a null set, by countably many pairwise disjoint open subsets cell i, then the response of V is at most the |cell i| / |V|-weighted sum of any majorant of the responses of the cells.

This is the countable, multi-scale, off-grid replacement for CoarseGraining's DomainPartition-indexed subadditivity, whose triadic_realization field forces a finite equal-depth partition of a grid cube.

2. The off-grid specialisation

theorem Algsuperdiff.Section4.Provider.ExcessDecay.volume_offGridCube_diff_iUnion_openCubeSet {d : ℕ} [NeZero d] (w : HCPolySupport.Vec d) (P : HCPolySupport.TriadicCube d) : MeasureTheory.volume (offGridCube w P \ ⋃ (Q : ↑(maximalCubes (offGridCube w P))), HCPolySupport.openCubeSet ↑Q) = 0

The open realizations of the maximal cubes cover the off-grid cube up to a null set: the discarded set is the countable union of the cubes' boundaries.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.responseJ_offGridCube_le_tsum_maximalCubes {d : ℕ} [NeZero d] {w : HCPolySupport.Vec d} {P : HCPolySupport.TriadicCube d} {a : HCPolySupport.CoeffField d} {lam Lam : ℝ} {p q : HCPolySupport.Vec d} (hEll : HCPolySupport.IsEllipticFieldOn lam Lam (offGridCube w P) a) (B : HCPolySupport.TriadicCube d → ℝ) (hB : ∀ (Q : ↑(maximalCubes (offGridCube w P))), HCPolySupport.ResponseJ (HCPolySupport.openCubeSet ↑Q) p q a ≤ B ↑Q) (hsummable : Summable fun (Q : ↑(maximalCubes (offGridCube w P))) => HCPolySupport.cubeVolume ↑Q * B ↑Q) : HCPolySupport.ResponseJ (offGridCube w P) p q a ≤ (HCPolySupport.cubeVolume P)⁻¹ * ∑' (Q : ↑(maximalCubes (offGridCube w P))), HCPolySupport.cubeVolume ↑Q * B ↑Q

The printed display, formalized.

For an arbitrary real translate w + □_k of a triadic cube, the response of the off-grid cube is at most the |Q| / |w + □_k|-weighted sum of any majorant of the responses of its maximal grid subcubes. This is |σ_*^{-1}(U)| ≤ ∑_n ∑_{z ∈ 𝒢_n(U)} (|□_n|/|U|) |σ_*^{-1}(z+□_n)| at the level of the response functional itself.

B and its two obligations are conditional A, per the disclosure in the module docstring.