Flag decompositions

This file contains the definitions from the beginning of Section 4 of the paper. The ambient finite-field space and every lattice fibre use the coordinate models from EGZ.Convex.Coordinate.

There are two different lifted weights. hat is cumulative over all nodes below x; localLift uses only the summand based at x. Proper-point generators are defined from localLift. This distinction is the correction integrated into the current version of the paper.

Slabs, thinness, and thickness

def EGZ.HasBoundedRepresentative (p K : ℕ) (a : ZMod p) : Prop

A residue has an integer representative in the interval [-K, K].

This definition remains meaningful without a large-prime hypothesis. Such a hypothesis is needed only when uniqueness of the representative is used.

Equations

• EGZ.HasBoundedRepresentative p K a = ∃ (z : ℤ), z.natAbs ≤ K ∧ ↑z = a

def EGZ.slab {p d : ℕ} (ξ : FpCoord p d →ᵃ[ZMod p] ZMod p) (K : ℕ) : Set (FpCoord p d)

The K-slab cut out by an affine functional on 𝔽_p^d.

Equations

• EGZ.slab ξ K = {v : EGZ.FpCoord p d | EGZ.HasBoundedRepresentative p K (ξ v)}

noncomputable def EGZ.natMassOn {α : Type u_1} [Fintype α] (w : α → ℕ) (S : Set α) : ℕ

The mass of a natural-valued function on a subset of a finite type.

Equations

• EGZ.natMassOn w S = ∑ a : α, if a ∈ S then w a else 0

noncomputable def EGZ.natMass {α : Type u_1} [Fintype α] (w : α → ℕ) : ℕ

The total mass of a natural-valued function on a finite type.

Equations

• EGZ.natMass w = ∑ a : α, w a

noncomputable def EGZ.nnrealMassOn {α : Type u_1} [Fintype α] (w : α → NNReal) (S : Set α) : NNReal

Mass of an NNReal-valued function on a subset of a finite type.

Equations

• EGZ.nnrealMassOn w S = ∑ a : α, if a ∈ S then w a else 0

noncomputable def EGZ.nnrealMass {α : Type u_1} [Fintype α] (w : α → NNReal) : NNReal

Total mass of an NNReal-valued function on a finite type.

Equations

• EGZ.nnrealMass w = ∑ a : α, w a

def EGZ.IsThinAlongNNReal {p d : ℕ} [NeZero p] (w : FpCoord p d → NNReal) (ξ : FpCoord p d →ᵃ[ZMod p] ZMod p) (K : ℕ) (ε : ℝ) : Prop

Definition 4.1 for the nonnegative real weights used in the paper.

Equations

• EGZ.IsThinAlongNNReal w ξ K ε = ((1 - ε) * ↑(EGZ.nnrealMass w) ≤ ↑(EGZ.nnrealMassOn w (EGZ.slab ξ K)))

def EGZ.IsThinAlong {p d : ℕ} [NeZero p] (w : FpCoord p d → ℕ) (ξ : FpCoord p d →ᵃ[ZMod p] ZMod p) (K : ℕ) (ε : ℝ) : Prop

Natural-valued specialization used by flag decompositions and Theorem 4.13.

Equations

• EGZ.IsThinAlong w ξ K ε = EGZ.IsThinAlongNNReal (fun (v : EGZ.FpCoord p d) => ↑(w v)) ξ K ε

def EGZ.IsThickAlong {p d : ℕ} [NeZero p] (w : FpCoord p d → ℕ) (ξ : FpCoord p d →ᵃ[ZMod p] ZMod p) (K : ℕ) (ε : ℝ) : Prop

Thickness is the negation of thinness, as in Definition tt.

Equations

• EGZ.IsThickAlong w ξ K ε = ¬EGZ.IsThinAlong w ξ K ε

Representations of a lattice flag over 𝔽_p

structure EGZ.FpRepresentation (p d : ℕ) (F : ConvexFlag) : Type u_1

An 𝔽_p-representation of a convex lattice flag in the ambient affine space 𝔽_p^d.

The maps are stored as affine maps on the ambient coordinate space and are required to be surjective only after restriction to space x. Every affine map on an affine subspace of this finite-dimensional space extends to the ambient space, while this representation avoids dependent subtype maps in all fibre sums below.

