Preparing a complete-element refinement

Choose the maximal thin directions, prune only below the selected anchor, and transfer its surviving local mass to a lower layer. This produces an actual flag decomposition, with controlled mass loss and a non-reduced old upper anchor, before adjoining the new slab coordinates.

structure EGZ.FlagDecomposition.CompletePreparation {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (t : ℕ → ℕ) (δ : ℝ) : Type

A bounded chain of thin directions used to prepare a complete refinement.

• count : ℕ

  Number of selected thin directions.

• count_le : self.count ≤ d
• chain : DirectionChain (Φ.representation.fiberConstantSubmodule anchor) (fun (i : ℕ) (ξ : FpCoord p d →ᵃ[ZMod p] ZMod p) => IsThinAlong (Φ.cumulativeWeight anchor) ξ (t (i + 1)) (3 ^ (i + 1) * δ)) self.count

  Chain witnessing thinness in the selected directions at their prescribed scales.

• maximal (ξ : FpCoord p d →ᵃ[ZMod p] ZMod p) : ξ ∉ self.chain.space self.count → IsThickAlong (Φ.cumulativeWeight anchor) ξ (t (self.count + 1)) (3 ^ (self.count + 1) * δ)

theorem EGZ.FlagDecomposition.nonempty_completePreparation {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (t : ℕ → ℕ) (δ : ℝ) : Nonempty (Φ.CompletePreparation anchor t δ)

def EGZ.FlagDecomposition.CompletePreparation.selectedSet {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} {anchor : Φ.flag.Node} {t : ℕ → ℕ} {δ : ℝ} (D : Φ.CompletePreparation anchor t δ) : Set (FpCoord p d)

Intersection of the slabs selected by the direction chain.

Equations

• D.selectedSet = EGZ.slabIntersection D.count D.chain.direction t

theorem EGZ.FlagDecomposition.CompletePreparation.selected_nonzero {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} {anchor : Φ.flag.Node} {t : ℕ → ℕ} {δ : ℝ} (D : Φ.CompletePreparation anchor t δ) (hδ : 0 ≤ δ) (hsmall : 3 ^ (d + 1) * δ < 1) : ∃ (v : FpCoord p d), restrictWeight (Φ.cumulativeWeight anchor) D.selectedSet v ≠ 0

@[reducible, inline]

noncomputable abbrev EGZ.FlagDecomposition.CompletePreparation.pruned {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) : FlagDecomposition p d f

Decomposition obtained by pruning to the selected slab intersection.

Equations

• D.pruned hp hδ hsmall = EGZ.FlagDecomposition.LocalizedPruning.decomposition Φ anchor D.selectedSet ⋯ hp

@[reducible, inline]

noncomputable abbrev EGZ.FlagDecomposition.CompletePreparation.prunedAnchor {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) : (D.pruned hp hδ hsmall).flag.Node

Distinguished anchor in the pruned decomposition.

Equations

• D.prunedAnchor hp hδ hsmall = EGZ.FlagDecomposition.LocalizedPruning.anchorNode Φ anchor D.selectedSet ⋯ hp

@[reducible, inline]

noncomputable abbrev EGZ.FlagDecomposition.CompletePreparation.split {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) : FlagDecomposition p d f

Two-layer decomposition obtained by splitting the pruned anchor.

Equations

• D.split hp hδ hsmall = EGZ.FlagDecomposition.LowerTransfer.decomposition (D.pruned hp hδ hsmall) (D.prunedAnchor hp hδ hsmall) hp

@[reducible, inline]

noncomputable abbrev EGZ.FlagDecomposition.CompletePreparation.lowerAnchor {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) : (D.split hp hδ hsmall).flag.Node

Lower copy of the anchor after splitting.

Equations

• D.lowerAnchor hp hδ hsmall = EGZ.FlagDecomposition.LowerTransfer.lowerAnchor (D.pruned hp hδ hsmall) (D.prunedAnchor hp hδ hsmall) hp

@[reducible, inline]

noncomputable abbrev EGZ.FlagDecomposition.CompletePreparation.upperAnchor {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) : (D.split hp hδ hsmall).flag.Node

Upper copy of the anchor after splitting.

Equations

• D.upperAnchor hp hδ hsmall = EGZ.FlagDecomposition.LowerTransfer.upper (D.pruned hp hδ hsmall) (D.prunedAnchor hp hδ hsmall) hp (D.prunedAnchor hp hδ hsmall)

theorem EGZ.FlagDecomposition.CompletePreparation.lowerAnchor_cumulativeWeight {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) : (D.split hp hδ hsmall).cumulativeWeight (D.lowerAnchor hp hδ hsmall) = restrictWeight (Φ.cumulativeWeight anchor) D.selectedSet

theorem EGZ.FlagDecomposition.CompletePreparation.lowerAnchor_space {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) : (D.split hp hδ hsmall).representation.space (D.lowerAnchor hp hδ hsmall) = Φ.representation.space anchor

theorem EGZ.FlagDecomposition.CompletePreparation.lowerAnchor_map {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) : (D.split hp hδ hsmall).representation.map (D.lowerAnchor hp hδ hsmall) = Φ.representation.map anchor

theorem EGZ.FlagDecomposition.CompletePreparation.upperAnchor_not_isReducedElement {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) : ¬(D.split hp hδ hsmall).IsReducedElement (D.upperAnchor hp hδ hsmall)

theorem EGZ.FlagDecomposition.CompletePreparation.retainedMass_loss {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) : ↑Φ.retainedMass - ↑(D.split hp hδ hsmall).retainedMass = ↑(natMass (Φ.cumulativeWeight anchor)) - ↑(natMass (restrictWeight (Φ.cumulativeWeight anchor) D.selectedSet))

theorem EGZ.FlagDecomposition.CompletePreparation.retainedMass_loss_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) : ↑Φ.retainedMass - ↑(D.split hp hδ hsmall).retainedMass ≤ 3 ^ (d + 1) * δ * ↑(natMass (Φ.cumulativeWeight anchor))

theorem EGZ.FlagDecomposition.CompletePreparation.card_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) : Fintype.card (D.split hp hδ hsmall).flag.Node ≤ 2 * Fintype.card Φ.flag.Node

noncomputable def EGZ.FlagDecomposition.CompletePreparation.subdivisionMap {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) : Φ.SubdivisionMap (D.split hp hδ hsmall)

Forget the lower-layer labels and recover a proper point of the old flag.

Equations

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

@[reducible, inline]

noncomputable abbrev EGZ.FlagDecomposition.CompletePreparation.extra {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) : (D.split hp hδ hsmall).flag.Node → ℕ

Number of additional coordinates assigned to each split node.

Equations

• D.extra hp hδ hsmall = EGZ.FlagDecomposition.LowerTransfer.extra (D.pruned hp hδ hsmall) (D.prunedAnchor hp hδ hsmall) hp D.count

theorem EGZ.FlagDecomposition.CompletePreparation.extra_antitone {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) : Antitone (D.extra hp hδ hsmall)

theorem EGZ.FlagDecomposition.CompletePreparation.extra_lowerAnchor {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) : D.extra hp hδ hsmall (D.lowerAnchor hp hδ hsmall) = D.count

theorem EGZ.FlagDecomposition.CompletePreparation.extra_upperAnchor {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) : D.extra hp hδ hsmall (D.upperAnchor hp hδ hsmall) = 0