GlobalCompetitor

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

The global piecewise-affine competitor ℓ̂_p on □_m

• ** the global assembly.** The competitor is no longer built on the window 𝒩(C) alone: it is the affine extension of the one global vertex datum competitorVertexData C p of CompetitorVertexData.lean on the uniform scale-s Kuhn mesh of the whole root cube □_m (rootCoarseMesh), at the window's own common coarse scale s = simplexScale m hn j. Because that mesh is single-scale and finite, the gluing of GlobalGluing.lean applies verbatim, and the resulting function is well defined and continuous on all of □_m, not merely on the window.
• (b) the matching with ℓ_p across the outer boundary of the window. The outer-boundary matching is proved, not assumed: globalCompetitor_eqOn_linearFn_closedCarrier_of_notMem_commonCoarseMesh states that on the closed carrier of every root cell off the window mesh the global competitor is ℓ_p, and notMem_commonCoarseMesh_of_mem_cubeSet puts every root cell that meets a Whitney cube off 𝒩(C) outside that mesh. Together they pin the function as "the window competitor inside 𝒩(C), ℓ_p outside", i.e. the manuscript's own ℓ̂_p. These are ordinary Provider results and do not settle either item as a source-node fraction.

The engine: the closed-star lemma

The correction is a geometric one, and it is mem_commonCoarseMesh_of_vertex_mem_closedCubeCarrier:

if a vertex of a scale-s root cell lies in the closed carrier of C, then that cell already belongs to the window mesh commonCoarseMesh 𝒩(C) s.

Equivalently: a root cell outside the window mesh has all its vertices off the closed bad cubes, so its interpolant of the global datum is exactly ℓ_p (eqOn_vertexSet_competitorVertexData_linearFn_of_notMem_commonCoarseMesh). Its proof is the locally-finite closed-star argument:

1. exists_whitneyCube_inter_cubeSet_mem_closedBall -- an interior point v in the closed realization of a triadic cube B lies in the closed cube of some Whitney cube whose half-open cube already meets B. This is local finiteness of 𝒲(□_m) in the interior, obtained from the upper half (boundaryMargin_le_of_mem_whitneyLayer): a point at boundary margin ≥ ε can only be met by Whitney cubes of boundedly many layers, and each layer is a Finset.
2. that Whitney cube touches C (both closed cubes contain v), hence lies in 𝒩(C), hence has scale ≥ s by the two-layer window hypothesis;
3. a scale-s root cube meeting a Whitney cube of scale ≥ s is a descendant of it (mem_descendantsAtScale_of_cubeSet_inter_nonempty), so B sits in a window cube and the cell is a window cell.

No "extra collar layer" and no cutoff is needed; the mesh is the same single-scale mesh, extended over the root cube.

Scope: what this module does NOT do

• One bad family only. Everything is stated at a single family C whose touching neighborhood occupies at most two consecutive layers. What this module supplies for it is exactly what that superposition needs: each component correction globalCompetitor − ℓ_p is now known to be continuous on all of □_m, to vanish on the closed cube of every Whitney cube off that component's neighborhood, and to be affine on every final e.SW.def cell. The remaining work is the locally-finite sum over components (local finiteness of the component carriers, and the finsum), and the resulting clause bookkeeping at badFamily M m hn omega rather than at one C.
• The two-layer window is a hypothesis, not a theorem (as in CommonCoarseMesh.lean): hNlayer carries 𝒩(C) ⊆ 𝒲(□_m,j) ∪ 𝒲(□_m,j+1), the conclusion; the proved Whitney.whitneyNeighborhood_finite_and_mem_leastLayer_or_succ is what a caller discharges it with (it also supplies the finiteness behind the Finset N). Nothing here proves it, and no three-layer window is used.
• /-c1 are read and not consumed: no gradient estimate, no collar constant, no component diameter and no overlap count occurs here. is read and not consumed: no connectivity statement is used -- the window is an explicit binder.

References

