The initial flag decomposition

Every nonzero weight has a singleton flag decomposition with a rank-zero lattice fibre. Its ambient affine space is the affine span of the support. It retains all the input mass and is reduced and minimal. This is the starting object for the refinement argument.

noncomputable def EGZ.rankZeroPolytope : RationalPolytope 0

The unique polytope in the rank-zero coordinate space.

Equations

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

@[reducible, inline]

noncomputable abbrev EGZ.rankZeroFlag : ConvexFlag

A singleton flag with a rank-zero lattice fibre.

Equations

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

noncomputable def EGZ.FlagDecomposition.initialRepresentation {p d : ℕ} [NeZero p] (f : FpCoord p d → ℕ) (hf : f ≠ 0) : FpRepresentation p d rankZeroFlag

The initial representation collapses the affine span of the support onto the unique rank-zero finite-field vector.

Equations

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

noncomputable def EGZ.FlagDecomposition.initial {p d : ℕ} [NeZero p] (f : FpCoord p d → ℕ) (hf : f ≠ 0) : FlagDecomposition p d f

The singleton initial decomposition retains all of a nonzero input weight. No lower bound on the modulus is needed for its rank-zero lifts.

Equations

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

@[simp]

theorem EGZ.FlagDecomposition.initial_retainedWeight {p d : ℕ} [NeZero p] (f : FpCoord p d → ℕ) (hf : f ≠ 0) : (initial f hf).retainedWeight = f

@[simp]

theorem EGZ.FlagDecomposition.initial_cumulative {p d : ℕ} [NeZero p] (f : FpCoord p d → ℕ) (hf : f ≠ 0) (x : (initial f hf).flag.Node) : (initial f hf).cumulativeWeight x = f

@[simp]

theorem EGZ.FlagDecomposition.initial_retainedMass {p d : ℕ} [NeZero p] (f : FpCoord p d → ℕ) (hf : f ≠ 0) : (initial f hf).retainedMass = natMass f

@[simp]

theorem EGZ.FlagDecomposition.initial_card {p d : ℕ} [NeZero p] (f : FpCoord p d → ℕ) (hf : f ≠ 0) : Fintype.card (initial f hf).flag.Node = 1

The initial flag has exactly one node.

theorem EGZ.FlagDecomposition.initial_isKBounded {p d : ℕ} [NeZero p] (f : FpCoord p d → ℕ) (hf : f ≠ 0) (K : (initial f hf).flag.Node → ℕ) : (initial f hf).IsKBounded K

Every coordinate of the initial fibre is zero, so every coordinate bound is valid.

theorem EGZ.FlagDecomposition.initial_isReduced {p d : ℕ} [NeZero p] (f : FpCoord p d → ℕ) (hf : f ≠ 0) : (initial f hf).IsReduced

The unique initial node is reduced.

theorem EGZ.FlagDecomposition.initial_isMinimal {p d : ℕ} [NeZero p] (f : FpCoord p d → ℕ) (hf : f ≠ 0) : (initial f hf).IsMinimal

The initial affine space and rank-zero affine lattice are minimal.

@[simp]

theorem EGZ.FlagDecomposition.initial_gap {p d : ℕ} [NeZero p] (f : FpCoord p d → ℕ) (hf : f ≠ 0) (x : (initial f hf).flag.Node) : (initial f hf).gap x = natMass f

The unique positive lifted mass of the initial decomposition is the entire input mass.

theorem EGZ.FlagDecomposition.initial_isRealizedFace {p d : ℕ} [NeZero p] (f : FpCoord p d → ℕ) (hf : f ≠ 0) (x : (initial f hf).flag.Node) (Γ : ((initial f hf).flag.polytope x).Face) : (initial f hf).IsRealizedFace x Γ

Every face of the initial polytope is realized.

theorem EGZ.FlagDecomposition.initial_isComplete_dimZero {p : ℕ} [NeZero p] (f : FpCoord p 0 → ℕ) (hf : f ≠ 0) (T : (initial f hf).flag.Node → ℕ) (ε δ : ℝ) : (initial f hf).IsComplete T ε δ

In ambient dimension zero every affine functional is constant, so the initial node satisfies completeness for all parameters.