OAI/Analysis/SeparableQuotients/PathLimits.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SeparableQuotient.PathLimits.unit_bound line 13
2. lemma OAI.SeparableQuotient.PathLimits.cauchy_of_dense line 17
3. lemma OAI.SeparableQuotient.PathLimits.exists_limit_of_dense line 40

   Source documentation

   Bounded pointwise convergence on a dense set determines an actual bounded functional on the completed space; no weak-star sequential compactness is used.

   lemma exists_limit_of_dense (f : ℕ → StrongDual ℝ Z) (hf : ∀ n, ‖f n‖ ≤ 1)
       (D : Set Z) (hD : Dense D) (h : ∀ x ∈ D, CauchySeq (fun n => f n x)) :
       ∃ P : StrongDual ℝ Z, ‖P‖ ≤ 1 ∧ ∀ x, Tendsto (fun n => f n x) atTop (𝓝 (P x)) := by
   …

4. def OAI.SeparableQuotient.Norming.Family.base line 61
5. def OAI.SeparableQuotient.Norming.Family.norming line 65
6. lemma OAI.SeparableQuotient.Norming.Family.norming_subset_full line 67
7. lemma OAI.SeparableQuotient.Norming.common_stage line 72
8. lemma OAI.SeparableQuotient.Norming.TypeI.mem_family line 78
9. lemma OAI.SeparableQuotient.Norming.TypeII.mem_family line 83
10. lemma OAI.SeparableQuotient.Norming.admissible_prefix line 90
11. structure OAI.SeparableQuotient.Norming.InfinitePath line 101

    Source documentation

    Actual infinite paths retain all original Type I expressions, weights, and uncropped metadata. No completion of the coding tree is inserted as a path.

    structure InfinitePath (f : Family) where
    …

    Mentions: OAI.SeparableQuotient.Norming.Family

12. def OAI.SeparableQuotient.Norming.InfinitePath.prefix line 110
13. def OAI.SeparableQuotient.Norming.FinitePath.oneTerm line 120
14. lemma OAI.SeparableQuotient.Norming.FinitePath.oneTerm_value line 128
15. lemma OAI.SeparableQuotient.Norming.InfinitePath.prefix_crop_mem line 133
16. lemma OAI.SeparableQuotient.Norming.InfinitePath.prefix_mem line 138
17. lemma OAI.SeparableQuotient.Norming.InfinitePath.piece_coefficient_unique line 143
18. lemma OAI.SeparableQuotient.Norming.InfinitePath.prefix_at_hit line 154
19. lemma OAI.SeparableQuotient.Norming.InfinitePath.prefix_coordinate_eventually_constant line 164
20. def OAI.SeparableQuotient.ActualSpace.pathPartial line 183
21. lemma OAI.SeparableQuotient.ActualSpace.pathPartial_bound line 186
22. lemma OAI.SeparableQuotient.ActualSpace.pathPartial_finite_cauchy line 189
23. lemma OAI.SeparableQuotient.ActualSpace.exists_pathFunctional line 202
24. def OAI.SeparableQuotient.ActualSpace.pathFunctional line 209

    Source documentation

    Path partial sums are bounded and converge pointwise.

    def pathFunctional {f : Family} (P : InfinitePath f) : StrongDual ℝ E :=
    …

    Mentions: OAI.SeparableQuotient.ActualSpace.E

25. lemma OAI.SeparableQuotient.ActualSpace.norm_pathFunctional_le line 212
26. lemma OAI.SeparableQuotient.ActualSpace.pathPartial_tendsto line 215
27. def OAI.SeparableQuotient.Norming.InfinitePath.tailCrop line 225
28. lemma OAI.SeparableQuotient.Norming.InfinitePath.tailCrop_set line 231
29. lemma OAI.SeparableQuotient.Norming.InfinitePath.before_endpoint line 235
30. lemma OAI.SeparableQuotient.Norming.InfinitePath.after_endpoint line 239
31. lemma OAI.SeparableQuotient.Norming.InfinitePath.tail_piece line 245
32. lemma OAI.SeparableQuotient.Norming.InfinitePath.tail_active_subset line 257
33. lemma OAI.SeparableQuotient.Norming.InfinitePath.tail_prefix_coeff line 272
34. lemma OAI.SeparableQuotient.ActualSpace.pathPartial_crop_apply line 316
35. def OAI.SeparableQuotient.ActualSpace.pathTail line 324
36. lemma OAI.SeparableQuotient.ActualSpace.pathTail_complement line 327
37. lemma OAI.SeparableQuotient.ActualSpace.pathTail_complement_mem line 341
38. lemma OAI.SeparableQuotient.ActualSpace.rational_tail_bound line 347

    Source documentation

    The exact original coding is retained in all finite tails.

    lemma rational_tail_bound {f : Family} {h : ℕ} (P : Fin h → InfinitePath f) (N : ℕ)
        (hdis : Pairwise (fun i j => Disjoint
          (Set.range (fun n => (P i).raw.weight (n+N+1)))
          (Set.range (fun n => (P j).raw.weight (n+N+1)))))
        (c : Fin h → ℚ) (hc : ∑ i, |(c i : ℝ)| ^ f.q ≤ 1) :
        ‖∑ i, (c i : ℝ) • pathTail (P i) N‖ ≤ 1 := by
    …

    Mentions: OAI.SeparableQuotient.ActualSpace.pathTail