SimplexDissection

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

A triadic Whitney dissection of the open Kuhn simplex

The identified route needs, as its first ingredient,

a triadic Whitney decomposition of the open simplex into countably many pairwise disjoint triadic cubes filling it up to a Lebesgue-null set.

That decomposition is what this file provides. Nothing about the response functional appears here; the analytic half (the boundary-count summability and the subadditivity assembly) is SimplexResponseBound.lean.

Contents

• the open Kuhn simplex as a Chapter 2 domain (simplexDomain), through its openness, convexity, boundedness and an explicit interior ball (ball_simplexIncenter_subset_openCarrier) around the equally spaced incenter of the ordered simplex;
• the Whitney selection whitneyInnerCubes U Q of an arbitrary set U inside a triadic cube Q: the triadic descendants of Q whose half-open realization lies in U while their triadic parent's does not — i.e. the maximal inner triadic cubes;
• its three defining properties: the selected cubes lie in U (cubeSet_subset_of_mem_whitneyInnerCubes), they are pairwise disjoint (pairwiseDisjoint_whitneyInnerCubes), and for U open they cover U (subset_iUnion_whitneyInnerCubes);
• the specialization to the open Kuhn simplex (simplexDissection), including the covering up to a null set in the open cube realizations that the Chapter 2 domain interface needs (volume_openCarrier_diff_iUnion_eq_zero).

Reading notes

• The selection is by triadic maximality, not by the usual comparison of side length with the distance to the boundary; the two agree up to a bounded number of generations, and maximality is what the disjointness proof and the boundary bound of SimplexResponseBound.lean actually use. The maximality clause is stated through parentCube, which is the triadic parent by Homogenization.childCube_parent.
• No Mathlib covering theorem (MeasureTheory.Covering.*, Vitali) is used: those produce almost-covering subfamilies of a given fine family with Besicovitch/Vitali structure, whereas what is needed here is the exact maximal-triadic-cube selection, whose disjointness and covering come from the triadic hierarchy of Homogenization.Geometry.TriadicPartition directly.

References

• ABK26, e.simplex.def, p.bfA.multiscalebound, Step 1.

The open Kuhn simplex is open, convex and bounded

The incenter and the interior ball

noncomputable def Algsuperdiff.Section3.Provider.Multiscale.simplexInradius {d : ℕ} (T : Whitney.KuhnCell d) : ℝ

An inner radius of a Kuhn cell in the sup metric: 3^{scale} / (2 (d+1)).

Equations

• Algsuperdiff.Section3.Provider.Multiscale.simplexInradius T = HCPolySupport.cubeScaleFactor T.supportCube / (2 * (↑d + 1))

theorem Algsuperdiff.Section3.Provider.Multiscale.simplexInradius_pos {d : ℕ} (T : Whitney.KuhnCell d) : 0 < simplexInradius T

noncomputable def Algsuperdiff.Section3.Provider.Multiscale.simplexIncenter {d : ℕ} (T : Whitney.KuhnCell d) : HCPolySupport.Vec d

The incenter of a Kuhn cell: the point of the ordered simplex whose local coordinates are equally spaced, 3^{scale} (k+1)/(d+1) - 3^{scale}/2 at the coordinate of rank k in the cell's order.

Equations

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

theorem Algsuperdiff.Section3.Provider.Multiscale.ball_simplexIncenter_subset_openCarrier {d : ℕ} (T : Whitney.KuhnCell d) : Metric.ball (simplexIncenter T) (simplexInradius T) ⊆ T.openCarrier

The interior ball of a Kuhn cell. The open sup-ball of radius 3^{scale}/(2(d+1)) around the equally spaced incenter is contained in the open simplex. Both the radius and the center are explicit; only positivity of the radius and this inclusion are used downstream.

theorem Algsuperdiff.Section3.Provider.Multiscale.simplexIncenter_mem_openCarrier {d : ℕ} (T : Whitney.KuhnCell d) : simplexIncenter T ∈ T.openCarrier

def Algsuperdiff.Section3.Provider.Multiscale.simplexDomain {d : ℕ} (T : Whitney.KuhnCell d) : HCPolySupport.Book.Ch02.Domain d

The open Kuhn simplex as a Chapter 2 domain. This is the carrier at which ABK26 applies the crude response bounds/6348.

Equations

• Algsuperdiff.Section3.Provider.Multiscale.simplexDomain T = { carrier := T.openCarrier, isDomain := ⋯, nonempty := ⋯ }

@[simp]

theorem Algsuperdiff.Section3.Provider.Multiscale.simplexDomain_coe {d : ℕ} (T : Whitney.KuhnCell d) : (simplexDomain T).carrier = T.openCarrier

The maximal inner triadic cubes of a set

def Algsuperdiff.Section3.Provider.Multiscale.whitneyInnerCubes {d : ℕ} (U : Set (HCPolySupport.Vec d)) (Q : HCPolySupport.TriadicCube d) : Set (HCPolySupport.TriadicCube d)

The triadic Whitney selection. The triadic descendants R of Q whose half-open realization is contained in U but whose triadic parent's is not: the maximal inner triadic cubes of U below Q.

Equations

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

theorem Algsuperdiff.Section3.Provider.Multiscale.cubeSet_subset_of_mem_whitneyInnerCubes {d : ℕ} {U : Set (HCPolySupport.Vec d)} {Q R : HCPolySupport.TriadicCube d} (hR : R ∈ whitneyInnerCubes U Q) : HCPolySupport.cubeSet R ⊆ U

