Surviving weights and their lifted supports

The support lemmas here prepare the geometric rebuilding after numerical pruning. A surviving collection is pointwise below the old local weights and has at least one nonzero atom.

structure EGZ.FlagDecomposition.PrunedWeights {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) : Type

A nonzero family of local weights obtained by decreasing the weights of a flag decomposition.

• weight : Φ.flag.Node → FpCoord p d → ℕ

  The retained local multiplicity at each node and ambient point.

• weight_le (x : Φ.flag.Node) (v : FpCoord p d) : self.weight x v ≤ Φ.localWeight x v
• nonzero : ∃ (x : Φ.flag.Node) (v : FpCoord p d), self.weight x v ≠ 0

@[reducible, inline]

noncomputable abbrev EGZ.FlagDecomposition.PrunedWeights.cumulative {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} (D : Φ.PrunedWeights) (x : Φ.flag.Node) (v : FpCoord p d) : ℕ

The pruned weight accumulated over all nodes below a given node.

Equations

• D.cumulative = EGZ.FlagDecompositionRaw.cumulativeWeight D.weight

@[reducible, inline]

noncomputable abbrev EGZ.FlagDecomposition.PrunedWeights.hat {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} (D : Φ.PrunedWeights) (x : Φ.flag.Node) (q : IntCoord (Φ.flag.rank x)) : ℕ

The centered integral lift of the cumulative pruned weight.

Equations

• D.hat = EGZ.FlagDecompositionRaw.hat Φ.representation D.weight

@[reducible, inline]

noncomputable abbrev EGZ.FlagDecomposition.PrunedWeights.localLift {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} (D : Φ.PrunedWeights) (x : Φ.flag.Node) (q : IntCoord (Φ.flag.rank x)) : ℕ

The centered integral lift of the pruned weight at a single node.

Equations

• D.localLift = EGZ.FlagDecompositionRaw.localLift Φ.representation D.weight

@[reducible, inline]

noncomputable abbrev EGZ.FlagDecomposition.PrunedWeights.support {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} (D : Φ.PrunedWeights) (x : Φ.flag.Node) : Finset (IntCoord (Φ.flag.rank x))

The finite support of the cumulative centered lift of the pruned weights.

Equations

• D.support = EGZ.FlagDecompositionRaw.hatSupport Φ.representation D.weight

theorem EGZ.FlagDecomposition.PrunedWeights.mem_support {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} (D : Φ.PrunedWeights) (x : Φ.flag.Node) (q : IntCoord (Φ.flag.rank x)) : q ∈ D.support x ↔ D.hat x q ≠ 0

theorem EGZ.FlagDecomposition.PrunedWeights.weight_supported {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} (D : Φ.PrunedWeights) (x : Φ.flag.Node) (v : FpCoord p d) (hv : D.weight x v ≠ 0) : v ∈ Φ.representation.space x

theorem EGZ.FlagDecomposition.PrunedWeights.cumulative_ne_zero_iff {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} (D : Φ.PrunedWeights) (x : Φ.flag.Node) (v : FpCoord p d) : D.cumulative x v ≠ 0 ↔ ∃ y ≤ x, D.weight y v ≠ 0

theorem EGZ.FlagDecomposition.PrunedWeights.cumulative_supported {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} (D : Φ.PrunedWeights) (x : Φ.flag.Node) (v : FpCoord p d) (hv : D.cumulative x v ≠ 0) : v ∈ Φ.representation.space x

theorem EGZ.FlagDecomposition.PrunedWeights.cumulative_ne_zero_of_le {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} (D : Φ.PrunedWeights) {y x : Φ.flag.Node} (h : y ≤ x) {v : FpCoord p d} (hv : D.cumulative y v ≠ 0) : D.cumulative x v ≠ 0

theorem EGZ.FlagDecomposition.PrunedWeights.hat_le_old {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} (D : Φ.PrunedWeights) (x : Φ.flag.Node) (q : IntCoord (Φ.flag.rank x)) : D.hat x q ≤ Φ.hat x q

theorem EGZ.FlagDecomposition.PrunedWeights.localLift_le_old {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} (D : Φ.PrunedWeights) (x : Φ.flag.Node) (q : IntCoord (Φ.flag.rank x)) : D.localLift x q ≤ Φ.localLift x q

theorem EGZ.FlagDecomposition.PrunedWeights.mem_old_polytope {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} (D : Φ.PrunedWeights) {x : Φ.flag.Node} {q : IntCoord (Φ.flag.rank x)} (hq : D.hat x q ≠ 0) : q.real ∈ (Φ.flag.polytope x).carrier

theorem EGZ.FlagDecomposition.PrunedWeights.hat_ne_zero_iff {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} (D : Φ.PrunedWeights) (x : Φ.flag.Node) (q : IntCoord (Φ.flag.rank x)) : D.hat x q ≠ 0 ↔ IsCenteredLift p q ∧ ∃ (v : FpCoord p d), (Φ.representation.map x) v = IntCoord.mod p q ∧ D.cumulative x v ≠ 0

theorem EGZ.FlagDecomposition.PrunedWeights.support_nonempty_iff {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} (D : Φ.PrunedWeights) (hp : Odd p) (x : Φ.flag.Node) : (D.support x).Nonempty ↔ ∃ (v : FpCoord p d), D.cumulative x v ≠ 0

theorem EGZ.FlagDecomposition.PrunedWeights.transition_centered {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} (D : Φ.PrunedWeights) {y x : Φ.flag.Node} (h : y ≤ x) {q : IntCoord (Φ.flag.rank y)} (hq : D.hat y q ≠ 0) : IsCenteredLift p ((Φ.flag.transition h).integer q)

Upper transitions of surviving support points remain centered because they lie in the old, bounded upper polytope.

theorem EGZ.FlagDecomposition.PrunedWeights.transition_mem_support {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} (D : Φ.PrunedWeights) {y x : Φ.flag.Node} (h : y ≤ x) {q : IntCoord (Φ.flag.rank y)} (hq : q ∈ D.support y) : (Φ.flag.transition h).integer q ∈ D.support x

theorem EGZ.FlagDecomposition.PrunedWeights.exists_localLift_of_hat_ne_zero {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} (D : Φ.PrunedWeights) (hp : Odd p) (x : Φ.flag.Node) (q : IntCoord (Φ.flag.rank x)) (hq : D.hat x q ≠ 0) : ∃ (y : Φ.flag.Node) (h : y ≤ x) (z : IntCoord (Φ.flag.rank y)), D.localLift y z ≠ 0 ∧ (Φ.flag.transition h).integer z = q

Every surviving cumulative atom comes from a surviving local atom at a lower node. This is the visibility input for the rebuilt support hulls.