SimplexPartition

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

d.simplex.partition: the simplicial refinement SW(□_m) of W(□_m)

This module defines a local implementation of ABK26's e.SW.def, the paragraph "The simplex partition" of sss.affine.approximation:

• the layer-n simplex scale m − (n+1) − h_{n+1} (simplexScale), equivalently the refinement depth 1 + (h_{n+1} − h_n) below the layer-n cube;
• the layer-n cell family S_{m−(n+1)−h_{n+1}}(□) of one Whitney cube (whitneySimplexCells), with the printed cardinality 3^{d(1 + h_{n+1} − h_n)} · d! and the printed size 3^{m−(n+1)−h_{n+1}};
• the simplex partition SW(□_m) = ⋃_n ⋃_{□ ∈ W(□_m,n)} S_{m−(n+1)−h_{n+1}}(□) (simplexPartition) and its membership characterization;
• the printed observation that a layer-n simplex has exactly the layer-(n+1) cube size is not recorded here but in Affine.CommonCoarseMesh, as scale_eq_simplexScale_of_mem_whitneyLayer_succ;
• exactness: the cells of SW(□_m) are pairwise disjoint and their union is the union of the Whitney cubes (simplexPartition_pairwiseDisjoint, iUnion_carrier_simplexPartition); composed with the proved Whitney covering of PartitionCovering this is the partition of the (open) root cube, iUnion_carrier_simplexPartition_eq_openCubeSet. This will support the measure splitting of p.bfA.multiscalebound once the volume layer proves: that consumer needs, in addition, measurability of the cells and the volume facts (|△_n^π| = 3^{dn}/d!, hence the per-simplex refinement count), none of which is proved here.

Compatibility scope

The manuscript infers from the size identity that SW(□_m) is a "valid simplicial partition" with compatible adjacent sizes. SW(□_m) therefore has hanging vertices, and

this module makes no global face-to-face claim, and no downstream statement proved here needs one.

Complete-face compatibility needs two ingredients, not one: the nested-refinement lemma (proved here) and a face-alignment lemma for equal-scale adjacent cubes, which is Provider/Affine/KuhnFaceAlignment.lean's closedCarrier_inter_subset_commonClosedFace.

The independent overlap defect (neighborhoods of distinct bad components are not disjoint) is untouched by this module: no statement below asserts or uses disjointness of component neighborhoods, and the cell interface is component-free, so the overlap-aware consumer statements remain available.

References

• ABK26, e.SW.def; e.simplex.def.

The layer-dependent simplex scale

def Algsuperdiff.Section3.Provider.Whitney.simplexScale (m : ℤ) (hn : ℕ → ℕ) (n : ℕ) : ℤ

The simplex scale of e.SW.def: a layer-n Whitney cube is decomposed into simplices of size 3^{m-(n+1)-h_{n+1}}.

Equations

• Algsuperdiff.Section3.Provider.Whitney.simplexScale m hn n = m - (↑n + 1) - ↑(hn (n + 1))

theorem Algsuperdiff.Section3.Provider.Whitney.simplexScale_le_scale_of_mem_whitneyLayer {d : ℕ} {m : ℤ} {hn : ℕ → ℕ} {n : ℕ} (hstep : hn n ≤ hn (n + 1) + 1) {Q : HCPolySupport.TriadicCube d} (hQ : Q ∈ whitneyLayer m hn n) : simplexScale m hn n ≤ Q.scale

The layer-n simplex scale is at most the layer-n cube scale, so the decomposition of a layer-n cube is nonempty. Uses only h_n ≤ h_{n+1} + 1.

The cells of one Whitney cube

def Algsuperdiff.Section3.Provider.Whitney.whitneySimplexCells {d : ℕ} (m : ℤ) (hn : ℕ → ℕ) (n : ℕ) (Q : HCPolySupport.TriadicCube d) : Finset (KuhnCell d)

S_{m-(n+1)-h_{n+1}}(□): the simplices refining a layer-n Whitney cube.

Equations

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

theorem Algsuperdiff.Section3.Provider.Whitney.mem_whitneySimplexCells_iff {d : ℕ} {m : ℤ} {hn : ℕ → ℕ} {n : ℕ} {Q : HCPolySupport.TriadicCube d} {T : KuhnCell d} : T ∈ whitneySimplexCells m hn n Q ↔ T.supportCube ∈ HCPolySupport.descendantsAtScale Q (simplexScale m hn n)

theorem Algsuperdiff.Section3.Provider.Whitney.carrier_subset_cubeSet_of_mem_whitneySimplexCells {d : ℕ} {m : ℤ} {hn : ℕ → ℕ} {n : ℕ} {Q : HCPolySupport.TriadicCube d} {T : KuhnCell d} (hT : T ∈ whitneySimplexCells m hn n Q) : T.carrier ⊆ HCPolySupport.cubeSet Q

Every cell of the layer-n decomposition sits inside its Whitney cube. This is the containment used.

