LayerMass

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

The Whitney layer mass, and the simplex-to-layer regrouping of Step 3

This module discharges the explicit layer-mass A obligation of Provider.Multiscale.ConclusionAssembly, LayerMassBound, and supplies the composition statement that carries the [0,∞] simplex sum of Multiscale.sum_of_a_decomp (SubadditiveDecomposition.lean) into the layer series of Step 3 of p.bfA.multiscalebound.

What is proved

1. The boundary-collar count (card_descendantsAtDepth_filter_touchesBoundary_le): at most 2 d 3^{j(d-1)} of the 3^{jd} depth-j triadic descendants of □_m touch ∂□_m. The proof is a union bound over the 2d faces, reduced by card_descendantsAtDepth_filter_index_le to the one-coordinate slice count #{R ∈ descendantsAtDepth Q j : R.index i = c} ≤ 3^{j(d-1)}, itself an induction on j from the single-generation fact that prescribing one index coordinate of a child forces one triadic digit. The naive recursion "a boundary cube has at most 3^d - 2^d boundary children" is not enough: it gives the decay (1 - (2/3)^d)^j, not the 3^{-j} the manuscript needs. The union bound over faces is what produces 3^{-j}.

2. The layer mass bound (sum_cubeMassRatio_whitneyLayer_le, layerMassBound_six_mul_dim): 𝒲(□_m,n) carries mass at most 6 d 3^{-n} inside □_m, i.e. LayerMassBound d m hn (6 d). Route: a layer-n cube is a depth-(1+h_n) descendant of a touching depth-(n-1) descendant of □_m (whitneyLayer_subset_collar), so

   # 𝒲(□_m,n) ≤ (2 d 3^{(n-1)(d-1)}) · (3^d)^{1+h_n} ,
   

   and each layer cube carries mass (3^d)^{-(n+h_n)}; the two powers collapse to 2 d 3^{-(n-1)} = 6 d 3^{-n} exactly (three_pow_collar_identity). The constant 6 d is the one the ConclusionAssembly docstring predicts. It is not claimed sharp: keeping the extra factor 2/3 from "a touching cube has at most 2 · 3^{d-1} non-touching children" would give 4 d, which for d = 1, n ≥ 2 is the exact layer mass 4 · 3^{-n} (at n = 1 it is 3^{-1} — one touching ancestor, not two;). That refinement is not proved here — nothing downstream distinguishes 4 d from 6 d, since layerSumConst carries Cmass as a parameter.

3. The simplex-to-layer regrouping (tsum_simplexPartition_eq_tsum_layer, toReal_tsum_simplexPartition_le_tsum, toReal_tsum_simplexPartition_le_payload, and its [0,∞]-valued twin tsum_simplexPartition_le_ofReal_payload at the identical binder list): SW(□_m) is the disjoint union over n of the finite cell families layerCells m hn n, so any [0,∞]-valued sum over SW(□_m) regroups as ∑'_n ∑_{□ ∈ 𝒲(□_m,n)} ∑_{𝔰 ∈ S(□)}, with no summability hypothesis. Composed with toReal and with ConclusionAssembly.tsum_layerContrib_le_payload this is the missing link between the right-hand side of e.sum-of-a-decomp and the Step-3 payload.

What is not proved

The exact boundary-touching count 3^{dt} - (3^t - 2)^d is not proved. It needs the surjectivity half of the index-box bijection (every u with |u i| ≤ E_t is attained by a depth-t descendant of □_m), which no consumer in this repository asks for: the layer mass bound consumes only the upper bound 2 d 3^{t(d-1)}. The injective half is proved (Provider.Whitney.index_injOn_descendantsAtDepth, Provider.Whitney.index_mem_cubeFinset_of_mem_descendantsAtDepth) and the cardinality #descendantsAtDepth Q t = 3^{dt} is CoarseGraining's Homogenization.descendantsAtDepth_card, restated here as card_descendantsAtDepth_originCube.

References

• ABK26, sss.whitney.partition; p.bfA.multiscalebound Step 3; e.SW.def.

The cardinality of a depth-t descendant family

theorem Algsuperdiff.Section3.Provider.Multiscale.card_descendantsAtDepth_originCube {d : ℕ} (m : ℤ) (t : ℕ) : (HCPolySupport.descendantsAtDepth (HCPolySupport.originCube d m) t).card = 3 ^ (d * t)

#{□ ⊆ □_m : |□| = 3^{m-t}} = 3^{dt}, CoarseGraining's Homogenization.descendantsAtDepth_card in the manuscript's exponent form. Together with Provider.Whitney.index_injOn_descendantsAtDepth and Provider.Whitney.index_mem_cubeFinset_of_mem_descendantsAtDepth this says the depth-t descendants of □_m inject into the index box {|u i| ≤ E_t}, which has the same cardinality 3^{dt}; the surjectivity half is not needed below and is not proved (see the module docstring).

The one-generation slice count

