Bounds for the augmented completeness diagram

Only lower-layer nodes carry added slab coordinates, and all their cumulative atoms lie in the selected slab intersection. Consequently the augmented support has rank at most twice the ambient dimension and lies in the last selected width box.

theorem EGZ.FlagDecomposition.CompletePreparation.extra_le_count {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} {anchor : Φ.flag.Node} {t : ℕ → ℕ} {δ : ℝ} (D : Φ.CompletePreparation anchor t δ) (hp : Odd p) (hδ : 0 ≤ δ) (hsmall : 3 ^ (d + 1) * δ < 1) (x : (D.split hp hδ hsmall).flag.Node) : D.extra hp hδ hsmall x ≤ D.count

theorem EGZ.FlagDecomposition.CompletePreparation.selected_of_extra_pos {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} {anchor : Φ.flag.Node} {t : ℕ → ℕ} {δ : ℝ} (D : Φ.CompletePreparation anchor t δ) (hp : Odd p) (hδ : 0 ≤ δ) (hsmall : 3 ^ (d + 1) * δ < 1) (x : (D.split hp hδ hsmall).flag.Node) (hx : 0 < D.extra hp hδ hsmall x) (v : FpCoord p d) (hv : (D.split hp hδ hsmall).cumulativeWeight x v ≠ 0) : v ∈ D.selectedSet

theorem EGZ.FlagDecomposition.CompletePreparation.slabCoordinates_bound {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} {anchor : Φ.flag.Node} {t : ℕ → ℕ} {δ : ℝ} (D : Φ.CompletePreparation anchor t δ) (hp : Odd p) (hδ : 0 ≤ δ) (hsmall : 3 ^ (d + 1) * δ < 1) (ht : Monotone t) (htsmall : ∀ (i : Fin D.count), 2 * t (↑i + 1) < p) (x : (D.split hp hδ hsmall).flag.Node) (v : FpCoord p d) (hv : (D.split hp hδ hsmall).cumulativeWeight x v ≠ 0) : latticeSupNorm (slabCoordinates (D.extra hp hδ hsmall x) D.chain.direction v) ≤ t D.count

theorem EGZ.FlagDecomposition.CompletePreparation.split_isKBounded {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} {anchor : Φ.flag.Node} {t : ℕ → ℕ} {δ : ℝ} (D : Φ.CompletePreparation anchor t δ) (hp : Odd p) (hδ : 0 ≤ δ) (hsmall : 3 ^ (d + 1) * δ < 1) {K : ℕ} (hK : Φ.IsKBounded fun (x : Φ.flag.Node) => K) : (D.split hp hδ hsmall).IsKBounded fun (x : (D.split hp hδ hsmall).flag.Node) => K

@[reducible, inline]

noncomputable abbrev EGZ.FlagDecomposition.CompletePreparation.diagram {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} {anchor : Φ.flag.Node} {t : ℕ → ℕ} {δ : ℝ} (D : Φ.CompletePreparation anchor t δ) (hp : Odd p) (hδ : 0 ≤ δ) (hsmall : 3 ^ (d + 1) * δ < 1) : LatticeSupportDiagram

Augmented lattice-support diagram associated with the preparation.

Equations

• D.diagram hp hδ hsmall = EGZ.FlagDecomposition.Augmented.diagram (D.split hp hδ hsmall) (D.extra hp hδ hsmall) D.chain.direction hp ⋯

theorem EGZ.FlagDecomposition.CompletePreparation.diagram_rank_le {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} {anchor : Φ.flag.Node} {t : ℕ → ℕ} {δ : ℝ} (D : Φ.CompletePreparation anchor t δ) (hp : Odd p) (hδ : 0 ≤ δ) (hsmall : 3 ^ (d + 1) * δ < 1) (x : (D.diagram hp hδ hsmall).Node) : (D.diagram hp hδ hsmall).rank x ≤ 2 * d

theorem EGZ.FlagDecomposition.CompletePreparation.diagram_support_bound {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} {anchor : Φ.flag.Node} {t : ℕ → ℕ} {δ : ℝ} (D : Φ.CompletePreparation anchor t δ) (hp : Odd p) (hδ : 0 ≤ δ) (hsmall : 3 ^ (d + 1) * δ < 1) {K : ℕ} (hK : Φ.IsKBounded fun (x : Φ.flag.Node) => K) (ht : Monotone t) (hKt : K ≤ t D.count) (htsmall : ∀ (i : Fin D.count), 2 * t (↑i + 1) < p) (x : (D.diagram hp hδ hsmall).Node) (q : IntCoord ((D.diagram hp hδ hsmall).rank x)) (hq : q ∈ (D.diagram hp hδ hsmall).support x) : latticeSupNorm q ≤ t D.count