theorem Algsuperdiff.Section3.Provider.Multiscale.exists_depth_of_mem_whitneyInnerCubes {d : ℕ} {U : Set (HCPolySupport.Vec d)} {Q R : HCPolySupport.TriadicCube d} (hR : R ∈ whitneyInnerCubes U Q) : ∃ (t : ℕ), R ∈ HCPolySupport.descendantsAtDepth Q t

theorem Algsuperdiff.Section3.Provider.Multiscale.one_le_depth_of_mem_whitneyInnerCubes {d : ℕ} {U : Set (HCPolySupport.Vec d)} {Q R : HCPolySupport.TriadicCube d} (hQ : ¬HCPolySupport.cubeSet Q ⊆ U) (hR : R ∈ whitneyInnerCubes U Q) {t : ℕ} (ht : R ∈ HCPolySupport.descendantsAtDepth Q t) : 1 ≤ t

A selected cube is a strict descendant: its own realization is inside U while Q's is not, so the selection depth is at least one.

theorem Algsuperdiff.Section3.Provider.Multiscale.pairwiseDisjoint_whitneyInnerCubes {d : ℕ} (U : Set (HCPolySupport.Vec d)) (Q : HCPolySupport.TriadicCube d) : (whitneyInnerCubes U Q).PairwiseDisjoint HCPolySupport.cubeSet

The selected cubes are pairwise disjoint. Two distinct maximal inner cubes cannot be nested: the deeper one's parent would then already be an inner cube.

theorem Algsuperdiff.Section3.Provider.Multiscale.subset_iUnion_whitneyInnerCubes {d : ℕ} {U : Set (HCPolySupport.Vec d)} {Q : HCPolySupport.TriadicCube d} (hopen : IsOpen U) (hUQ : U ⊆ HCPolySupport.cubeSet Q) (hQU : ¬HCPolySupport.cubeSet Q ⊆ U) : U ⊆ ⋃ R ∈ whitneyInnerCubes U Q, HCPolySupport.cubeSet R

The selected cubes cover an open set. For U open with U ⊆ cubeSet Q and cubeSet Q ⊄ U, every point of U lies in a maximal inner cube: take the shallowest triadic cube of the point whose realization already lies in U.

The dissection of an open Kuhn simplex

theorem Algsuperdiff.Section3.Provider.Multiscale.not_cubeSet_supportCube_subset_openCarrier {d : ℕ} [NeZero d] (T : Whitney.KuhnCell d) : ¬HCPolySupport.cubeSet T.supportCube ⊆ T.openCarrier

The realization of a Kuhn cell is not all of its support cube: the lower corner of the half-open cube is not even in the open cube.

def Algsuperdiff.Section3.Provider.Multiscale.simplexDissection {d : ℕ} (T : Whitney.KuhnCell d) : Set (HCPolySupport.TriadicCube d)

The triadic Whitney dissection of an open Kuhn simplex (the geometric ingredient of the identified route): the maximal inner triadic cubes of the open simplex below its support cube.

Equations

• Algsuperdiff.Section3.Provider.Multiscale.simplexDissection T = Algsuperdiff.Section3.Provider.Multiscale.whitneyInnerCubes T.openCarrier T.supportCube

theorem Algsuperdiff.Section3.Provider.Multiscale.cubeSet_subset_openCarrier_of_mem_simplexDissection {d : ℕ} {T : Whitney.KuhnCell d} {R : HCPolySupport.TriadicCube d} (hR : R ∈ simplexDissection T) : HCPolySupport.cubeSet R ⊆ T.openCarrier

theorem Algsuperdiff.Section3.Provider.Multiscale.openCubeSet_subset_openCarrier_of_mem_simplexDissection {d : ℕ} {T : Whitney.KuhnCell d} {R : HCPolySupport.TriadicCube d} (hR : R ∈ simplexDissection T) : HCPolySupport.openCubeSet R ⊆ T.openCarrier

theorem Algsuperdiff.Section3.Provider.Multiscale.pairwiseDisjoint_simplexDissection {d : ℕ} (T : Whitney.KuhnCell d) : (simplexDissection T).PairwiseDisjoint HCPolySupport.cubeSet

theorem Algsuperdiff.Section3.Provider.Multiscale.pairwiseDisjoint_openCubeSet_simplexDissection {d : ℕ} (T : Whitney.KuhnCell d) : (simplexDissection T).PairwiseDisjoint HCPolySupport.openCubeSet

theorem Algsuperdiff.Section3.Provider.Multiscale.openCarrier_subset_iUnion_simplexDissection {d : ℕ} [NeZero d] (T : Whitney.KuhnCell d) : T.openCarrier ⊆ ⋃ R ∈ simplexDissection T, HCPolySupport.cubeSet R

The dissection fills the simplex (half-open realizations).

theorem Algsuperdiff.Section3.Provider.Multiscale.volume_openCarrier_diff_iUnion_eq_zero {d : ℕ} [NeZero d] (T : Whitney.KuhnCell d) : MeasureTheory.volume (T.openCarrier \ ⋃ (R : ↑(simplexDissection T)), HCPolySupport.openCubeSet ↑R) = 0

The dissection fills the simplex up to a null set in the open cube realizations, which are the Chapter 2 domains of the subadditivity interface.