Completeness after pruning local weights #
The cumulative atoms at a node form a subset of all local atoms. Hence their mass loss is at most the global retained mass loss. This connects the gap-pruning estimate to the thickness estimate at every old large node.
theorem
EGZ.FlagDecompositionRaw.natMass_cumulativeWeight
{p d : ℕ}
[NeZero p]
{F : ConvexFlag}
(pieces : F.Node → FpCoord p d → ℕ)
(x : F.Node)
:
Cumulative mass is the mass of the local atoms based below the node.
theorem
EGZ.FlagDecompositionRaw.cumulativeWeight_mass_loss_le
{p d : ℕ}
[NeZero p]
{F : ConvexFlag}
{pieces pieces' : F.Node → FpCoord p d → ℕ}
(hle : ∀ (x : F.Node) (v : FpCoord p d), pieces' x v ≤ pieces x v)
(x : F.Node)
:
natMass (cumulativeWeight pieces x) - natMass (cumulativeWeight pieces' x) ≤ natMass (retainedWeight pieces) - natMass (retainedWeight pieces')
Loss from a cumulative weight is bounded by loss from all local atoms.
theorem
EGZ.FlagDecompositionRaw.cumulativeWeight_mass_loss_le_real
{p d : ℕ}
[NeZero p]
{F : ConvexFlag}
{pieces pieces' : F.Node → FpCoord p d → ℕ}
(hle : ∀ (x : F.Node) (v : FpCoord p d), pieces' x v ≤ pieces x v)
(x : F.Node)
:
↑(natMass (cumulativeWeight pieces x)) - ↑(natMass (cumulativeWeight pieces' x)) ≤ ↑(natMass (retainedWeight pieces)) - ↑(natMass (retainedWeight pieces'))
Real-valued form of the cumulative mass-loss bound, ready for relative loss estimates.
theorem
EGZ.FlagDecomposition.cumulativeWeight_thick_of_pruning
{p d : ℕ}
[NeZero p]
{f : FpCoord p d → ℕ}
(Φ : FlagDecomposition p d f)
(hp : Odd p)
{pieces : Φ.flag.Node → FpCoord p d → ℕ}
{x : Φ.flag.Node}
{t : ℕ}
{δ α ε : ℝ}
{ξ : FpCoord p d →ᵃ[ZMod p] ZMod p}
(hthick : IsThickAlong (Φ.cumulativeWeight x) ξ t δ)
(hle : ∀ (y : Φ.flag.Node) (v : FpCoord p d), pieces y v ≤ Φ.localWeight y v)
(hε : 0 < ε)
(hα : 0 ≤ α)
(hlarge : Φ.IsLargeElement ε x)
(hloss : ↑Φ.retainedMass - ↑(natMass (FlagDecompositionRaw.retainedWeight pieces)) ≤ α * ↑Φ.retainedMass)
(hδ : 0 ≤ δ - α / ε)
:
IsThickAlong (FlagDecompositionRaw.cumulativeWeight pieces x) ξ t (δ - α / ε)
Pruning at most α of the original retained mass preserves thickness
at an old ε-large node, with deterioration at most α / ε.
theorem
EGZ.FlagDecomposition.IsCompleteElement.thick_of_pruning
{p d : ℕ}
[NeZero p]
{f : FpCoord p d → ℕ}
{Φ : FlagDecomposition p d f}
{x : Φ.flag.Node}
{t : ℕ}
{δ α ε : ℝ}
(hcomplete : Φ.IsCompleteElement x t δ)
(hp : Odd p)
{pieces : Φ.flag.Node → FpCoord p d → ℕ}
(hle : ∀ (y : Φ.flag.Node) (v : FpCoord p d), pieces y v ≤ Φ.localWeight y v)
(hε : 0 < ε)
(hα : 0 ≤ α)
(hlarge : Φ.IsLargeElement ε x)
(hloss : ↑Φ.retainedMass - ↑(natMass (FlagDecompositionRaw.retainedWeight pieces)) ≤ α * ↑Φ.retainedMass)
(hδ : 0 ≤ δ - α / ε)
(ξ : FpCoord p d →ᵃ[ZMod p] ZMod p)
(hξ : Φ.representation.NonconstantOnFibers x ξ)
:
IsThickAlong (FlagDecompositionRaw.cumulativeWeight pieces x) ξ t (δ - α / ε)
Every functional required for completeness remains thick after the same global pruning, before the surviving flag is repackaged.