theorem Algsuperdiff.Section3.Provider.Multiscale.card_childCubes_filter_index_le {d : ℕ} (Q : HCPolySupport.TriadicCube d) (i : Fin d) (c : ℤ) : {R ∈ HCPolySupport.childCubes Q | R.index i = c}.card ≤ 3 ^ (d - 1)

Prescribing one index coordinate of a triadic child forces one of the d triadic digits, so at most 3^{d-1} of the 3^d children of a cube have a prescribed value in coordinate i.

The depth-j slice count

theorem Algsuperdiff.Section3.Provider.Multiscale.card_descendantsAtDepth_filter_index_le {d : ℕ} (Q : HCPolySupport.TriadicCube d) (i : Fin d) (j : ℕ) (c : ℤ) : {R ∈ HCPolySupport.descendantsAtDepth Q j | R.index i = c}.card ≤ (3 ^ (d - 1)) ^ j

The slice count. At most (3^{d-1})^j of the (3^d)^j depth-j descendants of a cube have a prescribed value in a fixed index coordinate.

The boundary-collar count

theorem Algsuperdiff.Section3.Provider.Multiscale.card_descendantsAtDepth_filter_touchesBoundary_le {d : ℕ} (m : ℤ) (j : ℕ) : (Finset.filter (Whitney.TouchesBoundary m) (HCPolySupport.descendantsAtDepth (HCPolySupport.originCube d m) j)).card ≤ 2 * d * (3 ^ (d - 1)) ^ j

The boundary-collar count. At most 2 d 3^{j(d-1)} of the 3^{jd} depth-j triadic descendants of □_m touch ∂□_m; equivalently the boundary collar of □_m at scale 3^{m-j} occupies volume fraction at most 2 d 3^{-j} (sum_cubeMassRatio_boundaryCollar_le). This is the geometric source of the 3^{-n} of Step 3.

The collapse arithmetic

The mass of the boundary collar

The Whitney layer sits in the depth-(n-1) collar

theorem Algsuperdiff.Section3.Provider.Multiscale.whitneyLayer_subset_collar {d : ℕ} (m : ℤ) (hn : ℕ → ℕ) (n : ℕ) : Whitney.whitneyLayer m hn n ⊆ (Finset.filter (Whitney.TouchesBoundary m) (HCPolySupport.descendantsAtDepth (HCPolySupport.originCube d m) (n - 1))).biUnion fun (A : HCPolySupport.TriadicCube d) => HCPolySupport.descendantsAtDepth A (1 + hn n)

A layer-n Whitney cube is a depth-(1+h_n) descendant of a boundary-touching depth-(n-1) descendant of □_m.

theorem Algsuperdiff.Section3.Provider.Multiscale.card_whitneyLayer_le {d : ℕ} (m : ℤ) (hn : ℕ → ℕ) (n : ℕ) : (Whitney.whitneyLayer m hn n).card ≤ 2 * d * (3 ^ (d - 1)) ^ (n - 1) * (3 ^ d) ^ (1 + hn n)

The layer-n cube count: at most 2 d 3^{(n-1)(d-1)} (3^d)^{1+h_n}.

The layer mass bound

theorem Algsuperdiff.Section3.Provider.Multiscale.sum_cubeMassRatio_whitneyLayer_le {d : ℕ} (m : ℤ) (hn : ℕ → ℕ) (n : ℕ) : ∑ Q ∈ Whitney.whitneyLayer m hn n, Whitney.cubeMassRatio (HCPolySupport.originCube d m) Q ≤ 6 * ↑d * 3 ^ (-↑n)

The Whitney layer mass estimate. The layer-n cubes of 𝒲(□_m) occupy mass at most 6 d 3^{-n} inside □_m. Layer 0 is empty, so the bound is trivial there.

Step 3 at the discharged layer-mass input

The simplex-to-layer regrouping bridge

def Algsuperdiff.Section3.Provider.Multiscale.layerCells {d : ℕ} (m : ℤ) (hn : ℕ → ℕ) (n : ℕ) : Finset (Whitney.KuhnCell d)

The layer-n cells of SW(□_m): the simplices of e.SW.def cut out of the layer-n Whitney cubes. SW(□_m) is the union of these finite families over n (simplexPartition_eq_iUnion_layerCells).

Equations

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

theorem Algsuperdiff.Section3.Provider.Multiscale.mem_layerCells_iff {d : ℕ} {m : ℤ} {hn : ℕ → ℕ} {n : ℕ} {T : Whitney.KuhnCell d} : T ∈ layerCells m hn n ↔ ∃ Q ∈ Whitney.whitneyLayer m hn n, T ∈ Whitney.whitneySimplexCells m hn n Q

theorem Algsuperdiff.Section3.Provider.Multiscale.simplexPartition_eq_iUnion_layerCells {d : ℕ} (m : ℤ) (hn : ℕ → ℕ) : Whitney.simplexPartition m hn = ⋃ (n : ℕ), ↑(layerCells m hn n)

theorem Algsuperdiff.Section3.Provider.Multiscale.pairwiseDisjoint_whitneySimplexCells {d : ℕ} (m : ℤ) (hn : ℕ → ℕ) (n : ℕ) : (↑(Whitney.whitneyLayer m hn n)).PairwiseDisjoint (Whitney.whitneySimplexCells m hn n)