• ABK26, (e.SW.def), labels (l.piecewise.affine.approx, e.hat.linear.properties; clause 1, clause 3), (the false disjointness), (Step 1, with "well-defined and continuous"), (the prescribed vertex values), (the layer/boundary distance), (ℓ_e(x) = e·x).
• The private nesting helper mem_descendantsAtDepth_of_mem_cubeSet_inter' is a re-proof of the private PartitionCovering.mem_descendantsAtDepth_of_mem_cubeSet_inter of this repository (private, hence not importable).

Local finiteness of the Whitney partition in the interior

theorem Algsuperdiff.Section3.Provider.Affine.exists_whitneyCube_inter_cubeSet_mem_closedBall {d : ℕ} [NeZero d] {m : ℤ} {hn : ℕ → ℕ} {B : HCPolySupport.TriadicCube d} {v : HCPolySupport.Vec d} (hv : v ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hvB : v ∈ Metric.closedBall (HCPolySupport.cubeCenter B) (HCPolySupport.cubeRadius B)) : ∃ Q ∈ Whitney.whitneyPartition m hn, (HCPolySupport.cubeSet Q ∩ HCPolySupport.cubeSet B).Nonempty ∧ v ∈ Metric.closedBall (HCPolySupport.cubeCenter Q) (HCPolySupport.cubeRadius Q)

The closed-star bridge. An interior point in the closed realization of a triadic cube B is in the closed realization of some Whitney cube whose half-open realization already meets B.

theorem Algsuperdiff.Section3.Provider.Affine.mem_descendantsAtScale_of_cubeSet_inter_nonempty {d : ℕ} {m : ℤ} {hn : ℕ → ℕ} {s : ℤ} {Q B : HCPolySupport.TriadicCube d} (hQ : Q ∈ Whitney.whitneyPartition m hn) (hB : B ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d m) s) (hs : s ≤ Q.scale) (hinter : (HCPolySupport.cubeSet Q ∩ HCPolySupport.cubeSet B).Nonempty) : B ∈ HCPolySupport.descendantsAtScale Q s

A scale-s triadic cube of the root that meets a Whitney cube of scale at least s is a descendant of it.

The closed-star lemma

theorem Algsuperdiff.Section3.Provider.Affine.mem_commonCoarseMesh_of_vertex_mem_closedCubeCarrier {d : ℕ} [NeZero d] {m : ℤ} {hn : ℕ → ℕ} {s : ℤ} {C : Set (HCPolySupport.TriadicCube d)} (hC : C ⊆ Whitney.whitneyPartition m hn) {N : Finset (HCPolySupport.TriadicCube d)} (hN : ∀ Q ∈ Whitney.whitneyPartition m hn, (∃ R ∈ C, Whitney.CubeTouch Q R) → Q ∈ N) (hs : ∀ Q ∈ N, s ≤ Q.scale) {T : Whitney.KuhnCell d} (hT : T.supportCube ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d m) s) {v : HCPolySupport.Vec d} (hv : v ∈ T.vertexSet) (hvC : v ∈ Whitney.closedCubeCarrier C) : T ∈ commonCoarseMesh N s

The closed-star lemma. If a vertex of a scale-s cell of the root mesh lies in the closed carrier of a family C of Whitney cubes, then the cell already belongs to the common coarse mesh of any window N containing every Whitney cube touching C, provided the window sits at scale at least s.

The root mesh

def Algsuperdiff.Section3.Provider.Affine.rootCoarseMesh {d : ℕ} (m s : ℤ) : Finset (Whitney.KuhnCell d)

The uniform scale-s Kuhn mesh of the root cube □_m.

Equations

• Algsuperdiff.Section3.Provider.Affine.rootCoarseMesh m s = Algsuperdiff.Section3.Provider.Whitney.triadicSimplexPartition (HCPolySupport.originCube d m) s

theorem Algsuperdiff.Section3.Provider.Affine.mem_rootCoarseMesh_iff {d : ℕ} {m s : ℤ} {T : Whitney.KuhnCell d} : T ∈ rootCoarseMesh m s ↔ T.supportCube ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d m) s

