OAI/Analysis/SeparableQuotients/PathStabilization.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SeparableQuotient.DiscreteDiagonal.exists_stabilizing_subsequence line 13

   Source documentation

   Countably many yes/no tests can be made eventually constant by one subsequence. The index set is arbitrary countable, not just natural numbers.

   lemma exists_stabilizing_subsequence {ι : Type*} [Countable ι] (p : ℕ → ι → Prop) :
       ∃ φ : ℕ → ℕ, StrictMono φ ∧ ∀ i, ∃ b : Prop,
         ∀ᶠ n in atTop, p (φ n) i ↔ b := by
   …

2. lemma OAI.SeparableQuotient.IncreasingLists.positions_stabilize line 35

   Source documentation

   Pointwise stabilization of membership in increasing finite lists, with an infinite limiting set, stabilizes every list position.

   lemma positions_stabilize (len : ℕ → ℕ) (v : ℕ → ℕ → ℕ)
       (hv : ∀ n, StrictMono (fun i : Fin (len n) => v n i)) (W : Set ℕ)
       (hW : W.Infinite)
       (hmem : ∀ w, ∀ᶠ n in atTop, (∃ i < len n, v n i = w) ↔ w ∈ W) :
       ∀ i, ∀ᶠ n in atTop, i < len n ∧ v n i = Nat.nth (· ∈ W) i := by
   …

3. lemma OAI.SeparableQuotient.IncreasingLists.infinite_of_windows line 72

   Source documentation

   Bounded windows of arbitrarily high eventual hits force the limiting membership set to be infinite. The upper window endpoints are essential.

   lemma infinite_of_windows (len : ℕ → ℕ) (v : ℕ → ℕ → ℕ) (W : Set ℕ)
       (hmem : ∀ w, ∀ᶠ n in atTop, (∃ i < len n, v n i = w) ↔ w ∈ W)
       (hwin : ∀ B, ∃ T, ∀ᶠ n in atTop, ∃ i < len n, B < v n i ∧ v n i ≤ T) :
       W.Infinite := by
   …

