OAI/Analysis/SeparableQuotients/PathRigidity.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SeparableQuotient.Norming.FinitePath.weightCrop line 12

   Source documentation

   Legal crop selecting an interval of original weights, without recoding.

   def FinitePath.weightCrop {f : Family} (P : FinitePath f) (J T : ℕ) : Crop where
   …

   Mentions: OAI.SeparableQuotient.Norming.Family, OAI.SeparableQuotient.Norming.FinitePath, OAI.SeparableQuotient.Norming.Crop

2. lemma OAI.SeparableQuotient.Norming.FinitePath.weightCrop_set line 22
3. lemma OAI.SeparableQuotient.Norming.FinitePath.weightCrop_piece line 26
4. def OAI.SeparableQuotient.Norming.FinitePath.window line 54
5. def OAI.SeparableQuotient.Norming.FinitePath.windowWeights line 57
6. lemma OAI.SeparableQuotient.Norming.FinitePath.weightCrop_value line 61
7. lemma OAI.SeparableQuotient.Norming.FinitePath.weightCrop_active line 65
8. lemma OAI.SeparableQuotient.Norming.FinitePath.mem_windowWeights line 75
9. def OAI.SeparableQuotient.ActualSpace.croppedPathFunctional line 92
10. lemma OAI.SeparableQuotient.ActualSpace.rational_cropped_path_bound line 95
11. lemma OAI.SeparableQuotient.ActualSpace.real_cropped_path_bound line 112
12. lemma OAI.SeparableQuotient.ActualSpace.cropped_abs_sum_bound line 121
13. lemma OAI.SeparableQuotient.ActualSpace.window_disjoint_cap line 141
14. def OAI.SeparableQuotient.Norming.FinitePath.lowHistory line 171

    Source documentation

    Actual pieces, original weights, and original metadata below a threshold. This is deliberately not the compressed history, nor a cropped code.

    def FinitePath.lowHistory {f : Family} (P : FinitePath f) (J : ℕ) : Set (Array × ℕ × ℕ) :=
    …

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

15. lemma OAI.SeparableQuotient.Norming.PrefixValid.metadata_mono line 175
16. lemma OAI.SeparableQuotient.Norming.FinitePath.code_of_shared_weight line 181
17. lemma OAI.SeparableQuotient.Norming.closure_downward_rho line 194
18. lemma OAI.SeparableQuotient.Norming.PrefixValid.low_piece_eq_of_anchors line 203

    Source documentation

    Two agreeing compressed histories whose later pieces meet one finite coordinate set with sufficiently small rho have identical actual earlier pieces. The anchors may be different coordinates and different pieces.

    lemma PrefixValid.low_piece_eq_of_anchors {P Q : RawPath} {len len' n i j k : ℕ}
        (hP : PrefixValid P len) (hQ : PrefixValid Q len')
        (hn : n < len) (hn' : n < len') (hc : P.code n = Q.code n)
        (hij : i < j) (hik : i < k) (hjn : j ≤ n) (hkn : k ≤ n)
        (a b : Γ) (ha : a ∈ (P.piece j).support) (hb : b ∈ (Q.piece k).support)
        (hr : rho (min a b) (max a b) ≤ P.metadata n) : P.piece i = Q.piece i := by
    …

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

19. lemma OAI.SeparableQuotient.Norming.FinitePath.lowHistory_eq_of_code_anchors line 224
20. lemma OAI.SeparableQuotient.Norming.FinitePath.lowHistory_eq_of_shared_later_weight line 267
21. def OAI.SeparableQuotient.Norming.FinitePath.lowHistoryFinset line 302
22. lemma OAI.SeparableQuotient.Norming.FinitePath.mem_lowHistoryFinset line 306
23. lemma OAI.SeparableQuotient.Norming.FinitePath.window_eq_sum_lowHistory line 316
24. lemma OAI.SeparableQuotient.Norming.FinitePath.window_eq_of_lowHistory line 330
25. def OAI.SeparableQuotient.ActualSpace.LegalFinitePath line 344

    Source documentation

    A finite path with its original finite-stage children.

    def LegalFinitePath (f : Family) := {P : FinitePath f // ∀ i j, (P.piece i).child j ∈ f.norming}

26. def OAI.SeparableQuotient.ActualSpace.WindowHit line 346
27. lemma OAI.SeparableQuotient.ActualSpace.window_anchor line 349
28. lemma OAI.SeparableQuotient.ActualSpace.WindowHit.anchor line 364
29. lemma OAI.SeparableQuotient.ActualSpace.disjoint_of_different_histories line 372

    Source documentation

    Rigidity of two path histories with shared later weights.

    lemma disjoint_of_different_histories {f : Family} (P Q : LegalFinitePath f)
        (x : Γ →₀ ℝ) (Jv Tv Jt Tt Jk Tk : ℕ) (hvt : Tv < Jt) (htk : Tt < Jk)
        (δ : ℝ) (hδ : 0 < δ)
        (hp : WindowHit P x Jv Tv δ) (hq : WindowHit Q x Jv Tv δ)
        (ht : ∃ t : Fin P.val.length, Jt ≤ P.val.raw.weight t ∧ P.val.raw.weight t ≤ Tt)
        (hr : ∀ a ∈ x.support, ∀ b ∈ x.support, rho (min a b) (max a b) ≤ Jt)
        (hne : P.val.lowHistory Jv ≠ Q.val.lowHistory Jv) :
        Disjoint (P.val.windowWeights Jk Tk) (Q.val.windowWeights Jk Tk) := by
    …

    Mentions: OAI.SeparableQuotient.ActualSpace.LegalFinitePath, OAI.SeparableQuotient.ActualSpace.WindowHit

30. lemma OAI.SeparableQuotient.ActualSpace.finite_window_covers line 395

    Source documentation

    Uniform finite covers from the history-class argument.

    lemma finite_window_covers {f : Family} (x : ℕ → Γ →₀ ℝ) (J T : ℕ → ℕ)
        (horder : ∀ i j, i < j → T i < J j)
        (hcoh : ∀ i j, i < j → ∀ a ∈ (x i).support, ∀ b ∈ (x i).support,
          rho (min a b) (max a b) ≤ J j)
        (M δ : ℝ) (hM : ∀ i, ‖norming.includeFinite (x i)‖ ≤ M) (hδ : 0 < δ)
        (hall : ∀ w v t k : ℕ, w < v → v < t → t < k →
          ∃ P : LegalFinitePath f, WindowHit P (x w) (J w) (T w) δ ∧
            WindowHit P (x v) (J v) (T v) δ ∧ WindowHit P (x t) (J t) (T t) δ ∧
            WindowHit P (x k) (J k) (T k) δ) :
        ∃ D : ℕ, ∀ n, ∃ R : Finset (LegalFinitePath f), R.card ≤ D ∧
          ∀ i ≤ n, ∃ P ∈ R, WindowHit P (x i) (J i) (T i) δ := by
    …

    Mentions: OAI.SeparableQuotient.ActualSpace.LegalFinitePath, OAI.SeparableQuotient.ActualSpace.WindowHit