• space : F.Node → AffineSubspace (ZMod p) (FpCoord p d)

  Affine subspace over the finite field represented at each flag node.

• map (x : F.Node) : FpCoord p d →ᵃ[ZMod p] FpCoord p (F.rank x)

  Affine coordinate map for each represented flag node.

• space_mono {x y : F.Node} : x ≤ y → self.space x ≤ self.space y
• map_surjective (x : F.Node) : Set.SurjOn (⇑(self.map x)) (↑(self.space x)) Set.univ
• compatible {x y : F.Node} (h : x ≤ y) {v : FpCoord p d} : v ∈ self.space x → (self.map y) v = ((F.transition h).modp p) ((self.map x) v)
• lattice_eq_standard (x : F.Node) (q : RealCoord (F.rank x)) : q ∈ F.lattice x ↔ IsIntegral q

def EGZ.FpRepresentation.NonconstantOnFibers {p d : ℕ} {F : ConvexFlag} (R : FpRepresentation p d F) (x : F.Node) (ξ : FpCoord p d →ᵃ[ZMod p] ZMod p) : Prop

An affine functional is nonconstant on the fibres of the representation at x if two points in one fibre receive different values.

Equations

• R.NonconstantOnFibers x ξ = ∃ (v : EGZ.FpCoord p d) (w : EGZ.FpCoord p d), v ∈ R.space x ∧ w ∈ R.space x ∧ (R.map x) v = (R.map x) w ∧ ξ v ≠ ξ w

Coordinate lifts

def EGZ.latticeSupNorm {n : ℕ} (z : IntCoord n) : ℕ

Sup norm in the chosen affine-lattice coordinates.

Equations

• EGZ.latticeSupNorm z = Finset.univ.sup fun (i : Fin n) => (z i).natAbs

def EGZ.IsCenteredLift (p : ℕ) {n : ℕ} (z : IntCoord n) : Prop

A lattice coordinate lies in the centered representative box modulo p.

Equations

• EGZ.IsCenteredLift p z = (EGZ.latticeSupNorm z ≤ (p - 1) / 2)

noncomputable def EGZ.FlagDecompositionRaw.retainedWeight {p d : ℕ} {F : ConvexFlag} (pieces : F.Node → FpCoord p d → ℕ) (v : FpCoord p d) : ℕ

Sum of all local summands at an ambient point.

Equations

• EGZ.FlagDecompositionRaw.retainedWeight pieces v = ∑ x : F.Node, pieces x v

noncomputable def EGZ.FlagDecompositionRaw.cumulativeWeight {p d : ℕ} {F : ConvexFlag} (pieces : F.Node → FpCoord p d → ℕ) (x : F.Node) (v : FpCoord p d) : ℕ

The cumulative function f_{≼ x}.

Equations

• EGZ.FlagDecompositionRaw.cumulativeWeight pieces x v = ∑ y : F.Node, if y ≤ x then pieces y v else 0

noncomputable def EGZ.FlagDecompositionRaw.affineFibreMass {p d : ℕ} [NeZero p] {n : ℕ} (w : FpCoord p d → ℕ) (φ : FpCoord p d → FpCoord p n) (c : FpCoord p n) : ℕ

Push a finite weight through an affine map whose target rank may vary.

Equations

• EGZ.FlagDecompositionRaw.affineFibreMass w φ c = ∑ v : EGZ.FpCoord p d, if φ v = c then w v else 0

noncomputable def EGZ.FlagDecompositionRaw.localLift {p d : ℕ} [NeZero p] {F : ConvexFlag} (R : FpRepresentation p d F) (pieces : F.Node → FpCoord p d → ℕ) (x : F.Node) (q : IntCoord (F.rank x)) : ℕ

The local centered lift f_x°, using only the summand based at x.

Equations

• EGZ.FlagDecompositionRaw.localLift R pieces x q = if EGZ.IsCenteredLift p q then EGZ.FlagDecompositionRaw.affineFibreMass (pieces x) (⇑(R.map x)) (EGZ.IntCoord.mod p q) else 0

