The selected cumulative lattice configuration

These bridges package an integral interior centerpoint and the cumulative lift at its base in the finite integer-coordinate language used by balanced combinations. The bounds retain the selected node's own radius.

theorem EGZ.FlagDecomposition.integralPoint_coordinates {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (q : Φ.flag.Point) (hq : q.IsIntegral) : ∃ (c : IntCoord (Φ.flag.rank q.base)), c.real = q.val

theorem EGZ.FlagDecomposition.integer_mem_affineSpan_liftedSupport {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (hmin : Φ.IsMinimal) (x : Φ.flag.Node) (c : IntCoord (Φ.flag.rank x)) : c ∈ affineSpan ℤ ↑(Φ.liftedSupport x)

theorem EGZ.FlagDecomposition.liftedSupport_bound {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) {K : Φ.flag.Node → ℕ} (hK : Φ.IsKBounded K) (x : Φ.flag.Node) (z : IntCoord (Φ.flag.rank x)) : z ∈ Φ.liftedSupport x → latticeSupNorm z ≤ K x

theorem EGZ.FlagDecomposition.liftedSupport_subset_latticeBox {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) {K : Φ.flag.Node → ℕ} (hK : Φ.IsKBounded K) (x : Φ.flag.Node) : Φ.liftedSupport x ⊆ latticeBox (Φ.flag.rank x) (K x)

theorem EGZ.FlagDecomposition.integralPoint_bound {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) {K : Φ.flag.Node → ℕ} (hK : Φ.IsKBounded K) (q : Φ.flag.Point) (c : IntCoord (Φ.flag.rank q.base)) (hc : c.real = q.val) : latticeSupNorm c ≤ K q.base

theorem EGZ.FlagDecomposition.cumulativeSupport_sum {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (hodd : Odd p) (x : Φ.flag.Node) : ∑ q : ↥(Φ.liftedSupport x), Φ.hat x ↑q = natMass (Φ.cumulativeWeight x)

noncomputable def EGZ.FlagDecomposition.cumulativeBalancedData {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (hmin : Φ.IsMinimal) (x : Φ.flag.Node) (c : IntCoord (Φ.flag.rank x)) (hc : c.real ∈ intrinsicInterior ℝ (Φ.flag.polytope x).carrier) : BalancedCombination.Data (Φ.flag.rank x)

The cumulative mass profile at an interior lattice center, in the balanced-combination interface.

Equations

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

noncomputable def EGZ.FlagDecomposition.cumulativeCentrality {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (x : Φ.flag.Node) : ℝ

Centrality normalized by the selected cumulative mass.

Equations

• Φ.cumulativeCentrality x = ↑Φ.retainedMass / (↑(EGZ.hollowConstant p d) * ↑(EGZ.natMass (Φ.cumulativeWeight x)))

theorem EGZ.FlagDecomposition.cumulativeCentrality_mul_mass {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (hodd : Odd p) (x : Φ.flag.Node) : Φ.cumulativeCentrality x * ↑(natMass (Φ.cumulativeWeight x)) = ↑Φ.retainedMass / ↑(hollowConstant p d)

theorem EGZ.FlagDecomposition.cumulativeCentrality_pos {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (hodd : Odd p) (hw : 0 < hollowConstant p d) (x : Φ.flag.Node) : 0 < Φ.cumulativeCentrality x

theorem EGZ.FlagDecomposition.inv_hollowConstant_le_cumulativeCentrality {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (hodd : Odd p) (x : Φ.flag.Node) : (↑(hollowConstant p d))⁻¹ ≤ Φ.cumulativeCentrality x

theorem EGZ.FlagDecomposition.cumulativeBalancedData_isCentral {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (hodd : Odd p) (hmin : Φ.IsMinimal) (x : Φ.flag.Node) (c : IntCoord (Φ.flag.rank x)) (hc : c.real ∈ intrinsicInterior ℝ (Φ.flag.polytope x).carrier) (hcentral : ∀ (ξ : RealCoord (Φ.flag.rank x) →ᵃ[ℝ] ℝ), ↑Φ.retainedMass / ↑(hollowConstant p d) ≤ ↑(Φ.liftedMassOn x {z : RealCoord (Φ.flag.rank x) | ξ c.real ≤ ξ z})) : BalancedCombination.IsCentral (Φ.cumulativeBalancedData hmin x c hc).support (Φ.cumulativeBalancedData hmin x c hc).weight (Φ.cumulativeCentrality x) c.real

structure EGZ.FlagDecomposition.CumulativeSelection {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (T K : Φ.flag.Node → ℕ) (δ : ℝ) : Type

The concrete cumulative fibre selected for the balanced-combination and relative-expansion arguments. All bounds use its own node radius.

• node : Φ.flag.Node

  The flag node at which the cumulative selection is made.

• center : IntCoord (Φ.flag.rank self.node)

  The integral center of the selected node's lifted support.

• center_mem_span : self.center ∈ affineSpan ℤ ↑(Φ.liftedSupport self.node)
• center_mem_interior : self.center.real ∈ intrinsicInterior ℝ ((convexHull ℝ) (IntCoord.real '' ↑(Φ.liftedSupport self.node)))
• center_mem_box : self.center ∈ latticeBox (Φ.flag.rank self.node) (K self.node)
• support_subset_box : Φ.liftedSupport self.node ⊆ latticeBox (Φ.flag.rank self.node) (K self.node)
• complete : Φ.IsCompleteElement self.node (T self.node) δ
• central : BalancedCombination.IsCentral (Φ.liftedSupport self.node) (fun (q : ↥(Φ.liftedSupport self.node)) => ↑(Φ.hat self.node ↑q)) (Φ.cumulativeCentrality self.node) self.center.real
• centrality_pos : 0 < Φ.cumulativeCentrality self.node

noncomputable def EGZ.FlagDecomposition.CumulativeSelection.data {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} {T K : Φ.flag.Node → ℕ} {δ : ℝ} (D : Φ.CumulativeSelection T K δ) : BalancedCombination.Data (Φ.flag.rank D.node)

The balanced combination data supplied by a cumulative selection.

Equations

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

theorem EGZ.FlagDecomposition.CumulativeSelection.centrality_le_one {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} {T K : Φ.flag.Node → ℕ} {δ : ℝ} (D : Φ.CumulativeSelection T K δ) : Φ.cumulativeCentrality D.node ≤ 1

theorem EGZ.FlagDecomposition.CumulativeSelection.mass_pos {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} {T K : Φ.flag.Node → ℕ} {δ : ℝ} (D : Φ.CumulativeSelection T K δ) (hodd : Odd p) : 0 < ∑ q : ↥(Φ.liftedSupport D.node), ↑(Φ.hat D.node ↑q)

theorem EGZ.FlagDecomposition.CumulativeSelection.mass_le_retained {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} {T K : Φ.flag.Node → ℕ} {δ : ℝ} (D : Φ.CumulativeSelection T K δ) (hodd : Odd p) : ∑ q : ↥(Φ.liftedSupport D.node), ↑(Φ.hat D.node ↑q) ≤ ↑Φ.retainedMass

theorem EGZ.FlagDecomposition.CumulativeSelection.centrality_mul_mass {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} {T K : Φ.flag.Node → ℕ} {δ : ℝ} (D : Φ.CumulativeSelection T K δ) (hodd : Odd p) : Φ.cumulativeCentrality D.node * ∑ q : ↥(Φ.liftedSupport D.node), ↑(Φ.hat D.node ↑q) = ↑Φ.retainedMass / ↑(hollowConstant p d)

theorem EGZ.FlagDecomposition.select_cumulative_node {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (hp : Nat.Prime p) (hodd : Odd p) {ε δ : ℝ} {T K : Φ.flag.Node → ℕ} (hε : 0 ≤ ε) (hεW : ε ≤ (↑(hollowConstant p d))⁻¹) (hcomplete : Φ.IsComplete T ε δ) (hK : Φ.IsKBounded K) : Nonempty (Φ.CumulativeSelection T K δ)

Completeness and the flag centerpoint theorem select a full-dimensional interior lattice center in an element complete at the requested scale.