OAI/Analysis/SeparableQuotients/StrictSingularity.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SeparableQuotient.Singular.StrictlySingular line 15

   Source documentation

   A strictly singular operator is not bounded below on any closed infinite-dimensional subspace.

   def StrictlySingular (T : Y →L[𝕜] Z) : Prop :=
   …

2. lemma OAI.SeparableQuotient.Singular.finiteDimensional_of_ker line 19
3. lemma OAI.SeparableQuotient.Singular.exists_finite_vector_normers line 26
4. lemma OAI.SeparableQuotient.Singular.finite_annihilator line 65

   Source documentation

   Finitely many exact annihilation conditions preserve infinite dimension.

   lemma finite_annihilator (M : Submodule 𝕜 Y) (hM : IsClosed (M : Set Y))
       (hI : ¬ FiniteDimensional 𝕜 M) (D : Finset (StrongDual 𝕜 Y)) :
       ∃ N : Submodule 𝕜 Y, N ≤ M ∧ IsClosed (N : Set Y) ∧ ¬ FiniteDimensional 𝕜 N ∧
         ∀ x ∈ N, ∀ d ∈ D, d x = 0 := by
   …

5. lemma OAI.SeparableQuotient.Singular.StrictlySingular.exists_unit_small line 86
6. structure OAI.SeparableQuotient.Singular.VectorNormers line 110
7. lemma OAI.SeparableQuotient.Singular.VectorNormers.prefix_eval line 119
8. lemma OAI.SeparableQuotient.Singular.VectorNormers.prefix_bound line 128
9. lemma OAI.SeparableQuotient.Singular.VectorNormers.coefficient_bound line 136
10. lemma OAI.SeparableQuotient.Singular.VectorNormers.linearCombination_eq_range line 146
11. lemma OAI.SeparableQuotient.Singular.VectorNormers.finsupp_bound line 154
12. lemma OAI.SeparableQuotient.Singular.VectorNormers.linearIndependent line 161
13. def OAI.SeparableQuotient.Singular.SmallRestriction.listSpan line 172
14. instance OAI.SeparableQuotient.Singular.SmallRestriction.(instance at line 173) line 173
15. def OAI.SeparableQuotient.Singular.SmallRestriction.listNormers line 175
16. lemma OAI.SeparableQuotient.Singular.SmallRestriction.listNormers_spec line 177
17. structure OAI.SeparableQuotient.Singular.SmallRestriction.State line 182
18. lemma OAI.SeparableQuotient.Singular.SmallRestriction.exists_next line 191
19. def OAI.SeparableQuotient.Singular.SmallRestriction.nextVector line 198
20. lemma OAI.SeparableQuotient.Singular.SmallRestriction.nextVector_spec line 199
21. def OAI.SeparableQuotient.Singular.SmallRestriction.step line 205
22. def OAI.SeparableQuotient.Singular.SmallRestriction.state line 209
23. def OAI.SeparableQuotient.Singular.SmallRestriction.seq line 213
24. lemma OAI.SeparableQuotient.Singular.SmallRestriction.vectors_state line 217
25. lemma OAI.SeparableQuotient.Singular.SmallRestriction.state_length line 225
26. lemma OAI.SeparableQuotient.Singular.SmallRestriction.seq_spec line 226
27. lemma OAI.SeparableQuotient.Singular.SmallRestriction.normers_mono line 231
28. lemma OAI.SeparableQuotient.Singular.SmallRestriction.normers_unit line 236
29. lemma OAI.SeparableQuotient.Singular.SmallRestriction.listNormers_subset line 245
30. def OAI.SeparableQuotient.Singular.SmallRestriction.normers line 250
31. lemma OAI.SeparableQuotient.Singular.VectorNormers.norm_small line 279
32. theorem OAI.SeparableQuotient.Singular.StrictlySingular.exists_small_restriction line 305

    Source documentation

    A strictly singular operator has arbitrarily small norm on a closed infinite-dimensional subspace.

    theorem StrictlySingular.exists_small_restriction (T : Y →L[𝕜] Z) (hT : StrictlySingular T)
        (M : Submodule 𝕜 Y) (hM : IsClosed (M : Set Y)) (hI : ¬ FiniteDimensional 𝕜 M)
        (ε : ℝ) (hε : 0 < ε) :
        ∃ N : Submodule 𝕜 Y, N ≤ M ∧ IsClosed (N : Set Y) ∧ ¬ FiniteDimensional 𝕜 N ∧
          ∀ x ∈ N, ‖T x‖ ≤ ε*‖x‖ := by
    …

    Mentions: OAI.SeparableQuotient.Singular.StrictlySingular

33. theorem OAI.SeparableQuotient.Singular.exists_small_restriction_finite line 332

    Source documentation

    Finitely many strictly singular operators admit a common closed infinite-dimensional small restriction, including the original ambient subspace.

    theorem exists_small_restriction_finite (D : Finset (Y →L[𝕜] Z))
        (hD : ∀ T ∈ D, StrictlySingular T)
        (M : Submodule 𝕜 Y) (hM : IsClosed (M : Set Y)) (hI : ¬ FiniteDimensional 𝕜 M)
        (ε : ℝ) (hε : 0 < ε) :
        ∃ N : Submodule 𝕜 Y, N ≤ M ∧ IsClosed (N : Set Y) ∧ ¬ FiniteDimensional 𝕜 N ∧
          ∀ T ∈ D, ∀ x ∈ N, ‖T x‖ ≤ ε*‖x‖ := by
    …

    Mentions: OAI.SeparableQuotient.Singular.StrictlySingular

34. lemma OAI.SeparableQuotient.Singular.not_strictlySingular_iff line 361
35. lemma OAI.SeparableQuotient.Singular.lowerBound_antilipschitz line 366
36. lemma OAI.SeparableQuotient.Singular.lowerBound_isClosed_range line 373
37. theorem OAI.SeparableQuotient.Singular.exists_lift_of_not_strictlySingular line 379

    Source documentation

    A non-strictly-singular map furnishes a closed infinite-dimensional image and a bounded lift into its original domain.

    theorem exists_lift_of_not_strictlySingular [CompleteSpace Y] [CompleteSpace Z] (T : Y →L[𝕜] Z)
        (hT : ¬ StrictlySingular T) :
        ∃ (H : Submodule 𝕜 Z), IsClosed (H : Set Z) ∧ ¬ FiniteDimensional 𝕜 H ∧
          ∃ U : H →L[𝕜] Y, ∀ x : H, T (U x) = x := by
    …

    Mentions: OAI.SeparableQuotient.Singular.StrictlySingular

38. lemma OAI.SeparableQuotient.Singular.StrictlySingular.comp_left line 395
39. lemma OAI.SeparableQuotient.Singular.StrictlySingular.comp_right line 415