noncomputable def EGZ.FlagDecompositionRaw.hat {p d : ℕ} [NeZero p] {F : ConvexFlag} (R : FpRepresentation p d F) (pieces : F.Node → FpCoord p d → ℕ) (x : F.Node) (q : IntCoord (F.rank x)) : ℕ

The cumulative centered lift hat f_x.

Equations

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

def EGZ.FlagDecompositionRaw.omegaZero {p d : ℕ} [NeZero p] {F : ConvexFlag} (R : FpRepresentation p d F) (pieces : F.Node → FpCoord p d → ℕ) : Set F.Point

Corrected local generating points. A generator based at x is selected by positive localLift, not by cumulative hat.

Equations

• EGZ.FlagDecompositionRaw.omegaZero R pieces = {q : F.Point | ∃ (z : EGZ.IntCoord (F.rank q.base)), z.real = q.val ∧ EGZ.FlagDecompositionRaw.localLift R pieces q.base z ≠ 0}

def EGZ.FlagDecompositionRaw.omega {p d : ℕ} [NeZero p] {F : ConvexFlag} (R : FpRepresentation p d F) (pieces : F.Node → FpCoord p d → ℕ) : Set F.Point

Proper points associated with local decomposition data.

Equations

• EGZ.FlagDecompositionRaw.omega R pieces = F.convexHull (EGZ.FlagDecompositionRaw.omegaZero R pieces)

def EGZ.FlagDecompositionRaw.pointsOnFace {p d : ℕ} [NeZero p] {F : ConvexFlag} (R : FpRepresentation p d F) (pieces : F.Node → FpCoord p d → ℕ) (x : F.Node) (Γ : (F.polytope x).Face) : Set F.Point

Proper points whose coordinate at x lies on a given face.

Equations

• EGZ.FlagDecompositionRaw.pointsOnFace R pieces x Γ = {q : F.Point | q ∈ EGZ.FlagDecompositionRaw.omega R pieces ∧ ∃ (h : q.base ≤ x), q.coord h ∈ Γ.carrier}

def EGZ.FlagDecompositionRaw.VisibleFace {p d : ℕ} [NeZero p] {F : ConvexFlag} (R : FpRepresentation p d F) (pieces : F.Node → FpCoord p d → ℕ) (x : F.Node) (Γ : (F.polytope x).Face) : Prop

Visibility before packaging the data into a FlagDecomposition.

Equations

• EGZ.FlagDecompositionRaw.VisibleFace R pieces x Γ = (EGZ.FlagDecompositionRaw.pointsOnFace R pieces x Γ).Nonempty

theorem EGZ.FlagDecompositionRaw.omega_convex_closed {p d : ℕ} [NeZero p] {F : ConvexFlag} (R : FpRepresentation p d F) (pieces : F.Node → FpCoord p d → ℕ) : F.convexHull (omega R pieces) ⊆ omega R pieces

The proper-point set is convex-closed because it is itself defined as a flag convex hull.

Flag decompositions

structure EGZ.FlagDecomposition (p d : ℕ) [NeZero p] (f : FpCoord p d → ℕ) : Type 1

A natural-valued flag decomposition of f.

The finite lifted support is stored explicitly. Besides making the later mass and gap definitions computationally finite, the accompanying fields record the support/polytope invariant and rule out inactive nodes with empty cumulative support.

• flag : ConvexFlag

  Convex flag supporting the decomposition.

• representation : FpRepresentation p d self.flag

  Finite-field representation of the decomposition flag.

• localWeight : self.flag.Node → FpCoord p d → ℕ

  Natural-valued weight assigned locally at each flag node.

• local_supported (x : self.flag.Node) (v : FpCoord p d) : self.localWeight x v ≠ 0 → v ∈ self.representation.space x
• retained_le (v : FpCoord p d) : FlagDecompositionRaw.retainedWeight self.localWeight v ≤ f v
• liftedSupport (x : self.flag.Node) : Finset (IntCoord (self.flag.rank x))

  Finite integral support of the lifted weight at each node.

