Geometric lineages for finite progress intervals

Finite comparisons extend by identity maps after their endpoint. The extension requires no progress certificate, event, or unsatisfied condition at the constant stages.

structure EGZ.FlagDecomposition.LineageStep {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} (Φ Ψ : FlagDecomposition p d f) : Type

The comparison data of one step, independently of its event.

• subdivision : Φ.SubdivisionMap Ψ

  The subdivision map sending each descendant node to its parent in the previous decomposition.

• cutoff : ℕ

  The largest level up to which the lineage step supplies stable and injective node transport.

• level_parent (y : Ψ.flag.Node) : Φ.level (self.subdivision.node y) ≤ Ψ.level y
• stable (y : Ψ.flag.Node) : Ψ.level y ≤ self.cutoff → Φ.StableNodeMap Ψ (self.subdivision.node y) y

  The stable node maps for descendants whose levels do not exceed the cutoff.

• stable_real (y : Ψ.flag.Node) (h : Ψ.level y ≤ self.cutoff) : (self.stable y h).coord.real = self.subdivision.fibre y
• injective_below : Set.InjOn ⇑self.subdivision.node {y : Ψ.flag.Node | Ψ.level y ≤ self.cutoff}

def EGZ.FlagDecomposition.LineageStep.refl {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (K : ℕ) : Φ.LineageStep Φ

The identity lineage step with an arbitrary prescribed cutoff.

Equations

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

def EGZ.FlagDecomposition.LineageStep.ofEq {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ Ψ : FlagDecomposition p d f} (h : Ψ = Φ) (K : ℕ) : Φ.LineageStep Ψ

The identity lineage step transported across an equality of decompositions.

Equations

• EGZ.FlagDecomposition.LineageStep.ofEq h K = ⋯ ▸ EGZ.FlagDecomposition.LineageStep.refl Φ K

@[simp]

theorem EGZ.FlagDecomposition.LineageStep.ofEq_cutoff {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ Ψ : FlagDecomposition p d f} (h : Ψ = Φ) (K : ℕ) : (ofEq h K).cutoff = K

noncomputable def EGZ.FlagDecomposition.LineageStep.ofProgress {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {s t : Iteration.State p d f} {ε δ : ℝ} {g : ℕ → ℕ} (P : Iteration.Progress s t ε δ g) : s.decomposition.LineageStep t.decomposition

The lineage step supplied by an iteration progress certificate.

Equations

• EGZ.FlagDecomposition.LineageStep.ofProgress P = { subdivision := P.subdivision, cutoff := P.event.cutoff, level_parent := ⋯, stable := P.stable, stable_real := ⋯, injective_below := ⋯ }

def EGZ.FlagDecomposition.LineageMassMaps.ofSteps {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : ℕ → FlagDecomposition p d f} (hminimal : ∀ (i : ℕ), (Φ i).IsMinimal) (D : (i : ℕ) → (Φ i).LineageStep (Φ (i + 1))) : LineageMassMaps Φ

The lineage mass maps assembled from consecutive lineage steps of minimal decompositions.

Equations

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

noncomputable def EGZ.FlagDecomposition.LineageMassMaps.stopped {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : ℕ → FlagDecomposition p d f} (hminimal : ∀ (i : ℕ), (Φ i).IsMinimal) (n K : ℕ) (hstop : ∀ (i : ℕ), n ≤ i → Φ (i + 1) = Φ i) (D : (i : ℕ) → i < n → (Φ i).LineageStep (Φ (i + 1))) : LineageMassMaps Φ

Extend a finite list of comparisons on an already stopped sequence.

Equations

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

@[simp]

theorem EGZ.FlagDecomposition.LineageMassMaps.stopped_step_of_lt {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : ℕ → FlagDecomposition p d f} (hminimal : ∀ (i : ℕ), (Φ i).IsMinimal) (n K : ℕ) (hstop : ∀ (i : ℕ), n ≤ i → Φ (i + 1) = Φ i) (D : (i : ℕ) → i < n → (Φ i).LineageStep (Φ (i + 1))) (i : ℕ) (hi : i < n) : (stopped hminimal n K hstop D).step i = (D i hi).subdivision

@[simp]

theorem EGZ.FlagDecomposition.LineageMassMaps.stopped_cutoff_of_lt {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : ℕ → FlagDecomposition p d f} (hminimal : ∀ (i : ℕ), (Φ i).IsMinimal) (n K : ℕ) (hstop : ∀ (i : ℕ), n ≤ i → Φ (i + 1) = Φ i) (D : (i : ℕ) → i < n → (Φ i).LineageStep (Φ (i + 1))) (i : ℕ) (hi : i < n) : (stopped hminimal n K hstop D).cutoff i = (D i hi).cutoff

theorem EGZ.FlagDecomposition.LineageMassMaps.stopped_cutoff_ge {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : ℕ → FlagDecomposition p d f} (hminimal : ∀ (i : ℕ), (Φ i).IsMinimal) (n K : ℕ) (hstop : ∀ (i : ℕ), n ≤ i → Φ (i + 1) = Φ i) (D : (i : ℕ) → i < n → (Φ i).LineageStep (Φ (i + 1))) {L : ℕ} (hLK : L ≤ K) (hcut : ∀ (i : ℕ) (hi : i < n), L ≤ (D i hi).cutoff) (i : ℕ) : L ≤ (stopped hminimal n K hstop D).cutoff i

@[reducible, inline]

abbrev EGZ.FlagDecomposition.Iteration.intervalState {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} (s : ℕ → State p d f) (a n i : ℕ) : State p d f

Restart at a and hold the state constant after n further steps.

Equations

• EGZ.FlagDecomposition.Iteration.intervalState s a n i = s (a + min i n)

theorem EGZ.FlagDecomposition.Iteration.intervalState_eq {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} (s : ℕ → State p d f) (a n i : ℕ) (hi : i ≤ n) : intervalState s a n i = s (a + i)

theorem EGZ.FlagDecomposition.Iteration.intervalState_succ_eq {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} (s : ℕ → State p d f) (a n i : ℕ) (hi : n ≤ i) : intervalState s a n (i + 1) = intervalState s a n i

noncomputable def EGZ.FlagDecomposition.Iteration.stoppedLineageMassMaps {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {s : ℕ → State p d f} {ε : ℝ} {δ : ℕ → ℝ} {g : ℕ → ℕ} (n : ℕ) (hstop : ∀ (i : ℕ), n ≤ i → s (i + 1) = s i) (P : (i : ℕ) → i < n → Progress (s i) (s (i + 1)) ε (δ i) g) : LineageMassMaps fun (i : ℕ) => (s i).decomposition

The geometric comparison sequence of a genuinely finite progress list.

Equations

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

@[simp]

theorem EGZ.FlagDecomposition.Iteration.stoppedLineageMassMaps_step {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {s : ℕ → State p d f} {ε : ℝ} {δ : ℕ → ℝ} {g : ℕ → ℕ} (n : ℕ) (hstop : ∀ (i : ℕ), n ≤ i → s (i + 1) = s i) (P : (i : ℕ) → i < n → Progress (s i) (s (i + 1)) ε (δ i) g) (i : ℕ) (hi : i < n) : (stoppedLineageMassMaps n hstop P).step i = (P i hi).subdivision

theorem EGZ.FlagDecomposition.Iteration.stoppedLineageMassMaps_cutoff_ge {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {s : ℕ → State p d f} {ε : ℝ} {δ : ℕ → ℝ} {g : ℕ → ℕ} (n : ℕ) (hstop : ∀ (i : ℕ), n ≤ i → s (i + 1) = s i) (P : (i : ℕ) → i < n → Progress (s i) (s (i + 1)) ε (δ i) g) {L : ℕ} (hL : L ≤ (d + 1) ^ 2) (hcolors : ∀ (i : ℕ) (hi : i < n), 2 * L ≤ (P i hi).event.color) (i : ℕ) : L ≤ (stoppedLineageMassMaps n hstop P).cutoff i

def EGZ.FlagDecomposition.Iteration.Progress.castStates {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {s t s' t' : State p d f} {ε δ : ℝ} {g : ℕ → ℕ} (Q : Progress s t ε δ g) (hs : s' = s) (ht : t' = t) : Progress s' t' ε δ g

Transport a progress certificate across equalities of its source and target states.

Equations

• Q.castStates hs ht = ⋯ ▸ ⋯ ▸ Q

@[simp]

theorem EGZ.FlagDecomposition.Iteration.Progress.castStates_event_color {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {s t s' t' : State p d f} {ε δ : ℝ} {g : ℕ → ℕ} (Q : Progress s t ε δ g) (hs : s' = s) (ht : t' = t) : (Q.castStates hs ht).event.color = Q.event.color

def EGZ.FlagDecomposition.Iteration.intervalProgress {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {s : ℕ → State p d f} {ε : ℝ} {δ : ℕ → ℝ} {g : ℕ → ℕ} {N : ℕ} (P : (i : ℕ) → i < N → Progress (s i) (s (i + 1)) ε (δ i) g) (a n : ℕ) (h : a + n ≤ N) (i : ℕ) (hi : i < n) : Progress (intervalState s a n i) (intervalState s a n (i + 1)) ε (δ (a + i)) g

A genuine original progress certificate on a shifted, stopped interval.

Equations

• EGZ.FlagDecomposition.Iteration.intervalProgress P a n h i hi = (P (a + i) ⋯).castStates ⋯ ⋯

@[simp]

theorem EGZ.FlagDecomposition.Iteration.intervalProgress_event_color {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {s : ℕ → State p d f} {ε : ℝ} {δ : ℕ → ℝ} {g : ℕ → ℕ} {N : ℕ} (P : (i : ℕ) → i < N → Progress (s i) (s (i + 1)) ε (δ i) g) (a n : ℕ) (h : a + n ≤ N) (i : ℕ) (hi : i < n) : (intervalProgress P a n h i hi).event.color = (P (a + i) ⋯).event.color

noncomputable def EGZ.FlagDecomposition.Iteration.intervalLineageMassMaps {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {s : ℕ → State p d f} {ε : ℝ} {δ : ℕ → ℝ} {g : ℕ → ℕ} {N : ℕ} (P : (i : ℕ) → i < N → Progress (s i) (s (i + 1)) ε (δ i) g) (a n : ℕ) (h : a + n ≤ N) : LineageMassMaps fun (i : ℕ) => (intervalState s a n i).decomposition

The lineage mass maps for a finite interval of an iteration, held constant after its endpoint.

Equations

• EGZ.FlagDecomposition.Iteration.intervalLineageMassMaps P a n h = EGZ.FlagDecomposition.Iteration.stoppedLineageMassMaps n ⋯ (EGZ.FlagDecomposition.Iteration.intervalProgress P a n h)

@[simp]

theorem EGZ.FlagDecomposition.Iteration.intervalLineageMassMaps_step {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {s : ℕ → State p d f} {ε : ℝ} {δ : ℕ → ℝ} {g : ℕ → ℕ} {N : ℕ} (P : (i : ℕ) → i < N → Progress (s i) (s (i + 1)) ε (δ i) g) (a n : ℕ) (h : a + n ≤ N) (i : ℕ) (hi : i < n) : (intervalLineageMassMaps P a n h).step i = (intervalProgress P a n h i hi).subdivision

theorem EGZ.FlagDecomposition.Iteration.intervalLineageMassMaps_cutoff_ge {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {s : ℕ → State p d f} {ε : ℝ} {δ : ℕ → ℝ} {g : ℕ → ℕ} {N : ℕ} (P : (i : ℕ) → i < N → Progress (s i) (s (i + 1)) ε (δ i) g) (a n : ℕ) (h : a + n ≤ N) {L : ℕ} (hL : L ≤ (d + 1) ^ 2) (hcolors : ∀ (i : ℕ) (hi : i < n), 2 * L ≤ (P (a + i) ⋯).event.color) (i : ℕ) : L ≤ (intervalLineageMassMaps P a n h).cutoff i