theorem Algsuperdiff.Section3.Provider.Affine.supportCube_scale_eq_of_mem_rootCoarseMesh {d : ℕ} {m s : ℤ} (hs : s ≤ m) {T : Whitney.KuhnCell d} (hT : T ∈ rootCoarseMesh m s) : T.supportCube.scale = s

theorem Algsuperdiff.Section3.Provider.Affine.cubeSet_originCube_subset_iUnion_closedCarrier_rootCoarseMesh {d : ℕ} {m s : ℤ} (hs : s ≤ m) : HCPolySupport.cubeSet (HCPolySupport.originCube d m) ⊆ ⋃ T ∈ ↑(rootCoarseMesh m s), T.closedCarrier

theorem Algsuperdiff.Section3.Provider.Affine.mem_descendantsAtScale_originCube_of_mem_descendantsAtScale {d : ℕ} {m : ℤ} {hn : ℕ → ℕ} {s : ℤ} {Q B : HCPolySupport.TriadicCube d} (hQ : Q ∈ Whitney.whitneyPartition m hn) (hs : s ≤ Q.scale) (hB : B ∈ HCPolySupport.descendantsAtScale Q s) : B ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d m) s

A triadic descendant of a Whitney cube is a triadic descendant of the root cube at the same scale.

The global competitor of one bad component

noncomputable def Algsuperdiff.Section3.Provider.Affine.globalCompetitor {d : ℕ} (m s : ℤ) (C : Set (HCPolySupport.TriadicCube d)) (p : HCPolySupport.Vec d) : HCPolySupport.Vec d → ℝ

The global piecewise-affine competitor ℓ̂_p of the bad family C.

Equations

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

noncomputable def Algsuperdiff.Section3.Provider.Affine.globalCompetitorSlope {d : ℕ} (m s : ℤ) (C : Set (HCPolySupport.TriadicCube d)) (p : HCPolySupport.Vec d) : HCPolySupport.Vec d → HCPolySupport.Vec d

The global piecewise-constant gradient field ∇ℓ̂_p.

Equations

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

theorem Algsuperdiff.Section3.Provider.Affine.globalCompetitorSlope_of_mem_openCarrier {d : ℕ} {m s : ℤ} (hs : s ≤ m) (C : Set (HCPolySupport.TriadicCube d)) (p : HCPolySupport.Vec d) {T : Whitney.KuhnCell d} (hT : T ∈ rootCoarseMesh m s) {x : HCPolySupport.Vec d} (hx : x ∈ T.openCarrier) : globalCompetitorSlope m s C p x = kuhnSlope T (competitorVertexData C p)

theorem Algsuperdiff.Section3.Provider.Affine.globalCompetitorSlope_of_forall_notMem {d : ℕ} {m s : ℤ} (C : Set (HCPolySupport.TriadicCube d)) (p : HCPolySupport.Vec d) {x : HCPolySupport.Vec d} (hx : ∀ T ∈ rootCoarseMesh m s, x ∉ T.openCarrier) : globalCompetitorSlope m s C p x = p

The matching with ℓ_p off the window

theorem Algsuperdiff.Section3.Provider.Affine.eqOn_vertexSet_competitorVertexData_linearFn_of_notMem_commonCoarseMesh {d : ℕ} [NeZero d] {m : ℤ} {hn : ℕ → ℕ} {s : ℤ} {C : Set (HCPolySupport.TriadicCube d)} (hC : C ⊆ Whitney.whitneyPartition m hn) {N : Finset (HCPolySupport.TriadicCube d)} (hN : ∀ Q ∈ Whitney.whitneyPartition m hn, (∃ R ∈ C, Whitney.CubeTouch Q R) → Q ∈ N) (hs : ∀ Q ∈ N, s ≤ Q.scale) (p : HCPolySupport.Vec d) {T : Whitney.KuhnCell d} (hT : T ∈ rootCoarseMesh m s) (hTnot : T ∉ commonCoarseMesh N s) : Set.EqOn (competitorVertexData C p) (linearFn p) T.vertexSet