• liftedSupport_spec (x : self.flag.Node) (q : IntCoord (self.flag.rank x)) : q ∈ self.liftedSupport x ↔ FlagDecompositionRaw.hat self.representation self.localWeight x q ≠ 0
• liftedSupport_nonempty (x : self.flag.Node) : (self.liftedSupport x).Nonempty
• polytope_eq_liftedSupport (x : self.flag.Node) : (self.flag.polytope x).carrier = (convexHull ℝ) (IntCoord.real '' ↑(self.liftedSupport x))
• faces_visible (x : self.flag.Node) (Γ : (self.flag.polytope x).Face) : FlagDecompositionRaw.VisibleFace self.representation self.localWeight x Γ

noncomputable def EGZ.FlagDecomposition.retainedWeight {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) : FpCoord p d → ℕ

Total retained function f^Φ.

Equations

• Φ.retainedWeight = EGZ.FlagDecompositionRaw.retainedWeight Φ.localWeight

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

Cumulative function f_{≼ x}.

Equations

• Φ.cumulativeWeight x = EGZ.FlagDecompositionRaw.cumulativeWeight Φ.localWeight x

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

Local centered lifted function f_x°.

Equations

• Φ.localLift x = EGZ.FlagDecompositionRaw.localLift Φ.representation Φ.localWeight x

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

Cumulative centered lifted function hat f_x.

Equations

• Φ.hat x = EGZ.FlagDecompositionRaw.hat Φ.representation Φ.localWeight x

noncomputable def EGZ.FlagDecomposition.retainedMass {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) : ℕ

Total retained mass f^Φ(V).

Equations

• Φ.retainedMass = EGZ.natMass Φ.retainedWeight

