YoungestCrossing.lean`

28 declarations, 0 contain sorry, 0 declared as axioms

def OAI.BoundedTreewidthL1.InfinitesimalAlong line 8
def OAI.BoundedTreewidthL1.CrossingSequence line 13
Source documentation
A reservation interval whose effective start is early and terminal time is late. Validity is explicit; no anchor is created merely by taking a quotient.
```
def CrossingSequence {I : Type*} (U : Ultrafilter I)
    (valid : I → ℕ → Prop) (start finish : I → ℕ → ℕ)
    (δ : I → ℕ → ℝ) (a : I → ℕ) : Prop :=
…
```

def OAI.BoundedTreewidthL1.CrossingGerms line 21

Source documentation

Crossing anchor sequences identified precisely when they agree eventually.

def CrossingGerms {I : Type*} (U : Ultrafilter I)
    (valid : I → ℕ → Prop) (start finish : I → ℕ → ℕ) (δ : I → ℕ → ℝ) :
    Set (Germ (U : Filter I) ℕ) :=
…

lemma OAI.BoundedTreewidthL1.noninfinitesimal_iff line 32
lemma OAI.BoundedTreewidthL1.early_precedes_late line 46
lemma OAI.BoundedTreewidthL1.germ_total line 57

theorem OAI.BoundedTreewidthL1.crossing_family_card_le line 67

Source documentation

Any fixed finite collection of pairwise distinct crossing reservations is simultaneously present at the latest of its effective start times.

theorem crossing_family_card_le {I J : Type*} [Fintype J] (U : Ultrafilter I)
    (valid : I → ℕ → Prop) (start finish : I → ℕ → ℕ) (δ : I → ℕ → ℝ)
    (cache : I → ℕ → Finset ℕ) (N : ℕ)
    (hmono : ∀ i, Antitone (δ i))
    (hcache : ∀ i a t, valid i a → start i a ≤ t → t ≤ finish i a → a ∈ cache i t)
    (hsize : ∀ i t, (cache i t).card ≤ N)
    (a : J → I → ℕ) (ha : ∀ j, CrossingSequence U valid start finish δ (a j))
    (hdistinct : ∀ j k, j ≠ k → ∀ᶠ i in U, a j i ≠ a k i) :
    Fintype.card J ≤ N := by
…

Mentions: OAI.BoundedTreewidthL1.CrossingSequence

lemma OAI.BoundedTreewidthL1.crossing_finset_card_le line 115

theorem OAI.BoundedTreewidthL1.youngest_crossing line 140

Source documentation

The youngest crossing, with the inclusive cache bound and monotone normalized distances made explicit.

theorem youngest_crossing {I : Type*} (U : Ultrafilter I)
    (valid : I → ℕ → Prop) (start finish : I → ℕ → ℕ) (δ : I → ℕ → ℝ)
    (cache : I → ℕ → Finset ℕ) (N : ℕ)
    (hmono : ∀ i, Antitone (δ i))
    (hcache : ∀ i a t, valid i a → start i a ≤ t → t ≤ finish i a → a ∈ cache i t)
    (hsize : ∀ i t, (cache i t).card ≤ N)
    (hne : (CrossingGerms U valid start finish δ).Nonempty) :
    (CrossingGerms U valid start finish δ).Finite ∧
    (CrossingGerms U valid start finish δ).ncard ≤ N ∧
    ∃ youngest ∈ CrossingGerms U valid start finish δ,
      ∀ a ∈ CrossingGerms U valid start finish δ, a ≤ youngest := by
…

Mentions: OAI.BoundedTreewidthL1.CrossingGerms

def OAI.BoundedTreewidthL1.ReservationPath.Present line 179
def OAI.BoundedTreewidthL1.ReservationPath.Successor line 181
lemma OAI.BoundedTreewidthL1.ReservationPath.mem_inclusive line 185
lemma OAI.BoundedTreewidthL1.ReservationPath.proposal_present line 191
lemma OAI.BoundedTreewidthL1.ReservationPath.successor_exists line 194
lemma OAI.BoundedTreewidthL1.ReservationPath.proposal_retained_of_other_release line 207
lemma OAI.BoundedTreewidthL1.ReservationPath.successor_at_later_test line 217
Source documentation
Once b immediately follows a after an eviction test, no subsequent insertion can appear between them: new anchors have later launch times.
```
lemma successor_at_later_test (P : ReservationPath) (a b t u : ℕ)
    (hab : a < b) (hbt : b ≤ t) (htu : t < u)
    (ha : P.Present a u) (hb : P.Present b u)
    (hmin : ∀ c, a < c → c ≤ t → t < P.finish c → b ≤ c) :
    P.Successor a b u := by
…
```
Mentions: OAI.BoundedTreewidthL1.ReservationPath

lemma OAI.BoundedTreewidthL1.ReservationPath.retained_successor line 231

Source documentation

A surviving younger anchor exists after the last eviction of any younger anchor launched above S. The only use of protection is for a successor already launched at or after S.

lemma retained_successor (P : ReservationPath) (a S t : ℕ)
    (haS : a < S) (hSt : S ≤ t) (ht : t < P.last)
    (ha : t < P.finish a)
    (hold : ∀ c, a < c → c < S → P.finish c ≤ t)
    (hprotect : ∀ b, S ≤ b → P.Successor a b t → t < P.finish b) :
    ∃ b, a < b ∧ S ≤ b ∧ b ≤ t ∧ t < P.finish b ∧
      ∀ c, a < c → c ≤ t → t < P.finish c → b ≤ c := by
…

Mentions: OAI.BoundedTreewidthL1.ReservationPath

def OAI.BoundedTreewidthL1.PathCrossing line 270
lemma OAI.BoundedTreewidthL1.infinitesimal_congr line 276
lemma OAI.BoundedTreewidthL1.infinitesimal_mono line 286
lemma OAI.BoundedTreewidthL1.eventually_choose_nat line 293
theorem OAI.BoundedTreewidthL1.younger_crossing line 301
theorem OAI.BoundedTreewidthL1.cache_no_failure line 399
structure OAI.BoundedTreewidthL1.CacheControl line 444
Source documentation
Numerical interface to the actual cached ensemble. The three tests below are proved from that ensemble, rather than postulated in the embedding theorem.
```
structure CacheControl (N : ℕ) (Q H : ℝ) where
…
```
lemma OAI.BoundedTreewidthL1.infinitesimal_add_mul line 464
lemma OAI.BoundedTreewidthL1.CacheControl.no_failure line 474
theorem OAI.BoundedTreewidthL1.CacheControl.uniform_lower line 539
Source documentation
Compactness is used only on numerical cache data, not on random samplers or on a bounded number of vertices.
```
theorem CacheControl.uniform_lower (N : ℕ) (Q H : ℝ) (hQ : 0 < Q) :
    ∃ c : ℝ, 0 < c ∧ ∀ C : CacheControl N Q H, c ≤ C.error := by
…
```
Mentions: OAI.BoundedTreewidthL1.CacheControl
theorem OAI.BoundedTreewidthL1.protected_threshold line 563