The closed-star consequence: on a root cell outside the window mesh the global vertex datum is ℓ_p at every vertex.

theorem Algsuperdiff.Section3.Provider.Affine.kuhnSlope_competitorVertexData_eq_of_notMem_commonCoarseMesh {d : ℕ} [NeZero d] {m : ℤ} {hn : ℕ → ℕ} {s : ℤ} {C : Set (HCPolySupport.TriadicCube d)} (hC : C ⊆ Whitney.whitneyPartition m hn) {N : Finset (HCPolySupport.TriadicCube d)} (hN : ∀ Q ∈ Whitney.whitneyPartition m hn, (∃ R ∈ C, Whitney.CubeTouch Q R) → Q ∈ N) (hs : ∀ Q ∈ N, s ≤ Q.scale) (p : HCPolySupport.Vec d) {T : Whitney.KuhnCell d} (hT : T ∈ rootCoarseMesh m s) (hTnot : T ∉ commonCoarseMesh N s) : kuhnSlope T (competitorVertexData C p) = p

theorem Algsuperdiff.Section3.Provider.Affine.globalCompetitor_eqOn_linearFn_closedCarrier_of_notMem_commonCoarseMesh {d : ℕ} [NeZero d] {m : ℤ} {hn : ℕ → ℕ} {s : ℤ} (hsm : s ≤ m) {C : Set (HCPolySupport.TriadicCube d)} (hC : C ⊆ Whitney.whitneyPartition m hn) {N : Finset (HCPolySupport.TriadicCube d)} (hN : ∀ Q ∈ Whitney.whitneyPartition m hn, (∃ R ∈ C, Whitney.CubeTouch Q R) → Q ∈ N) (hs : ∀ Q ∈ N, s ≤ Q.scale) (p : HCPolySupport.Vec d) {T : Whitney.KuhnCell d} (hT : T ∈ rootCoarseMesh m s) (hTnot : T ∉ commonCoarseMesh N s) : Set.EqOn (globalCompetitor m s C p) (linearFn p) T.closedCarrier

theorem Algsuperdiff.Section3.Provider.Affine.notMem_commonCoarseMesh_of_mem_cubeSet {d : ℕ} {m : ℤ} {hn : ℕ → ℕ} {s : ℤ} {N : Finset (HCPolySupport.TriadicCube d)} (hNsub : ∀ Q ∈ N, Q ∈ Whitney.whitneyPartition m hn) (hs : ∀ Q ∈ N, s ≤ Q.scale) {R : HCPolySupport.TriadicCube d} (hR : R ∈ Whitney.whitneyPartition m hn) (hRnot : R ∉ N) {T : Whitney.KuhnCell d} {x : HCPolySupport.Vec d} (hxR : x ∈ HCPolySupport.cubeSet R) (hxT : x ∈ HCPolySupport.cubeSet T.supportCube) : T ∉ commonCoarseMesh N s

A root cell meeting a Whitney cube outside the window is outside the window mesh.

Continuity

theorem Algsuperdiff.Section3.Provider.Affine.continuousOn_globalCompetitor {d : ℕ} {m s : ℤ} (hsm : s ≤ m) (C : Set (HCPolySupport.TriadicCube d)) (p : HCPolySupport.Vec d) : ContinuousOn (globalCompetitor m s C p) (HCPolySupport.cubeSet (HCPolySupport.originCube d m))

"this extension is well-defined and continuous" for the global competitor, on the whole root cube.

Subordination to SW(□_m)

