Geometric gap cleanup

Surviving local weights first give a flag of their nonempty cumulative support hulls. Restricting that flag to reduced nodes finishes the geometric cleanup. The construction retains exactly the mass supplied by numerical pruning.

theorem EGZ.FlagDecomposition.cumulativeMass_pos {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (hp : Odd p) (x : Φ.flag.Node) : 0 < natMass (Φ.cumulativeWeight x)

theorem EGZ.FlagDecomposition.retainedMass_pos {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (hp : Odd p) : 0 < Φ.retainedMass

Every decomposition has positive retained mass: its top lifted support is nonempty and all its stored masses are positive.

theorem EGZ.FlagDecomposition.PrunedWeights.rebuildData {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} (D : Φ.PrunedWeights) (hp : Odd p) : FlagDecompositionRaw.RebuildData Φ.representation D.weight f

The old support polytopes supply all compatibility conditions for the rebuilding construction; none is an additional geometric assumption.

@[reducible, inline]

noncomputable abbrev EGZ.FlagDecomposition.PrunedWeights.rebuilt {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} (D : Φ.PrunedWeights) (hp : Odd p) : FlagDecomposition p d f

Rebuild the flag decomposition from the pruned weights.

Equations

• D.rebuilt hp = ⋯.decomposition

@[reducible, inline]

noncomputable abbrev EGZ.FlagDecomposition.PrunedWeights.cleaned {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} (D : Φ.PrunedWeights) (hp : Odd p) : FlagDecomposition p d f

Reduced decomposition obtained after rebuilding the pruned weights.

Equations

• D.cleaned hp = (D.rebuilt hp).reduced hp

theorem EGZ.FlagDecomposition.PrunedWeights.rebuilt_polytope_subset {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} (D : Φ.PrunedWeights) (hp : Odd p) (x : (D.rebuilt hp).flag.Node) : ((D.rebuilt hp).flag.polytope x).carrier ⊆ (Φ.flag.polytope ↑x).carrier

@[simp]

theorem EGZ.FlagDecomposition.PrunedWeights.cleaned_localWeight {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} (D : Φ.PrunedWeights) (hp : Odd p) (x : (D.cleaned hp).flag.Node) : (D.cleaned hp).localWeight x = D.weight ↑↑x

theorem EGZ.FlagDecomposition.PrunedWeights.cleaned_cumulativeWeight {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} (D : Φ.PrunedWeights) (hp : Odd p) (x : (D.cleaned hp).flag.Node) : (D.cleaned hp).cumulativeWeight x = D.cumulative ↑↑x

theorem EGZ.FlagDecomposition.PrunedWeights.cleaned_hat {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} (D : Φ.PrunedWeights) (hp : Odd p) (x : (D.cleaned hp).flag.Node) : (D.cleaned hp).hat x = D.hat ↑↑x

theorem EGZ.FlagDecomposition.PrunedWeights.cleaned_retainedMass {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} (D : Φ.PrunedWeights) (hp : Odd p) : (D.cleaned hp).retainedMass = natMass (FlagDecompositionRaw.retainedWeight D.weight)

theorem EGZ.FlagDecomposition.PrunedWeights.cleaned_isReduced {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} (D : Φ.PrunedWeights) (hp : Odd p) : (D.cleaned hp).IsReduced

theorem EGZ.FlagDecomposition.PrunedWeights.cleaned_card_le {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} (D : Φ.PrunedWeights) (hp : Odd p) : Fintype.card (D.cleaned hp).flag.Node ≤ Fintype.card Φ.flag.Node

theorem EGZ.FlagDecomposition.PrunedWeights.cleaned_polytope_subset {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} (D : Φ.PrunedWeights) (hp : Odd p) (x : (D.cleaned hp).flag.Node) : ((D.cleaned hp).flag.polytope x).carrier ⊆ (Φ.flag.polytope ↑↑x).carrier

theorem EGZ.FlagDecomposition.PrunedWeights.cleaned_isKBounded {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} (D : Φ.PrunedWeights) (hp : Odd p) {K : Φ.flag.Node → ℕ} (hK : Φ.IsKBounded K) : (D.cleaned hp).IsKBounded fun (x : (D.cleaned hp).flag.Node) => K ↑↑x

noncomputable def EGZ.FlagDecomposition.PrunedWeights.rebuiltSubdivisionMap {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} (D : Φ.PrunedWeights) (hp : Odd p) : Φ.SubdivisionMap (D.rebuilt hp)

Subdivision map from the rebuilt decomposition to the original one.

Equations

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

noncomputable def EGZ.FlagDecomposition.PrunedWeights.cleanedSubdivisionMap {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} (D : Φ.PrunedWeights) (hp : Odd p) : Φ.SubdivisionMap (D.cleaned hp)

Subdivision map from the cleaned decomposition to the original one.

Equations

• D.cleanedSubdivisionMap hp = (D.rebuiltSubdivisionMap hp).comp ((D.rebuilt hp).reducedSubdivisionMap hp)

theorem EGZ.FlagDecomposition.PrunedWeights.cleaned_isRealizedFace {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} (D : Φ.PrunedWeights) (hp : Odd p) (x : (D.cleaned hp).flag.Node) (Γ : (Φ.flag.polytope ↑↑x).Face) (hne : (((D.cleaned hp).flag.polytope x).carrier ∩ Γ.carrier).Nonempty) (hΓ : Φ.IsRealizedFace (↑↑x) Γ) : (D.cleaned hp).IsRealizedFace x ((D.cleanedSubdivisionMap hp).face x Γ hne)

A realized old face remains realized on its nonempty intersection with the cleaned polytope. Its new index is allowed to move downwards.

theorem EGZ.FlagDecomposition.PrunedWeights.cleaned_isCompleteElement {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} (D : Φ.PrunedWeights) (hp : Odd p) {x : (D.cleaned hp).flag.Node} {t : ℕ} {ε δ α : ℝ} (hε : 0 < ε) (hα : 0 ≤ α) (hlarge : Φ.IsLargeElement ε ↑↑x) (hcomplete : Φ.IsCompleteElement (↑↑x) t δ) (hloss : ↑Φ.retainedMass - ↑(D.cleaned hp).retainedMass ≤ α * ↑Φ.retainedMass) : (D.cleaned hp).IsCompleteElement x t (δ - α / ε)

The cleanup thickness bound holds for every resulting parameter, including negative ones, since every retained cumulative weight is nonzero.

theorem EGZ.FlagDecomposition.PrunedWeights.cleaned_gap_gt {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} (D : Φ.PrunedWeights) (hp : Odd p) (threshold : Φ.flag.Node → ℝ) (hgap : ∀ (x : Φ.flag.Node) (q : IntCoord (Φ.flag.rank x)), D.hat x q ≠ 0 → threshold x < ↑(D.hat x q)) (x : (D.cleaned hp).flag.Node) : threshold ↑↑x < ↑((D.cleaned hp).gap x)

theorem EGZ.FlagDecomposition.gap_cleanup_lemma {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} [Fact (Nat.Prime p)] (Φ : FlagDecomposition p d f) (hp : Odd p) {K : Φ.flag.Node → ℕ} (hK : Φ.IsKBounded K) {α : ℝ} (hα : 0 ≤ α) (hαone : α < 1) : ∃ (D : Φ.PrunedWeights), (∀ (x : Φ.flag.Node) (v : FpCoord p d), D.weight x v = 0 ∨ D.weight x v = Φ.localWeight x v) ∧ (D.cleaned hp).IsReduced ∧ ((D.cleaned hp).IsKBounded fun (x : (D.cleaned hp).flag.Node) => K ↑↑x) ∧ (∀ (x : (D.cleaned hp).flag.Node), α * ↑Φ.retainedMass / (↑(Fintype.card Φ.flag.Node) * (2 * ↑(K ↑↑x) + 1) ^ d) ≤ ↑((D.cleaned hp).gap x)) ∧ (1 - α) * ↑Φ.retainedMass ≤ ↑(D.cleaned hp).retainedMass

Gap cleanup with a rebuilt, reduced output decomposition. All geometric properties of the output (including preservation of realized faces and thickness) are supplied by the PrunedWeights.cleaned_* theorems above. No coordinate-versus-prime bound is needed for this operation.