OAI/Analysis/SeparableQuotients/FiniteNormers.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SeparableQuotient.exists_finite_normers line 18

    Source documentation

    Finite half-normers in the unit ball.

    theorem exists_finite_normers (F : Submodule š•œ (StrongDual š•œ X))
    [FiniteDimensional š•œ F] :
    āˆƒ D : Finset X, (āˆ€ d āˆˆ D, ā€–dā€– ā‰¤ 1) āˆ§
      āˆ€ v : F, āˆƒ d āˆˆ D, ā€–vā€– ā‰¤ 2 * ā€–(v : StrongDual š•œ X) dā€– := by
ā€¦
  2. theorem OAI.SeparableQuotient.exists_unit_annihilator line 62

    Source documentation

    Finite annihilation conditions leave a unit functional in every infinite-dimensional subspace.

    theorem exists_unit_annihilator (F : Submodule š•œ (StrongDual š•œ X))
    (hF : Ā¬ FiniteDimensional š•œ F) (A : Finset X) :
    āˆƒ f : F, ā€–fā€– = 1 āˆ§ āˆ€ x āˆˆ A, (f : StrongDual š•œ X) x = 0 := by
ā€¦
  3. structure OAI.SeparableQuotient.NormerStep line 88

    Source documentation

    One finite stage of the normer construction.

    structure NormerStep (F : Submodule š•œ (StrongDual š•œ X))
    (A : Finset X) (S : Finset (StrongDual š•œ X)) where
ā€¦
  4. def OAI.SeparableQuotient.chooseNormerStep line 98
  5. def OAI.SeparableQuotient.NormerStep.state line 115

    Source documentation

    Accumulated annihilation constraints and preceding functionals.

    noncomputable def state : ā„• ā†’ Finset X Ɨ Finset (StrongDual š•œ X)
  | 0 => (āˆ…, āˆ…)
  | n + 1 =>
    let p := state n
ā€¦
  6. def OAI.SeparableQuotient.NormerStep.stage line 122
  7. def OAI.SeparableQuotient.NormerStep.seq line 125
  8. lemma OAI.SeparableQuotient.NormerStep.state_succ line 127
  9. lemma OAI.SeparableQuotient.NormerStep.state_monotone line 132
  10. lemma OAI.SeparableQuotient.NormerStep.state_vectors line 139
  11. lemma OAI.SeparableQuotient.NormerStep.seq_mem line 146
  12. lemma OAI.SeparableQuotient.NormerStep.seq_norm line 147
  13. lemma OAI.SeparableQuotient.NormerStep.seq_vanish_x line 149
  14. lemma OAI.SeparableQuotient.NormerStep.seq_vanish_D line 160
  15. lemma OAI.SeparableQuotient.NormerStep.stage_norms_prefix line 170
  16. def OAI.SeparableQuotient.NormerStep.prefixNormers line 208

    Source documentation

    The recursive choices satisfy exactly the prefix hypotheses.

    noncomputable def prefixNormers : PrefixNormers (seq F hF xs) where
ā€¦

    Mentions: OAI.SeparableQuotient.PrefixNormers, OAI.SeparableQuotient.NormerStep.seq

  17. lemma OAI.SeparableQuotient.NormerStep.span_le line 230
  18. lemma OAI.SeparableQuotient.NormerStep.evaluation_x line 237
  19. def OAI.SeparableQuotient.subspaceEvaluation line 265

    Source documentation

    The actual evaluation operator on a dual subspace.

    noncomputable def subspaceEvaluation (F : Submodule š•œ (StrongDual š•œ X)) :
    X ā†’L[š•œ] StrongDual š•œ F :=
ā€¦
  20. lemma OAI.SeparableQuotient.subspaceEvaluation_apply line 269
  21. lemma OAI.SeparableQuotient.exists_dense_evaluations line 278

    Source documentation

    A dense sequence of evaluations can be represented by actual vectors of X.

    lemma exists_dense_evaluations (F : Submodule š•œ (StrongDual š•œ X))
    (hsep : TopologicalSpace.IsSeparable (Set.range (subspaceEvaluation F))) :
    āˆƒ xs : ā„• ā†’ X, āˆ€ x : X, subspaceEvaluation F x āˆˆ
      closure (Set.range (fun n => subspaceEvaluation F (xs n))) := by
ā€¦

    Mentions: OAI.SeparableQuotient.subspaceEvaluation