OAI/Analysis/SeparableQuotients/PathConvergence.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SeparableQuotient.PathSelection.threshold_selection line 13

   Source documentation

   A finite threshold selection procedure for quantitative overlap bounds.

   lemma threshold_selection {Λ : Type u} (f : Λ → ℕ → ℝ) (M δ : ℝ)
       (hM : ∀ a n, |f a n| ≤ M) (N : ℕ)
       (hcap : ∀ (s : Finset Λ) (φ : ℕ → ℕ), StrictMono φ →
         (∀ a ∈ s, ∀ n, δ < |f a (φ n)|) → s.card ≤ N) :
       ∃ φ : ℕ → ℕ, StrictMono φ ∧
         ∀ a, CauchySeq (fun n => f a (φ n)) ∨ ∀ᶠ n in atTop, |f a (φ n)| ≤ δ := by
   …

2. structure OAI.SeparableQuotient.PathSelection.Nested line 60

   Source documentation

   A genuinely nested sequence of subsequences, with the usual diagonal map.

   structure Nested where
   …

3. def OAI.SeparableQuotient.PathSelection.Nested.diag line 65
4. lemma OAI.SeparableQuotient.PathSelection.Nested.represent line 67
5. lemma OAI.SeparableQuotient.PathSelection.Nested.diag_strictMono line 76
6. lemma OAI.SeparableQuotient.PathSelection.Nested.eventually_diag line 84
7. lemma OAI.SeparableQuotient.PathSelection.Nested.cauchy_diag line 93
8. lemma OAI.SeparableQuotient.PathSelection.simultaneous_cauchy line 114

   Source documentation

   Simultaneous convergence on an arbitrary, possibly uncountable, path family. Only finite quantitative overlap bounds are required.

   lemma simultaneous_cauchy {Λ : Type u} (f : Λ → ℕ → ℝ) (M : ℝ)
       (hM : ∀ a n, |f a n| ≤ M)
       (hcap : ∀ δ : ℝ, 0 < δ → ∃ N : ℕ,
         ∀ (s : Finset Λ) (φ : ℕ → ℕ), StrictMono φ →
           (∀ a ∈ s, ∀ n, δ < |f a (φ n)|) → s.card ≤ N) :
       ∃ φ : ℕ → ℕ, StrictMono φ ∧ ∀ a, CauchySeq (fun n => f a (φ n)) := by
   …

9. lemma OAI.SeparableQuotient.PathSelection.power_cap line 162
10. def OAI.SeparableQuotient.Norming.PathIndex line 188

    Source documentation

    Paths are indexed by their full raw data, not by an arbitrary chosen expression witnessing membership. The witness is retained when used.

    def PathIndex (f : Family) := {r : RawPath // ∃ P : InfinitePath f, P.raw = r}

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

11. def OAI.SeparableQuotient.Norming.PathIndex.repr line 190
12. lemma OAI.SeparableQuotient.Norming.PathIndex.repr_raw line 192
13. lemma OAI.SeparableQuotient.Norming.PathIndex.repr_injective line 195
14. lemma OAI.SeparableQuotient.ActualSpace.real_tail_bound line 210
15. lemma OAI.SeparableQuotient.ActualSpace.exists_tail_estimate line 222
16. lemma OAI.SeparableQuotient.ActualSpace.tail_abs_sum_bound line 236
17. def OAI.SeparableQuotient.ActualSpace.PredualNull line 264

    Source documentation

    Bounded blocks are null on the coordinate predual. This intermediate property is stated separately so that the path argument works for any such sequence, not just a chosen block representation.

    def PredualNull (x : ℕ → E) : Prop :=
    …

    Mentions: OAI.SeparableQuotient.ActualSpace.E

18. lemma OAI.SeparableQuotient.ActualSpace.path_threshold_cap line 267
19. lemma OAI.SeparableQuotient.ActualSpace.path_all_cauchy line 308
20. lemma OAI.SeparableQuotient.DenseZero.tendsto_zero_of_dense line 327
21. lemma OAI.SeparableQuotient.ActualSpace.predualNull_of_coordinates line 364
22. structure OAI.SeparableQuotient.ActualSpace.BlockSequence line 390

    Source documentation

    Admissible block sequences with real coefficients. Pure mode requires one color, mixed mode both orders.

    structure BlockSequence (f : Family) where
    …

23. def OAI.SeparableQuotient.ActualSpace.BlockSequence.embed line 397
24. lemma OAI.SeparableQuotient.ActualSpace.BlockSequence.coordinate_eventually_zero line 400
25. lemma OAI.SeparableQuotient.ActualSpace.BlockSequence.predualNull line 415
26. lemma OAI.SeparableQuotient.ActualSpace.pathFunctional_eq_of_raw line 421
27. lemma OAI.SeparableQuotient.ActualSpace.BlockSequence.all_paths_cauchy line 434

    Source documentation

    Every bounded block sequence has a subsequence on which every path functional converges.

    lemma BlockSequence.all_paths_cauchy {f : Family} (x : BlockSequence f) (M : ℝ)
        (hM : ∀ n, ‖x.embed n‖ ≤ M) :
        ∃ φ : ℕ → ℕ, StrictMono φ ∧ ∀ P : InfinitePath f,
          CauchySeq (fun n => pathFunctional P (x.embed (φ n))) := by
    …

    Mentions: OAI.SeparableQuotient.ActualSpace.BlockSequence, OAI.SeparableQuotient.ActualSpace.pathFunctional