theorem Algsuperdiff.Section3.Provider.Affine.simplexScale_succ_le (m : ℤ) {hn : ℕ → ℕ} {j : ℕ} (hstep' : hn (j + 1) ≤ hn (j + 2) + 1) : Whitney.simplexScale m hn (j + 1) ≤ Whitney.simplexScale m hn j

theorem Algsuperdiff.Section3.Provider.Affine.simplexScale_le_self (m : ℤ) (hn : ℕ → ℕ) (j : ℕ) : Whitney.simplexScale m hn j ≤ m

theorem Algsuperdiff.Section3.Provider.Affine.simplexScale_le_scale_of_mem_window {d : ℕ} {m : ℤ} {hn : ℕ → ℕ} {j : ℕ} (hstep : ∀ (n : ℕ), hn n ≤ hn (n + 1) + 1) {N : Finset (HCPolySupport.TriadicCube d)} (hNsub : ∀ Q ∈ N, Q ∈ Whitney.whitneyPartition m hn) (hNlayer : ∀ Q ∈ N, ∀ (n : ℕ), Q ∈ Whitney.whitneyLayer m hn n → n = j ∨ n = j + 1) (Q : HCPolySupport.TriadicCube d) : Q ∈ N → Whitney.simplexScale m hn j ≤ Q.scale

The window sits at scale at least the common coarse scale.

theorem Algsuperdiff.Section3.Provider.Affine.exists_rootCell_openCarrier_subset {d : ℕ} {m : ℤ} {hn : ℕ → ℕ} {j n : ℕ} (hstep : ∀ (k : ℕ), hn k ≤ hn (k + 1) + 1) (hns : Whitney.simplexScale m hn n ≤ Whitney.simplexScale m hn j) {Q : HCPolySupport.TriadicCube d} (hQ : Q ∈ Whitney.whitneyLayer m hn n) {T : Whitney.KuhnCell d} (hT : T ∈ Whitney.whitneySimplexCells m hn n Q) : ∃ U ∈ rootCoarseMesh m (Whitney.simplexScale m hn j), T.openCarrier ⊆ U.openCarrier

The subordination step: a final e.SW.def cell whose simplex scale is not coarser than the common scale sits inside a single root cell.

The sum_of_a_decomp binder shapes

noncomputable def Algsuperdiff.Section3.Provider.Affine.globalCompetitorCellSlope {d : ℕ} (m s : ℤ) (C : Set (HCPolySupport.TriadicCube d)) (p : HCPolySupport.Vec d) (T : Whitney.KuhnCell d) : HCPolySupport.Vec d

The cell constant of ∇ℓ̂_p on a cell of SW(□_m).

Equations

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

theorem Algsuperdiff.Section3.Provider.Affine.globalCompetitorSlope_eq_cellSlope {d : ℕ} [NeZero d] {m : ℤ} {hn : ℕ → ℕ} {j : ℕ} (hstep : ∀ (k : ℕ), hn k ≤ hn (k + 1) + 1) (hstep' : hn (j + 1) ≤ hn (j + 2) + 1) {C : Set (HCPolySupport.TriadicCube d)} (hC : C ⊆ Whitney.whitneyPartition m hn) {N : Finset (HCPolySupport.TriadicCube d)} (hNmem : ∀ (Q : HCPolySupport.TriadicCube d), Q ∈ N ↔ Q ∈ Whitney.whitneyNeighborhood m hn C) (hNlayer : ∀ Q ∈ N, ∀ (n : ℕ), Q ∈ Whitney.whitneyLayer m hn n → n = j ∨ n = j + 1) (p : HCPolySupport.Vec d) {T : Whitney.KuhnCell d} (hT : T ∈ Whitney.simplexPartition m hn) : (∀ x ∈ T.openCarrier, globalCompetitorSlope m (Whitney.simplexScale m hn j) C p x = globalCompetitorCellSlope m (Whitney.simplexScale m hn j) C p T) ∧ (Multiscale.whitneyCubeOf m hn T ∈ C → globalCompetitorCellSlope m (Whitney.simplexScale m hn j) C p T = 0) ∧ (Multiscale.whitneyCubeOf m hn T ∉ Whitney.whitneyNeighborhood m hn C → globalCompetitorCellSlope m (Whitney.simplexScale m hn j) C p T = p)

The three sum_of_a_decomp clauses at one cell of SW(□_m). The gradient field of the global competitor is constant on the open cell (hFc/hGc), the constant is 0 when the cell's Whitney cube is bad (clause 1) and it is p when the cell's Whitney cube lies off the neighborhood 𝒩(C) (clause 3).