OAI/Analysis/SeparableQuotients/BranchReduction.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SeparableQuotient.Singular.top_infinite line 8
2. abbrev OAI.SeparableQuotient.ActualSpace.Cut line 19
3. def OAI.SeparableQuotient.ActualSpace.initialSet line 21
4. lemma OAI.SeparableQuotient.ActualSpace.initialSet_connected line 23
5. def OAI.SeparableQuotient.ActualSpace.initialCrop line 26
6. def OAI.SeparableQuotient.ActualSpace.initialP line 28
7. def OAI.SeparableQuotient.ActualSpace.colorP line 30
8. lemma OAI.SeparableQuotient.ActualSpace.coordinate_initialP line 32
9. lemma OAI.SeparableQuotient.ActualSpace.coordinate_colorP line 36
10. lemma OAI.SeparableQuotient.ActualSpace.initialP_top line 40
11. lemma OAI.SeparableQuotient.ActualSpace.initialP_initialP line 45
12. lemma OAI.SeparableQuotient.ActualSpace.initialP_colorP line 53
13. lemma OAI.SeparableQuotient.ActualSpace.colorP_colorP line 60
14. lemma OAI.SeparableQuotient.ActualSpace.exists_minimal_cut line 68

    Source documentation

    The least non-strictly-singular initial projection terminates at an actual limit cut: every coordinate below it has a strictly larger coordinate below it.

    lemma exists_minimal_cut (F : Submodule ℝ E) (_hF : IsClosed (F : Set E))
        (hI : ¬ FiniteDimensional ℝ F) :
        ∃ γ : Cut, (¬ StrictlySingular ((initialP γ).comp F.subtypeL)) ∧
          (∀ β < γ, StrictlySingular ((initialP β).comp F.subtypeL)) ∧
          (∀ a : Γ, (a : Cut) < γ → ∃ b : Γ, a < b ∧ (b : Cut) < γ) := by
    …

    Mentions: OAI.SeparableQuotient.ActualSpace.E, OAI.SeparableQuotient.ActualSpace.Cut, OAI.SeparableQuotient.ActualSpace.initialP

15. lemma OAI.SeparableQuotient.ActualSpace.exists_initial_reduction line 113

    Source documentation

    Range reduction before the optional single-color reduction.

    lemma exists_initial_reduction (F : Submodule ℝ E) (hF : IsClosed (F : Set E))
        (hI : ¬ FiniteDimensional ℝ F) :
        ∃ (γ : Cut) (H : Submodule ℝ E), IsClosed (H : Set E) ∧
          ¬ FiniteDimensional ℝ H ∧
          (∀ a : Γ, (a : Cut) < γ → ∃ b : Γ, a < b ∧ (b : Cut) < γ) ∧
          (∀ β < γ, StrictlySingular ((initialP β).comp H.subtypeL)) ∧
          ∃ U : H →L[ℝ] F, ∀ x : H, initialP γ (U x) = x := by
    …

    Mentions: OAI.SeparableQuotient.ActualSpace.E, OAI.SeparableQuotient.ActualSpace.Cut, OAI.SeparableQuotient.ActualSpace.initialP

16. def OAI.SeparableQuotient.ActualSpace.familyP line 136
17. structure OAI.SeparableQuotient.ActualSpace.BranchReduction line 140
18. theorem OAI.SeparableQuotient.ActualSpace.exists_branchReduction line 153

    Source documentation

    Ordinal and color projections reduce a closed infinite-dimensional subspace to a branch subspace.

    theorem exists_branchReduction (F : Submodule ℝ E) (hF : IsClosed (F : Set E))
        (hI : ¬ FiniteDimensional ℝ F) : Nonempty (BranchReduction F) := by
    …

    Mentions: OAI.SeparableQuotient.ActualSpace.E, OAI.SeparableQuotient.ActualSpace.BranchReduction