Within one layer the cell families of distinct Whitney cubes are disjoint: a cell determines the Whitney cube containing it (whitneyCubeOf).

theorem Algsuperdiff.Section3.Provider.Multiscale.pairwiseDisjoint_layerCells {d : ℕ} {m : ℤ} {hn : ℕ → ℕ} (hmono : Monotone hn) : Set.univ.PairwiseDisjoint fun (n : ℕ) => ↑(layerCells m hn n)

Distinct layers of SW(□_m) are disjoint. A cell determines its Whitney cube, and a Whitney cube determines its layer once the scale profile is monotone (Provider.Whitney.whitneyLayer_disjoint).

theorem Algsuperdiff.Section3.Provider.Multiscale.tsum_simplexPartition_eq_tsum_layer {d : ℕ} {m : ℤ} {hn : ℕ → ℕ} (hmono : Monotone hn) (f : Whitney.KuhnCell d → ENNReal) : ∑' (T : ↑(Whitney.simplexPartition m hn)), f ↑T = ∑' (n : ℕ), ∑ Q ∈ Whitney.whitneyLayer m hn n, ∑ T ∈ Whitney.whitneySimplexCells m hn n Q, f T

The regrouping of a [0,∞] sum over SW(□_m) into the Whitney layer series. SW(□_m) is the disjoint union over n of the finite families layerCells m hn n, so any [0,∞]-valued sum over it equals the iterated sum

∑'_n  ∑_{□ ∈ 𝒲(□_m,n)}  ∑_{𝔰 ∈ S_{m-(n+1)-h_{n+1}}(□)}  f 𝔰 ,

with no summability hypothesis: in [0,∞] every family is summable and rearrangement is unconditional. This is the composition statement between the right-hand side of Multiscale.sum_of_a_decomp (SubadditiveDecomposition.lean) and the layer series of Step 3.

theorem Algsuperdiff.Section3.Provider.Multiscale.toReal_tsum_simplexPartition_le_tsum {d : ℕ} {m : ℤ} {hn : ℕ → ℕ} (hmono : Monotone hn) (f : Whitney.KuhnCell d → ENNReal) {g : ℕ → ℝ} (hg0 : ∀ (n : ℕ), 0 ≤ g n) (hgsum : Summable g) (hlayer : ∀ (n : ℕ), ∑ Q ∈ Whitney.whitneyLayer m hn n, ∑ T ∈ Whitney.whitneySimplexCells m hn n Q, f T ≤ ENNReal.ofReal (g n)) : (∑' (T : ↑(Whitney.simplexPartition m hn)), f ↑T).toReal ≤ ∑' (n : ℕ), g n

The regrouping bridge with toReal. A per-layer real majorant of the [0,∞] cell sums controls the real value of the whole simplex sum by the real layer series. The finiteness needed for toReal is produced by the majorant, not assumed.

theorem Algsuperdiff.Section3.Provider.Multiscale.tsum_simplexPartition_le_ofReal_payload {d : ℕ} {m : ℤ} {hn : ℕ → ℕ} {b γ ε Cmass Ktot Ccol : ℝ} {hs k₀ : ℕ} {Mass Bad : ℕ → ℝ} (hmono : Monotone hn) (hb0 : 0 < b) (hb9 : 9 * b ≤ 1) (hγ0 : 0 ≤ γ) (hγ : 4 * γ ≤ 1 - b) (hK : 0 ≤ Ktot) (hC : 0 ≤ Ccol) (hCmass : 0 ≤ Cmass) (hε0 : 0 ≤ ε) (hεk0 : ε ≤ Real.exp (-↑k₀)) (hMass0 : ∀ (j : ℕ), 0 ≤ Mass j) (hBad0 : ∀ (j : ℕ), 0 ≤ Bad j) (hMass : ∀ (j : ℕ), Mass j ≤ Cmass * 3 ^ (-↑j)) (hBadMass : ∀ (j : ℕ), Bad j ≤ Cmass * 3 ^ (-↑j)) (hBadDens : ∀ (j : ℕ), Bad j ≤ ε + 3 ^ (-(layerQuantity b hs k₀ j / 2))) (f : Whitney.KuhnCell d → ENNReal) (hlayer : ∀ (n : ℕ), ∑ Q ∈ Whitney.whitneyLayer m hn n, ∑ T ∈ Whitney.whitneySimplexCells m hn n Q, f T ≤ ENNReal.ofReal (layerContrib b γ hs k₀ Ktot Ccol Mass Bad n)) : ∑' (T : ↑(Whitney.simplexPartition m hn)), f ↑T ≤ ENNReal.ofReal (layerSumConst b γ k₀ Ktot Ccol Cmass * (3 ^ (γ * ↑hs) * (1 + 3 ^ (2 * b * ↑hs) * Real.exp (-(↑k₀ / 36)))))

The Step-3 composition in [0,∞] --- the ofReal twin of toReal_tsum_simplexPartition_le_payload, at the identical binder list.