noncomputable def EGZ.FlagDecomposition.liftedMassOn {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (x : Φ.flag.Node) (S : Set (RealCoord (Φ.flag.rank x))) : ℕ

Mass of hat f_x over lattice points whose real coordinates lie in S. The stored support makes this a finite sum.

Equations

• Φ.liftedMassOn x S = ∑ q ∈ Φ.liftedSupport x, if q.real ∈ S then Φ.hat x q else 0

def EGZ.FlagDecomposition.omegaZero {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) : Set Φ.flag.Point

Corrected set Ω₀ of local generating points.

Equations

• Φ.omegaZero = EGZ.FlagDecompositionRaw.omegaZero Φ.representation Φ.localWeight

def EGZ.FlagDecomposition.omega {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) : Set Φ.flag.Point

Corrected proper-point set Ω = conv Ω₀.

Equations

• Φ.omega = EGZ.FlagDecompositionRaw.omega Φ.representation Φ.localWeight

def EGZ.FlagDecomposition.properPoints {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) : Φ.flag.ProperPointSet

The corrected proper points, packaged with convex closure.

Equations

• Φ.properPoints = { carrier := Φ.omega, convex_closed := ⋯ }

def EGZ.FlagDecomposition.HasLocalPointMass {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (q : Φ.flag.Point) (m : ℕ) : Prop

The paper's pointwise local mass f° on flag points. The existential form avoids choosing integer coordinates; realification is injective, so the value is unambiguous whenever it is nonzero.

Equations

• Φ.HasLocalPointMass q m = ∃ (z : EGZ.IntCoord (Φ.flag.rank q.base)), z.real = q.val ∧ Φ.localLift q.base z = m

def EGZ.FlagDecomposition.pointsOnFace {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (x : Φ.flag.Node) (Γ : (Φ.flag.polytope x).Face) : Set Φ.flag.Point

Points of Ω lying over the face Γ at x.

Equations

• Φ.pointsOnFace x Γ = EGZ.FlagDecompositionRaw.pointsOnFace Φ.representation Φ.localWeight x Γ

def EGZ.FlagDecomposition.IsVisibleFace {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (x : Φ.flag.Node) (Γ : (Φ.flag.polytope x).Face) : Prop

A face is visible when a proper point lies over it.

Equations

• Φ.IsVisibleFace x Γ = (Φ.pointsOnFace x Γ).Nonempty

noncomputable def EGZ.FlagDecomposition.faceBases {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (x : Φ.flag.Node) (Γ : (Φ.flag.polytope x).Face) : Finset Φ.flag.Node

The finite set of bases used to define x_Γ.

Equations

• Φ.faceBases x Γ = {y : Φ.flag.Node | ∃ q ∈ Φ.pointsOnFace x Γ, q.base = y}

noncomputable def EGZ.FlagDecomposition.faceIndex {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (x : Φ.flag.Node) (Γ : (Φ.flag.polytope x).Face) : Φ.flag.Node

The element x_Γ: the supremum of the bases of proper points over a face. Every face of a flag decomposition is visible.

Equations

• Φ.faceIndex x Γ = (Φ.faceBases x Γ).sup' ⋯ id

theorem EGZ.FlagDecomposition.faceIndex_le {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (x : Φ.flag.Node) (Γ : (Φ.flag.polytope x).Face) : Φ.faceIndex x Γ ≤ x

def EGZ.FlagDecomposition.IsRealizedFace {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (x : Φ.flag.Node) (Γ : (Φ.flag.polytope x).Face) : Prop

A face is realized when the polytope at x_Γ maps into it.

Equations

• Φ.IsRealizedFace x Γ = ∀ q ∈ (Φ.flag.polytope (Φ.faceIndex x Γ)).carrier, (Φ.flag.transition ⋯).real q ∈ Γ.carrier

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

An element is reduced when some proper point is based exactly there.

Equations

• Φ.IsReducedElement x = ∃ q ∈ Φ.omega, q.base = x

def EGZ.FlagDecomposition.IsReduced {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) : Prop

Every element of the decomposition is reduced.

Equations

• Φ.IsReduced = ∀ (x : Φ.flag.Node), Φ.IsReducedElement x

def EGZ.FlagDecomposition.AffineIntSpans {n : ℕ} (S : Finset (IntCoord n)) : Prop

A finite set of lattice points affinely generates the full coordinate lattice over ℤ.

Equations

• EGZ.FlagDecomposition.AffineIntSpans S = ∀ (z : EGZ.IntCoord n), ∃ (c : EGZ.IntCoord n →₀ ℤ), c.support ⊆ S ∧ ∑ q ∈ c.support, c q = 1 ∧ ∑ q ∈ c.support, c q • q = z

def EGZ.FlagDecomposition.IsMinimal {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) : Prop

Minimality of the finite-field affine spaces and affine lattices.

Equations

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

def EGZ.FlagDecomposition.IsKBounded {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (K : Φ.flag.Node → ℕ) : Prop

The chosen affine-lattice coordinates are bounded by K on every lattice point of every node polytope.

Equations

• Φ.IsKBounded K = ∀ (x : Φ.flag.Node) (z : EGZ.IntCoord (Φ.flag.rank x)), z.real ∈ (Φ.flag.polytope x).carrier → EGZ.latticeSupNorm z ≤ K x

def EGZ.FlagDecomposition.IsLargeFace {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (ε : ℝ) (x : Φ.flag.Node) (Γ : (Φ.flag.polytope x).Face) : Prop

An ε-large face, Definition largef.

Equations

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

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

An ε-large flag element.

Equations

• Φ.IsLargeElement ε x = (ε * ↑Φ.retainedMass ≤ ↑(Φ.liftedMassOn x (Φ.flag.polytope x).carrier))

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

The minimum positive cumulative lifted mass at a node.

Equations

• Φ.gap x = (Finset.image (Φ.hat x) (Φ.liftedSupport x)).min' ⋯

def EGZ.FlagDecomposition.IsCompleteElement {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (x : Φ.flag.Node) (t : ℕ) (δ : ℝ) : Prop

Completeness of one element: every affine functional which varies on a representation fibre sees a thick cumulative weight.

Equations

• Φ.IsCompleteElement x t δ = ∀ (ξ : EGZ.FpCoord p d →ᵃ[ZMod p] ZMod p), Φ.representation.NonconstantOnFibers x ξ → EGZ.IsThickAlong (Φ.cumulativeWeight x) ξ t δ

def EGZ.FlagDecomposition.IsComplete {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (T : Φ.flag.Node → ℕ) (ε δ : ℝ) : Prop

A (T, ε, δ)-complete flag decomposition.

Equations

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

def EGZ.IsGrowing (g : ℕ → ℕ) : Prop

A growing function is monotone and strictly exceeds the identity.

Equations

• EGZ.IsGrowing g = (Monotone g ∧ ∀ (n : ℕ), n < g n)