CommonCoarseMesh

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

The common coarse mesh and the competitor on it

This module provides a proved local implementation of the corrected Step 1 construction associated with ABK26's l.piecewise.affine.approx, in the form prescribed:

Let j be the least layer occupied by the neighborhood. Then 𝒩(𝒞) ⊆ 𝒲(□_m, j) ∪ 𝒲(□_m, j+1). The target-j common mesh is exactly the final e.SW.def mesh on layer j. On layer j+1, the printed final mesh refines that common coarse mesh. Hence one may prescribe values and extend affinely on the common coarse mesh, then restrict the affine maps to the deeper final simplices. The restriction remains affine, continuous, and subordinate to the printed SW(□_m).

commonCoarseMesh N s is that mesh: every cube of the window N triangulated at the single scale s.

Scope: what this module does NOT do

• The two-layer window is a hypothesis here, not a theorem. Every statement takes the window N and the layer bound as explicit binders; the fact that the actual touching neighborhood 𝒩(𝒞) occupies at most two consecutive layers -- the second "small point" -- is a statement about l.bad.clusters.geometry, is not proved here, and is not assumed anywhere below in disguise: nothing in this file mentions 𝒩(𝒞).
• No global assembly. The competitor is built on one window. Assembling the per-component window competitors into a single global ℓ̂_p on □_m still requires handling the overlap (neighborhoods of distinct components are not disjoint) and the matching of each window competitor with ℓ_p across the outer boundary of its window. Neither is proved here or anywhere in this repository.
• No H¹ statement. e.hat.linear.1 (label and content) and the hF/hG binders of sum_of_a_decomp require an H10Function witness and an L² weak gradient; see the scope section of GlobalGluing.lean.
• /-c1 are not consumed: no gradient estimate, no collar constant and no component diameter occurs here.

References

• ABK26, (e.SW.def), (l.piecewise.affine.approx, e.hat.linear.properties), (Step 1), (the prescribed vertex values), (ℓ_e(x) = e·x).

The common coarse mesh

def Algsuperdiff.Section3.Provider.Affine.commonCoarseMesh {d : ℕ} (N : Finset (HCPolySupport.TriadicCube d)) (s : ℤ) : Finset (Whitney.KuhnCell d)

The common coarse mesh: every cube of the window N triangulated at the one scale s. On the shallow layer of a two-layer window this is e.SW.def itself; on the deeper layer it is the d!-simplex decomposition of the cube at its own scale, which the final e.SW.def mesh refines.

Equations

• Algsuperdiff.Section3.Provider.Affine.commonCoarseMesh N s = N.biUnion fun (R : HCPolySupport.TriadicCube d) => Algsuperdiff.Section3.Provider.Whitney.triadicSimplexPartition R s

theorem Algsuperdiff.Section3.Provider.Affine.mem_commonCoarseMesh_iff {d : ℕ} {N : Finset (HCPolySupport.TriadicCube d)} {s : ℤ} {T : Whitney.KuhnCell d} : T ∈ commonCoarseMesh N s ↔ ∃ R ∈ N, T.supportCube ∈ HCPolySupport.descendantsAtScale R s

The two-layer window

theorem Algsuperdiff.Section3.Provider.Affine.scale_eq_simplexScale_of_mem_whitneyLayer_succ {d : ℕ} {m : ℤ} {hn : ℕ → ℕ} {j : ℕ} {R : HCPolySupport.TriadicCube d} (hR : R ∈ Whitney.whitneyLayer m hn (j + 1)) : R.scale = Whitney.simplexScale m hn j

The scale identity, in the form the window needs: a layer-(j+1) Whitney cube has exactly the layer-j simplex scale.