SimplexDomains

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

The cells of SW(□_m) as Chapter 2 domains

This module is the measure-theoretic layer that the proved simplex partition d.simplex.partition (Provider/Whitney/SimplexPartition.lean) explicitly leaves open, and that the subadditive decomposition of p.bfA.multiscalebound (e.sum-of-a-decomp) needs in order to feed SW(□_m) to l.subadd.betterer (Provider/Whitney/SubadditivityCountable.lean):

• the manuscript's open simplex △_n^π(z) (KuhnCell.openCarrier) is a nonempty bounded open convex set, hence a Homogenization.Book.Ch02.Domain (KuhnCell.domain);
• KuhnCell d is countable, so SW(□_m) is a countable family (instCountableKuhnCell);
• the canonical half-open realization differs from the open one by a Lebesgue null set (volume_carrier_diff_openCarrier), because the half-open cell is contained in the closure of the open one and an open convex set has null frontier;
• consequently the open cells of SW(□_m) cover the open root cube up to a null set (volume_openCubeSet_diff_iUnion_openCarrier), which is exactly the hcover hypothesis of Whitney.ofReal_bfA_quadratic_le_simplex_weighted_tsum.

Why the open realization

l.subadd.betterer is stated for a family of Ch02.Domains — open bounded convex nonempty sets — because the variational class L²_pot,0(U) × L²_sol,0(U) of e.variational.mu.U.P is only defined there. The manuscript's simplices are open, and the exact half-open partition of SimplexPartition.lean is the bookkeeping device that makes the covering statement exact; the passage between them is the null-boundary fact proved here. No face-to-face or simplicial-complex property is used or asserted.

References

• ABK26, (e.simplex.def), (e.SW.def).

Countability

instance Algsuperdiff.Section3.Provider.Multiscale.instCountableKuhnCell (d : ℕ) : Countable (Whitney.KuhnCell d)

KuhnCell d is countable: a cell is a triadic cube together with a permutation of Fin d.

The open cell is a Chapter 2 domain

theorem Algsuperdiff.Section3.Provider.Multiscale.isOpen_openCarrier {d : ℕ} (T : Whitney.KuhnCell d) : IsOpen T.openCarrier

theorem Algsuperdiff.Section3.Provider.Multiscale.convex_openCarrier {d : ℕ} (T : Whitney.KuhnCell d) : Convex ℝ T.openCarrier

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

The barycentric-type interior point of a Kuhn cell: the k-th coordinate is placed at height (rank(k) + 1)/(d + 1) of the support cube, where rank is the position of k in the cell's order.

Equations

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

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

theorem Algsuperdiff.Section3.Provider.Multiscale.openCarrier_nonempty {d : ℕ} (T : Whitney.KuhnCell d) : T.openCarrier.Nonempty

theorem Algsuperdiff.Section3.Provider.Multiscale.isBoundedDomain_openCarrier {d : ℕ} (T : Whitney.KuhnCell d) : HCPolySupport.IsBoundedDomain T.openCarrier

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

The open simplex △ as a Chapter 2 domain. This is the carrier at which l.subadd.betterer reads the cells of SW(□_m).

Equations

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

The half-open cell exceeds the open one by a null set

theorem Algsuperdiff.Section3.Provider.Multiscale.carrier_subset_closure_openCarrier {d : ℕ} (T : Whitney.KuhnCell d) : T.carrier ⊆ closure T.openCarrier

The half-open cell is contained in the closure of the open one: sliding a point of the half-open cell towards the interior point makes every weak inequality strict.

theorem Algsuperdiff.Section3.Provider.Multiscale.volume_carrier_diff_openCarrier {d : ℕ} (T : Whitney.KuhnCell d) : MeasureTheory.volume (T.carrier \ T.openCarrier) = 0

The open cells cover the root cube up to a null set

theorem Algsuperdiff.Section3.Provider.Multiscale.volume_openCubeSet_diff_iUnion_openCarrier {d : ℕ} [NeZero d] {m : ℤ} {hn : ℕ → ℕ} (hstep : ∀ (n : ℕ), hn n ≤ hn (n + 1) + 1) : MeasureTheory.volume (HCPolySupport.openCubeSet (HCPolySupport.originCube d m) \ ⋃ T ∈ Whitney.simplexPartition m hn, T.openCarrier) = 0

The hcover input of l.subadd.betterer at SW(□_m). The open cells of the simplex partition exhaust the open root cube up to a Lebesgue null set: the half-open cells exhaust it exactly (iUnion_carrier_simplexPartition_eq_openCubeSet) and each half-open cell exceeds its open cell by a null set.