4. lemma OAI.SeparableQuotient.Norming.PrefixValid.support_subset_closure line 92
5. lemma OAI.SeparableQuotient.Norming.PrefixValid.piece_support_subset_closure line 99
6. lemma OAI.SeparableQuotient.Norming.PrefixValid.piece_eq_of_code_anchor line 106

   Source documentation

   A retained coordinate in a later piece anchors the compressed code in the actual ordinal labels. This is the finite-prefix version of path rigidity.

   lemma PrefixValid.piece_eq_of_code_anchor {P Q : RawPath} {len len' i j n : ℕ}
       (hP : PrefixValid P len) (hQ : PrefixValid Q len')
       (hn : n < len) (hn' : n < len') (hij : i < j) (hjn : j ≤ n)
       (hc : P.code n = Q.code n) (a : Γ)
       (ha : a ∈ (P.piece j).support) (ha' : a ∈ Q.closure n) :
       P.piece i = Q.piece i := by
   …

   Mentions: OAI.SeparableQuotient.Norming.PrefixValid, OAI.SeparableQuotient.Norming.Γ

7. lemma OAI.SeparableQuotient.Norming.finite_paths_stabilize line 125

   Source documentation

   Fixed successor weights and arbitrarily late retained coordinates force stabilization of the entire uncropped data, not just coordinatewise limits.

   lemma finite_paths_stabilize {f : Family} (P : ℕ → FinitePath f)
       (hlen : ∀ i, ∀ᶠ n in atTop, i < (P n).length)
       (hw : ∀ i, ∃ w, ∀ᶠ n in atTop, (P n).raw.weight i = w)
       (ha : ∀ i, ∃ j > i, ∃ a : Γ,
         ∀ᶠ n in atTop, a ∈ ((P n).raw.piece j).support) :
       ∀ i, ∃ d : Array × ℕ × ℕ, ∀ᶠ n in atTop,
         (P n).raw.piece i = d.1 ∧ (P n).raw.weight i = d.2.1 ∧
           (P n).raw.metadata i = d.2.2 := by
   …

   Mentions: OAI.SeparableQuotient.Norming.Family, OAI.SeparableQuotient.Norming.FinitePath, OAI.SeparableQuotient.Norming.Γ, OAI.SeparableQuotient.Norming.Array

8. lemma OAI.SeparableQuotient.Norming.raw_support_eq_of_prefix line 149
9. lemma OAI.SeparableQuotient.Norming.raw_code_eq_of_prefix line 157
10. lemma OAI.SeparableQuotient.Norming.infinite_path_of_stabilized line 174

    Source documentation

    Assemble the pointwise stabilized raw data into an actual infinite path. Type-I membership is witnessed by original finite-path pieces, never by an assumption that a limit belongs to the norming set.

    lemma infinite_path_of_stabilized {f : Family} (P : ℕ → FinitePath f)
        (hmem : ∀ n i j, ((P n).piece i).child j ∈ f.norming)
        (hlen : ∀ i, ∀ᶠ n in atTop, i < (P n).length)
        (hstable : ∀ i, ∃ d : Array × ℕ × ℕ, ∀ᶠ n in atTop,
          (P n).raw.piece i = d.1 ∧ (P n).raw.weight i = d.2.1 ∧
            (P n).raw.metadata i = d.2.2) :
        ∃ Q : InfinitePath f, ∀ i, ∀ᶠ n in atTop,
          (P n).raw.piece i = Q.raw.piece i ∧
          (P n).raw.weight i = Q.raw.weight i ∧
          (P n).raw.metadata i = Q.raw.metadata i := by
    …

    Mentions: OAI.SeparableQuotient.Norming.Family, OAI.SeparableQuotient.Norming.FinitePath, OAI.SeparableQuotient.Norming.Array, OAI.SeparableQuotient.Norming.InfinitePath

11. lemma OAI.SeparableQuotient.Norming.infinite_path_of_fixed_chain line 247
12. lemma OAI.SeparableQuotient.Norming.PrefixValid.index_le_weight line 265
13. lemma OAI.SeparableQuotient.Norming.path_of_recurrent_windows line 278

    Source documentation

    A compactness statement sufficient for the four-hits contradiction. Unlike weak-star compactness alone, it recovers one actual infinite coded path. Every high window has a finite upper endpoint and a finite possible coordinate set.

    lemma path_of_recurrent_windows {f : Family} (P : ℕ → FinitePath f)
        (hmem : ∀ n i j, ((P n).piece i).child j ∈ f.norming)
        (hwin : ∀ B : ℕ, ∃ T : ℕ, ∃ s : Finset Γ, ∀ᶠ n in atTop,
          ∃ i < (P n).length, B < (P n).raw.weight i ∧ (P n).raw.weight i ≤ T ∧
            ∃ a ∈ s, a ∈ ((P n).raw.piece i).support) :
        ∃ (φ : ℕ → ℕ) (Q : InfinitePath f), StrictMono φ ∧ ∀ i, ∀ᶠ n in atTop,
          i < (P (φ n)).length ∧ (P (φ n)).raw.piece i = Q.raw.piece i ∧
          (P (φ n)).raw.weight i = Q.raw.weight i ∧
          (P (φ n)).raw.metadata i = Q.raw.metadata i := by
    …

    Mentions: OAI.SeparableQuotient.Norming.Family, OAI.SeparableQuotient.Norming.FinitePath, OAI.SeparableQuotient.Norming.Γ, OAI.SeparableQuotient.Norming.InfinitePath

14. lemma OAI.SeparableQuotient.Norming.Family.m_mono line 339
15. lemma OAI.SeparableQuotient.Norming.FinitePath.at_piece line 342
16. lemma OAI.SeparableQuotient.Norming.FinitePath.coefficient_le line 358
17. def OAI.SeparableQuotient.Norming.InfinitePath.coordinateValue line 366

    Source documentation

    Coordinate value of the bounded infinite path functional.

    def InfinitePath.coordinateValue {f : Family} (P : InfinitePath f) (a : Γ) : ℚ :=
    …

    Mentions: OAI.SeparableQuotient.Norming.Family, OAI.SeparableQuotient.Norming.InfinitePath, OAI.SeparableQuotient.Norming.Γ

18. lemma OAI.SeparableQuotient.Norming.InfinitePath.prefix_coordinateValue line 369
19. lemma OAI.SeparableQuotient.Norming.InfinitePath.coordinateValue_at_hit line 373
20. lemma OAI.SeparableQuotient.Norming.InfinitePath.coordinateValue_zero line 379
21. lemma OAI.SeparableQuotient.Norming.stabilized_coordinate_tendsto line 388

    Source documentation

    Stabilization is on exact actual uncropped pieces. Any extra pieces escape in weight, and their coordinate coefficients tend to zero.

    lemma stabilized_coordinate_tendsto {f : Family} (P : ℕ → FinitePath f)
        (hm : ∀ n i j, ((P n).piece i).child j ∈ f.norming) (Q : InfinitePath f)
        (hst : ∀ i, ∀ᶠ n in atTop, i < (P n).length ∧
          (P n).raw.piece i = Q.raw.piece i ∧ (P n).raw.weight i = Q.raw.weight i)
        (a : Γ) : Tendsto (fun n => ((P n).value a : ℝ)) atTop (𝓝 (Q.coordinateValue a : ℝ)) := by
    …

    Mentions: OAI.SeparableQuotient.Norming.Family, OAI.SeparableQuotient.Norming.FinitePath, OAI.SeparableQuotient.Norming.InfinitePath, OAI.SeparableQuotient.Norming.Γ

22. lemma OAI.SeparableQuotient.ActualSpace.pathFunctional_finite line 439
23. lemma OAI.SeparableQuotient.ActualSpace.finitePath_mem_full line 449
24. def OAI.SeparableQuotient.ActualSpace.finitePathFunctional line 455
25. lemma OAI.SeparableQuotient.ActualSpace.norm_finitePathFunctional_le line 459
26. lemma OAI.SeparableQuotient.ActualSpace.stabilized_path_tendsto line 463