Coarse-graining support: Support.Book.Ch04.SourceEllipticity

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Deterministic ellipticity slices for the exact coarse source

Every coarse-source carrier field is locally uniformly elliptic on source Euclidean balls. This file converts that carrier membership fact into the countable AEE ellipticity slices used on a fixed triadic cube without invoking any probabilistic assumptions.

theorem HCPolySupport.Book.Ch04.exists_source_isAEEllipticFieldOn_cubeSet {d : ℕ} (a : Source.Coarse.Carrier d) (Q : TriadicCube d) : ∃ (ε : ℝ), 0 < ε ∧ ε ≤ 1 ∧ IsAEEllipticFieldOn ε ε⁻¹ (cubeSet Q) ↑a

A coarse-source carrier field has positive a.e. ellipticity constants on every triadic cube. The only inputs are its coordinate measurability and its pointwise source-ball ellipticity from carrier membership.

theorem HCPolySupport.Book.Ch04.exists_source_aeeQuantitativeEllipticSlice_cubeSet {d : ℕ} (a : Source.Coarse.Carrier d) (Q : TriadicCube d) : ∃ (k : ℕ), AEEQuantitativeEllipticSlice (cubeSet Q) k ↑a

Every coarse-source carrier field belongs to a countable AEE ellipticity slice on every triadic cube.