From the flag centerpoint to a cumulative fibre

Local ambient atoms are used as a labelled weighted family. Repeated generating points retain their separate masses; the centerpoint theorem does not require the family to be injective. Compatibility and centered integer transitions identify its upper masses with cumulative lifted mass.

theorem EGZ.ConvexFlag.flagCenterpoint_fintype {F : ConvexFlag} (Ω : F.ProperPointSet) {I : Type u_1} [Fintype I] (points : I → F.Point) (hproper : ∀ (i : I), points i ∈ Ω) (hintegral : ∀ (i : I), (points i).IsIntegral) (weight : I → ℝ) (hweight : ∀ (i : I), 0 ≤ weight i) (htotal : 0 < ∑ i : I, weight i) : ∃ q ∈ Ω, q.IsIntegral ∧ ∀ (ξ : F.LinearFunction) (hq : ξ.EvaluableAt q), (∑ i : I, weight i) / ↑(hellyConstant Ω) ≤ ∑ i : I, if ∃ (hi : ξ.EvaluableAt (points i)), ξ.eval q hq ≤ ξ.eval (points i) hi then weight i else 0

@[reducible, inline]

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

The nonzero local ambient atoms, with node labels retained.

Equations

• Φ.LocalAtom = { a : Φ.flag.Node × EGZ.FpCoord p d // Φ.localWeight a.1 a.2 ≠ 0 }

theorem EGZ.FlagDecomposition.localLift_centeredLift_ne_zero {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (hp : Odd p) (x : Φ.flag.Node) (v : FpCoord p d) (hv : Φ.localWeight x v ≠ 0) : Φ.localLift x ((Φ.representation.map x) v).centeredLift ≠ 0

def EGZ.FlagDecomposition.localAtomPoint {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (hp : Odd p) (a : Φ.LocalAtom) : Φ.flag.Point

The flag point associated with a local atom through its centered integral lift.

Equations

• Φ.localAtomPoint hp a = { base := (↑a).1, val := ((Φ.representation.map (↑a).1) (↑a).2).centeredLift.real, val_mem := ⋯ }

theorem EGZ.FlagDecomposition.localAtomPoint_proper {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (hp : Odd p) (a : Φ.LocalAtom) : Φ.localAtomPoint hp a ∈ Φ.properPoints

theorem EGZ.FlagDecomposition.localAtomPoint_integral {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (hp : Odd p) (a : Φ.LocalAtom) : (Φ.localAtomPoint hp a).IsIntegral

theorem EGZ.FlagDecomposition.sum_localAtom_weight {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) : ∑ a : Φ.LocalAtom, Φ.localWeight (↑a).1 (↑a).2 = Φ.retainedMass

theorem EGZ.FlagDecomposition.localAtomPoint_coord {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (hp : Odd p) (a : Φ.LocalAtom) {x : Φ.flag.Node} (h : (↑a).1 ≤ x) : (Φ.localAtomPoint hp a).coord h = ((Φ.representation.map x) (↑a).2).centeredLift.real

theorem EGZ.FlagDecomposition.sum_localAtom_on {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (hp : Odd p) (x : Φ.flag.Node) (S : Set (RealCoord (Φ.flag.rank x))) : (∑ a : Φ.LocalAtom, if (↑a).1 ≤ x ∧ ((Φ.representation.map x) (↑a).2).centeredLift.real ∈ S then Φ.localWeight (↑a).1 (↑a).2 else 0) = Φ.liftedMassOn x S

Grouping local ambient atoms below a node gives exactly its cumulative lifted mass on any set of real coordinates.

theorem EGZ.FlagDecomposition.exists_cumulative_centerpoint_helly {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (hp : Odd p) : ∃ q ∈ Φ.omega, q.IsIntegral ∧ ∀ (ξ : RealCoord (Φ.flag.rank q.base) →ᵃ[ℝ] ℝ), ↑Φ.retainedMass / ↑(ConvexFlag.hellyConstant Φ.properPoints) ≤ ↑(Φ.liftedMassOn q.base {z : RealCoord (Φ.flag.rank q.base) | ξ q.val ≤ ξ z})

The flag centerpoint has an integral base coordinate, and every closed halfspace through it carries at least retained mass divided by the flag's Helly constant in the cumulative lift at that base.

theorem EGZ.FlagDecomposition.exists_cumulative_centerpoint {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (hp : Nat.Prime p) (hodd : Odd p) : ∃ q ∈ Φ.omega, q.IsIntegral ∧ ∀ (ξ : RealCoord (Φ.flag.rank q.base) →ᵃ[ℝ] ℝ), ↑Φ.retainedMass / ↑(hollowConstant p d) ≤ ↑(Φ.liftedMassOn q.base {z : RealCoord (Φ.flag.rank q.base) | ξ q.val ≤ ξ z})

Proposition 7.1 converts the cumulative centerpoint bound to the hollow constant of the original finite-field space.

theorem EGZ.FlagDecomposition.cumulativeMass_lower_of_halfspace_lower {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (hodd : Odd p) (q : Φ.flag.Point) {a : ℝ} (h : ∀ (ξ : RealCoord (Φ.flag.rank q.base) →ᵃ[ℝ] ℝ), a ≤ ↑(Φ.liftedMassOn q.base {z : RealCoord (Φ.flag.rank q.base) | ξ q.val ≤ ξ z})) : a ≤ ↑(natMass (Φ.cumulativeWeight q.base))

The constant zero functional detects the entire cumulative mass, including when the base lattice has dimension zero.

theorem EGZ.FlagDecomposition.isLargeElement_of_halfspace_lower {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (hodd : Odd p) (q : Φ.flag.Point) {ε : ℝ} (h : ∀ (ξ : RealCoord (Φ.flag.rank q.base) →ᵃ[ℝ] ℝ), ε * ↑Φ.retainedMass ≤ ↑(Φ.liftedMassOn q.base {z : RealCoord (Φ.flag.rank q.base) | ξ q.val ≤ ξ z})) : Φ.IsLargeElement ε q.base

theorem EGZ.FlagDecomposition.exists_cumulative_centerpoint_large {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (hp : Nat.Prime p) (hodd : Odd p) : ∃ q ∈ Φ.omega, q.IsIntegral ∧ Φ.IsLargeElement (↑(hollowConstant p d))⁻¹ q.base ∧ ∀ (ξ : RealCoord (Φ.flag.rank q.base) →ᵃ[ℝ] ℝ), ↑Φ.retainedMass / ↑(hollowConstant p d) ≤ ↑(Φ.liftedMassOn q.base {z : RealCoord (Φ.flag.rank q.base) | ξ q.val ≤ ξ z})

The cumulative centerpoint lies at a node large at inverse-hollow scale.