OAI/Analysis/SeparableQuotients/BoundedCompleteness.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SeparableQuotient.ActualSpace.IsPiece line 19

   Source documentation

   Coordinates of a proposed prefix or interval coincide with the fixed g.

   def IsPiece (g : StrongDual ℝ X₀) (S : Set Γ) (x : E) : Prop :=
   …

   Mentions: OAI.SeparableQuotient.ActualSpace.X₀, OAI.SeparableQuotient.ActualSpace.E

2. lemma OAI.SeparableQuotient.ActualSpace.IsPiece.zero_off line 22
3. lemma OAI.SeparableQuotient.ActualSpace.IsPiece.projection line 26
4. lemma OAI.SeparableQuotient.ActualSpace.IsPiece.eval_eq line 33
5. lemma OAI.SeparableQuotient.ActualSpace.exists_piece_normer line 40
6. lemma OAI.SeparableQuotient.ActualSpace.exists_pure_piece_normer line 55
7. lemma OAI.SeparableQuotient.ActualSpace.projection_colorsBelow_sum line 83
8. lemma OAI.SeparableQuotient.ActualSpace.tendsto_low_colors line 91
9. lemma OAI.SeparableQuotient.OrderedCauchy.separated_pairs_of_not_cauchy line 109

   Source documentation

   Failure of the Cauchy condition on a linearly ordered directed set yields successive separated pairs. This applies equally to countable ordinal prefixes and to an uncountable limit; no countable cofinality is assumed.

   lemma separated_pairs_of_not_cauchy (u : ι → Z) (hu : ¬ CauchySeq u) :
       ∃ ε : ℝ, 0 < ε ∧ ∃ a b : ℕ → ι,
         (∀ i, a i < b i) ∧ (∀ i j, i < j → b i ≤ a j) ∧
         ∀ i, ε ≤ dist (u (b i)) (u (a i)) := by
   …

10. lemma OAI.SeparableQuotient.OrderedCauchy.norm_large_subsequence line 153
11. def OAI.SeparableQuotient.Norming.Crop.colorWindow line 169
12. lemma OAI.SeparableQuotient.Norming.Crop.colorWindow_set line 171
13. lemma OAI.SeparableQuotient.ActualSpace.successive_pieces_color_tendsto line 189
14. lemma OAI.SeparableQuotient.ActualSpace.projection_colorWindow_eq line 208
15. lemma OAI.SeparableQuotient.ActualSpace.exists_large_colorWindow line 220
16. lemma OAI.SeparableQuotient.ActualSpace.no_large_successive_pieces line 262

    Source documentation

    The limit-step contradiction for vector pieces, with normers cropped after norm approximation.

    lemma no_large_successive_pieces (g : StrongDual ℝ X₀) (I : ℕ → Set Γ)
        (hI : ∀ i, (I i).OrdConnected) (v : ℕ → E) (hv : ∀ i, IsPiece g (I i) (v i))
        (hord : ∀ i j, i < j → ∀ a ∈ I i, ∀ b ∈ I j, a < b)
        (δ : ℝ) (hδ : 0 < δ) (hlarge : ∀ i, δ ≤ ‖v i‖) : False := by
    …

    Mentions: OAI.SeparableQuotient.ActualSpace.X₀, OAI.SeparableQuotient.ActualSpace.E, OAI.SeparableQuotient.ActualSpace.IsPiece

17. lemma OAI.SeparableQuotient.ActualSpace.IsPiece.sub_Iic line 301
18. lemma OAI.SeparableQuotient.ActualSpace.prefixes_cauchy line 313

    Source documentation

    The ordinal-prefix net is Cauchy at every limit. It also works at successor limits and at ω₁, without any cofinality assumption.

    lemma prefixes_cauchy {ι : Type*} [LinearOrder ι] [Nonempty ι]
        (g : StrongDual ℝ X₀) (a : ι ↪o Γ) (v : ι → E)
        (hv : ∀ i, IsPiece g (Set.Iic (a i)) (v i)) : CauchySeq v := by
    …

    Mentions: OAI.SeparableQuotient.ActualSpace.X₀, OAI.SeparableQuotient.ActualSpace.E, OAI.SeparableQuotient.ActualSpace.IsPiece

19. lemma OAI.SeparableQuotient.ActualSpace.coordinate_e line 341
20. lemma OAI.SeparableQuotient.ActualSpace.IsPiece.append line 344
21. lemma OAI.SeparableQuotient.ActualSpace.exists_strict_prefix line 359

    Source documentation

    Every strict prefix is the limit of its already constructed inclusive prefixes. This handles empty, successor, and limit initial segments uniformly.

    lemma exists_strict_prefix (g : StrongDual ℝ X₀) (β : Γ)
        (h : ∀ a : Γ, a < β → ∃ x : E, IsPiece g (Set.Iic a) x) :
        ∃ x : E, IsPiece g (Set.Iio β) x := by
    …

    Mentions: OAI.SeparableQuotient.ActualSpace.X₀, OAI.SeparableQuotient.ActualSpace.E, OAI.SeparableQuotient.ActualSpace.IsPiece

22. lemma OAI.SeparableQuotient.ActualSpace.exists_prefix line 388
23. lemma OAI.SeparableQuotient.ActualSpace.exists_all_coordinates line 395
24. lemma OAI.SeparableQuotient.ActualSpace.dense_span_coordinate₀ line 407
25. lemma OAI.SeparableQuotient.ActualSpace.predual_dual_ext line 419
26. lemma OAI.SeparableQuotient.ActualSpace.evaluation_surjective line 426

    Source documentation

    Evaluation onto the dual of the coordinate predual is surjective.

    lemma evaluation_surjective : Function.Surjective norming.evaluation := by
    …

27. def OAI.SeparableQuotient.ActualSpace.predualIsometry line 432