Stability of decomposition completeness #
These monotonicity and mass identities are used when normalizing epsilon, choosing the final uniform delta, and transferring thickness through cleanup.
theorem
EGZ.FlagDecomposition.liftedMassOn_polytope
{p d : ℕ}
[NeZero p]
{f : FpCoord p d → ℕ}
(hp : Odd p)
(Φ : FlagDecomposition p d f)
(x : Φ.flag.Node)
:
Total lifted mass at a node is its cumulative finite-field mass.
theorem
EGZ.FlagDecomposition.isLargeElement_iff_natMass
{p d : ℕ}
[NeZero p]
{f : FpCoord p d → ℕ}
(hp : Odd p)
(Φ : FlagDecomposition p d f)
(ε : ℝ)
(x : Φ.flag.Node)
:
theorem
EGZ.FlagDecomposition.IsLargeElement.mono_epsilon
{p d : ℕ}
[NeZero p]
{f : FpCoord p d → ℕ}
{Φ : FlagDecomposition p d f}
{ε ε' : ℝ}
{x : Φ.flag.Node}
(h : Φ.IsLargeElement ε x)
(hε : ε' ≤ ε)
:
Φ.IsLargeElement ε' x
theorem
EGZ.FlagDecomposition.IsLargeFace.mono_epsilon
{p d : ℕ}
[NeZero p]
{f : FpCoord p d → ℕ}
{Φ : FlagDecomposition p d f}
{ε ε' : ℝ}
{x : Φ.flag.Node}
{Γ : (Φ.flag.polytope x).Face}
(h : Φ.IsLargeFace ε x Γ)
(hε : ε' ≤ ε)
:
Φ.IsLargeFace ε' x Γ
theorem
EGZ.FlagDecomposition.IsCompleteElement.mono_delta
{p d : ℕ}
[NeZero p]
{f : FpCoord p d → ℕ}
{Φ : FlagDecomposition p d f}
{x : Φ.flag.Node}
{t : ℕ}
{δ δ' : ℝ}
(h : Φ.IsCompleteElement x t δ)
(hδ : δ' ≤ δ)
:
Φ.IsCompleteElement x t δ'
theorem
EGZ.FlagDecomposition.IsComplete.mono_epsilon
{p d : ℕ}
[NeZero p]
{f : FpCoord p d → ℕ}
{Φ : FlagDecomposition p d f}
{T : Φ.flag.Node → ℕ}
{ε ε' δ : ℝ}
(h : Φ.IsComplete T ε δ)
(hε : ε ≤ ε')
:
Φ.IsComplete T ε' δ
Increasing epsilon asks for completeness and realization at fewer nodes and faces.
theorem
EGZ.FlagDecomposition.IsComplete.mono_delta
{p d : ℕ}
[NeZero p]
{f : FpCoord p d → ℕ}
{Φ : FlagDecomposition p d f}
{T : Φ.flag.Node → ℕ}
{ε δ δ' : ℝ}
(h : Φ.IsComplete T ε δ)
(hδ : δ' ≤ δ)
:
Φ.IsComplete T ε δ'