theorem Algsuperdiff.Section3.Provider.Whitney.cubeSet_eq_iUnion_whitneySimplexCells {d : ℕ} {m : ℤ} {hn : ℕ → ℕ} {n : ℕ} (hstep : hn n ≤ hn (n + 1) + 1) {Q : HCPolySupport.TriadicCube d} (hQ : Q ∈ whitneyLayer m hn n) : HCPolySupport.cubeSet Q = ⋃ T ∈ ↑(whitneySimplexCells m hn n Q), T.carrier

The cells of one layer-n cube tile it exactly.

The simplex partition SW(□_m)

def Algsuperdiff.Section3.Provider.Whitney.simplexPartition {d : ℕ} (m : ℤ) (hn : ℕ → ℕ) : Set (KuhnCell d)

ABK26 e.SW.def: the simplex partition SW(□_m) = ⋃_{n ∈ ℕ} ⋃_{□ ∈ W(□_m, n)} S_{m-(n+1)-h_{n+1}}(□).

Equations

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

theorem Algsuperdiff.Section3.Provider.Whitney.mem_simplexPartition_iff {d : ℕ} {m : ℤ} {hn : ℕ → ℕ} {T : KuhnCell d} : T ∈ simplexPartition m hn ↔ ∃ (n : ℕ), ∃ Q ∈ whitneyLayer m hn n, T ∈ whitneySimplexCells m hn n Q

theorem Algsuperdiff.Section3.Provider.Whitney.mem_simplexPartition_of_mem_whitneySimplexCells {d : ℕ} {m : ℤ} {hn : ℕ → ℕ} {n : ℕ} {Q : HCPolySupport.TriadicCube d} (hQ : Q ∈ whitneyLayer m hn n) {T : KuhnCell d} (hT : T ∈ whitneySimplexCells m hn n Q) : T ∈ simplexPartition m hn

Disjointness of the Whitney cubes

theorem Algsuperdiff.Section3.Provider.Whitney.disjoint_cubeSet_of_mem_whitneyPartition {d : ℕ} {m : ℤ} {hn : ℕ → ℕ} {Q R : HCPolySupport.TriadicCube d} (hQ : Q ∈ whitneyPartition m hn) (hR : R ∈ whitneyPartition m hn) (hne : Q ≠ R) : Disjoint (HCPolySupport.cubeSet Q) (HCPolySupport.cubeSet R)

The Whitney cubes are pairwise disjoint. This is the cube-level input of the exactness of SW(□_m); it is not stated by sss.whitney.partition itself. No hypothesis on the depth profile hn is needed: the statement is the proved whitneyPartition_pairwiseDisjoint_cubeSet of PartitionCovering, whose exit-depth proof is profile-free.

Exactness of SW(□_m)

theorem Algsuperdiff.Section3.Provider.Whitney.simplexPartition_pairwiseDisjoint {d : ℕ} {m : ℤ} {hn : ℕ → ℕ} : (simplexPartition m hn).PairwiseDisjoint KuhnCell.carrier

The cells of SW(□_m) are pairwise disjoint. This is a partition statement for the canonical half-open realizations; it is not a face-to-face assertion (see the module docstring). No hypothesis on the depth profile hn is needed.

theorem Algsuperdiff.Section3.Provider.Whitney.iUnion_carrier_simplexPartition {d : ℕ} {m : ℤ} {hn : ℕ → ℕ} (hstep : ∀ (n : ℕ), hn n ≤ hn (n + 1) + 1) : ⋃ T ∈ simplexPartition m hn, T.carrier = ⋃ Q ∈ whitneyPartition m hn, HCPolySupport.cubeSet Q

SW(□_m) is an exact refinement of W(□_m): the canonical cells cover exactly the Whitney cubes. The Whitney covering ⋃_{□ ∈ W(□_m)} □ = □_m is proved (openCubeSet_originCube_eq_iUnion_whitneyPartition), so this composes to the partition of the root cube: iUnion_carrier_simplexPartition_eq_openCubeSet.

theorem Algsuperdiff.Section3.Provider.Whitney.iUnion_carrier_simplexPartition_eq_openCubeSet {d : ℕ} [NeZero d] {m : ℤ} {hn : ℕ → ℕ} (hstep : ∀ (n : ℕ), hn n ≤ hn (n + 1) + 1) : ⋃ T ∈ simplexPartition m hn, T.carrier = HCPolySupport.openCubeSet (HCPolySupport.originCube d m)

SW(□_m) tiles □_m: the cells of the simplex partition cover the root cube exactly. Together with simplexPartition_pairwiseDisjoint this is the partition-of-□_m statement; the carrier is the open root cube, which is the manuscript's own □_m and the form forced by the termination clause of sss.whitney.partition (see PartitionCovering).

This will support the measure splitting of p.bfA.multiscalebound once the volume layer proves: that consumer needs, in addition, measurability of the cells and the volume facts (|△_n^π| = 3^{dn}/d!, hence the per-simplex refinement count), which are not proved here.