Documentation

LeanPool.ErdosGinzburgZiv.EGZ.Decomposition.Restrict

Restriction to reduced nodes #

The reduced bases form a nonempty finite join-closed set. Restriction to this set preserves every local contribution, since a non-reduced base has zero local weight. The resulting flag has the same proper points, viewed through the inclusion of its nodes in the original flag.

theorem EGZ.FlagDecomposition.exists_isReducedElement {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) :

∃ (x : Φ.flag.Node), Φ.IsReducedElement x

@[reducible, inline]

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

The join-closed set of bases which occur among the proper points.

Equations

Φ.ReducedNode = { x : Φ.flag.Node // Φ.IsReducedElement x }

Instances For

@[instance_reducible]

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

Fintype Φ.ReducedNode

Equations

Φ.instFintypeReducedNode = Subtype.fintype Φ.IsReducedElement

instance EGZ.FlagDecomposition.instNonemptyReducedNode {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) :

Nonempty Φ.ReducedNode

@[instance_reducible]

instance EGZ.FlagDecomposition.instSemilatticeSupReducedNode {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) :

SemilatticeSup Φ.ReducedNode

Equations

Φ.instSemilatticeSupReducedNode = Subtype.semilatticeSup ⋯

@[instance_reducible]

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

OrderTop Φ.ReducedNode

Equations

Φ.instOrderTopReducedNode = { top := Finset.univ.sup' ⋯ id, le_top := ⋯ }

@[reducible, inline]

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

The convex flag obtained by retaining just the reduced nodes.

Equations

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

Instances For

def EGZ.FlagDecomposition.reducedPointInclusion {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (q : Φ.reducedFlag.Point) :

The inclusion of points of the restricted flag in the original flag.

Equations

Φ.reducedPointInclusion q = { base := ↑q.base, val := q.val, val_mem := ⋯ }

Instances For

def EGZ.FlagDecomposition.toReducedPoint {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (q : Φ.flag.Point) (hq : Φ.IsReducedElement q.base) :

Φ.reducedFlag.Point

A point whose base is reduced can be viewed in the restricted flag.

Equations

Φ.toReducedPoint q hq = { base := ⟨q.base, hq⟩, val := q.val, val_mem := ⋯ }

Instances For

@[simp]

theorem EGZ.FlagDecomposition.reducedPointInclusion_toReducedPoint {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (q : Φ.flag.Point) (hq : Φ.IsReducedElement q.base) :

Φ.reducedPointInclusion (Φ.toReducedPoint q hq) = q

theorem EGZ.FlagDecomposition.convexCombination_toReducedPoint {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) {I : Type u_1} [Fintype I] (points : I → Φ.flag.Point) (weight : I → ℝ) (q : Φ.flag.Point) (hpoints : ∀ (i : I), Φ.IsReducedElement (points i).base) (hq : Φ.IsReducedElement q.base) (hcomb : ConvexFlag.ConvexCombination points weight q) :

ConvexFlag.ConvexCombination (fun (i : I) => Φ.toReducedPoint (points i) ⋯) weight (Φ.toReducedPoint q hq)

Convex combinations in the original flag descend to the restricted flag whenever all the displayed bases are reduced.

theorem EGZ.FlagDecomposition.convexCombination_reducedPointInclusion {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) {I : Type u_1} [Fintype I] (points : I → Φ.reducedFlag.Point) (weight : I → ℝ) (q : Φ.reducedFlag.Point) (hcomb : ConvexFlag.ConvexCombination points weight q) :

ConvexFlag.ConvexCombination (fun (i : I) => Φ.reducedPointInclusion (points i)) weight (Φ.reducedPointInclusion q)

Inclusion into the original flag preserves convex combinations. The finite join of the active bases is reduced, so it can be used to compare the two least-upper-bound conditions.

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

FpRepresentation p d Φ.reducedFlag

The original representation restricted to the reduced nodes.

Equations

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

Instances For

theorem EGZ.FlagDecomposition.sum_reducedNode_eq {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (hp : Odd p) (v : FpCoord p d) :

∑ x : Φ.ReducedNode, Φ.localWeight (↑x) v = ∑ x : Φ.flag.Node, Φ.localWeight x v

theorem EGZ.FlagDecomposition.cumulativeWeight_reducedNode {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (hp : Odd p) (x : Φ.ReducedNode) (v : FpCoord p d) :

FlagDecompositionRaw.cumulativeWeight (fun (y : Φ.reducedFlag.Node) => Φ.localWeight ↑y) x v = Φ.cumulativeWeight (↑x) v

theorem EGZ.FlagDecomposition.hat_reducedNode {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (hp : Odd p) (x : Φ.ReducedNode) (z : IntCoord (Φ.flag.rank ↑x)) :

FlagDecompositionRaw.hat Φ.reducedRepresentation (fun (y : Φ.reducedFlag.Node) => Φ.localWeight ↑y) x z = Φ.hat (↑x) z

theorem EGZ.FlagDecomposition.omegaZero_reducedPointInclusion_iff {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (q : Φ.reducedFlag.Point) :

(q ∈ FlagDecompositionRaw.omegaZero Φ.reducedRepresentation fun (x : Φ.reducedFlag.Node) => Φ.localWeight ↑x) ↔ Φ.reducedPointInclusion q ∈ Φ.omegaZero

theorem EGZ.FlagDecomposition.omega_reducedPointInclusion_iff {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (q : Φ.reducedFlag.Point) :

(q ∈ FlagDecompositionRaw.omega Φ.reducedRepresentation fun (x : Φ.reducedFlag.Node) => Φ.localWeight ↑x) ↔ Φ.reducedPointInclusion q ∈ Φ.omega

Inclusion identifies the proper-point set of the restricted data with the original proper points whose bases lie in the restriction.

@[reducible, inline]

noncomputable abbrev EGZ.FlagDecomposition.reduced {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (hp : Odd p) :

FlagDecomposition p d f

Restrict a decomposition to its reduced nodes. No local mass is lost. The odd-modulus assumption ensures that zero local lifts detect exactly zero local finite-field weights.

Equations

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

Instances For

@[simp]

theorem EGZ.FlagDecomposition.reduced_localWeight {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (hp : Odd p) (x : Φ.ReducedNode) :

(Φ.reduced hp).localWeight x = Φ.localWeight ↑x

@[simp]

theorem EGZ.FlagDecomposition.reduced_cumulativeWeight {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (hp : Odd p) (x : Φ.ReducedNode) :

(Φ.reduced hp).cumulativeWeight x = Φ.cumulativeWeight ↑x

@[simp]

theorem EGZ.FlagDecomposition.reduced_retainedWeight {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (hp : Odd p) :

(Φ.reduced hp).retainedWeight = Φ.retainedWeight

@[simp]

theorem EGZ.FlagDecomposition.reduced_retainedMass {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (hp : Odd p) :

(Φ.reduced hp).retainedMass = Φ.retainedMass

theorem EGZ.FlagDecomposition.card_reduced_le {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (hp : Odd p) :

Fintype.card (Φ.reduced hp).flag.Node ≤ Fintype.card Φ.flag.Node

Removing non-reduced nodes cannot increase the number of nodes.

@[simp]

theorem EGZ.FlagDecomposition.reduced_hat {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (hp : Odd p) (x : Φ.ReducedNode) :

(Φ.reduced hp).hat x = Φ.hat ↑x

@[simp]

theorem EGZ.FlagDecomposition.reduced_gap {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (hp : Odd p) (x : Φ.ReducedNode) :

(Φ.reduced hp).gap x = Φ.gap ↑x

@[simp]

theorem EGZ.FlagDecomposition.reduced_omega_iff {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (hp : Odd p) (q : Φ.reducedFlag.Point) :

q ∈ (Φ.reduced hp).omega ↔ Φ.reducedPointInclusion q ∈ Φ.omega

theorem EGZ.FlagDecomposition.image_reduced_omega {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (hp : Odd p) :

Φ.reducedPointInclusion '' (Φ.reduced hp).omega = Φ.omega

Every original proper point is retained: its base is reduced by definition. Thus inclusion identifies the two full proper-point sets.

theorem EGZ.FlagDecomposition.reduced_isReduced {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (hp : Odd p) :

(Φ.reduced hp).IsReduced

Every retained node is reduced in the restricted decomposition.

theorem EGZ.FlagDecomposition.reduced_isKBounded {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (hp : Odd p) {K : Φ.flag.Node → ℕ} (hK : Φ.IsKBounded K) :

(Φ.reduced hp).IsKBounded fun (x : (Φ.reduced hp).flag.Node) => K ↑x

Restriction preserves the same coordinate bound at every retained node.

@[simp]

theorem EGZ.FlagDecomposition.reduced_liftedMassOn {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (hp : Odd p) (x : Φ.ReducedNode) (S : Set (RealCoord (Φ.flag.rank ↑x))) :

(Φ.reduced hp).liftedMassOn x S = Φ.liftedMassOn (↑x) S

@[simp]

theorem EGZ.FlagDecomposition.reduced_isLargeElement_iff {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (hp : Odd p) (ε : ℝ) (x : Φ.ReducedNode) :

(Φ.reduced hp).IsLargeElement ε x ↔ Φ.IsLargeElement ε ↑x

@[simp]

theorem EGZ.FlagDecomposition.reduced_isLargeFace_iff {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (hp : Odd p) (ε : ℝ) (x : Φ.ReducedNode) (Γ : (Φ.flag.polytope ↑x).Face) :

(Φ.reduced hp).IsLargeFace ε x Γ ↔ Φ.IsLargeFace ε (↑x) Γ

@[simp]

theorem EGZ.FlagDecomposition.reduced_isCompleteElement_iff {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (hp : Odd p) (x : Φ.ReducedNode) (t : ℕ) (δ : ℝ) :

(Φ.reduced hp).IsCompleteElement x t δ ↔ Φ.IsCompleteElement (↑x) t δ

theorem EGZ.FlagDecomposition.reduced_isMinimal {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (hp : Odd p) (hmin : Φ.IsMinimal) :

(Φ.reduced hp).IsMinimal

The ambient affine spans and affine integer generating sets at retained nodes are unchanged, so minimality is preserved.

theorem EGZ.FlagDecomposition.reduced_pointsOnFace_iff {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (hp : Odd p) (x : Φ.ReducedNode) (Γ : (Φ.flag.polytope ↑x).Face) (q : Φ.reducedFlag.Point) :

q ∈ (Φ.reduced hp).pointsOnFace x Γ ↔ Φ.reducedPointInclusion q ∈ Φ.pointsOnFace (↑x) Γ

theorem EGZ.FlagDecomposition.reduced_faceBases_iff {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (hp : Odd p) (x y : Φ.ReducedNode) (Γ : (Φ.flag.polytope ↑x).Face) :

y ∈ (Φ.reduced hp).faceBases x Γ ↔ ↑y ∈ Φ.faceBases (↑x) Γ

theorem EGZ.FlagDecomposition.reduced_faceIndex_val {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (hp : Odd p) (x : Φ.ReducedNode) (Γ : (Φ.flag.polytope ↑x).Face) :

↑((Φ.reduced hp).faceIndex x Γ) = Φ.faceIndex (↑x) Γ

The face index computed after restriction is the same original node. Every face index is reduced, which makes it available in the restriction.

theorem EGZ.FlagDecomposition.reduced_faceIndex {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (hp : Odd p) (x : Φ.ReducedNode) (Γ : (Φ.flag.polytope ↑x).Face) :

(Φ.reduced hp).faceIndex x Γ = ⟨Φ.faceIndex (↑x) Γ, ⋯⟩

@[simp]

theorem EGZ.FlagDecomposition.reduced_isRealizedFace_iff {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (hp : Odd p) (x : Φ.ReducedNode) (Γ : (Φ.flag.polytope ↑x).Face) :

(Φ.reduced hp).IsRealizedFace x Γ ↔ Φ.IsRealizedFace (↑x) Γ

theorem EGZ.FlagDecomposition.reduced_isComplete {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (hp : Odd p) {T : Φ.flag.Node → ℕ} {ε δ : ℝ} (hcomplete : Φ.IsComplete T ε δ) :

(Φ.reduced hp).IsComplete (fun (x : (Φ.reduced hp).flag.Node) => T ↑x) ε δ

Restriction preserves completeness with the same thresholds at every retained node and the same parameters.