EvaluationCriterion.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.SeparableQuotient.hasSeparableQuotient_of_separable_evaluation line 22

Source documentation

Norm-separable evaluation on an infinite-dimensional dual subspace yields a separable quotient.

theorem hasSeparableQuotient_of_separable_evaluation
    (F : Submodule 𝕜 (StrongDual 𝕜 X)) [IsClosed (F : Set (StrongDual 𝕜 X))]
    (hF : ¬ FiniteDimensional 𝕜 F)
    (hsep : TopologicalSpace.IsSeparable (Set.range (subspaceEvaluation F))) :
    HasSeparableQuotient 𝕜 X := by
…

Mentions: OAI.SeparableQuotient.subspaceEvaluation, OAI.SeparableQuotient.HasSeparableQuotient

lemma OAI.SeparableQuotient.dual_infiniteDimensional line 75
Source documentation
The dual of an infinite-dimensional normed space is infinite-dimensional.
```
lemma dual_infiniteDimensional (hY : ¬ FiniteDimensional 𝕜 Y) :
    ¬ FiniteDimensional 𝕜 (StrongDual 𝕜 Y) := by
…
```

lemma OAI.SeparableQuotient.precomp_antilipschitz_of_surjective line 84

Source documentation

The adjoint of an onto map is bounded below, with the actual open-mapping lift constant.

lemma precomp_antilipschitz_of_surjective (T : X →L[𝕜] Y) (hT : Function.Surjective T) :
    ∃ C : NNReal, AntilipschitzWith C
      (ContinuousLinearMap.precomp 𝕜 T : StrongDual 𝕜 Y →L[𝕜] StrongDual 𝕜 X) := by
…

theorem OAI.SeparableQuotient.separable_evaluation_of_hasSeparableQuotient line 104

Source documentation

A separable quotient yields an infinite-dimensional dual subspace with norm-separable evaluation.

theorem separable_evaluation_of_hasSeparableQuotient (hX : HasSeparableQuotient 𝕜 X) :
    ∃ F : Submodule 𝕜 (StrongDual 𝕜 X), IsClosed (F : Set (StrongDual 𝕜 X)) ∧
      (¬ FiniteDimensional 𝕜 F) ∧
      TopologicalSpace.IsSeparable (Set.range (subspaceEvaluation F)) := by
…

Mentions: OAI.SeparableQuotient.HasSeparableQuotient, OAI.SeparableQuotient.subspaceEvaluation

theorem OAI.SeparableQuotient.hasSeparableQuotient_iff_separable_evaluation line 138

Source documentation

Exact evaluation criterion over either scalar field.

theorem hasSeparableQuotient_iff_separable_evaluation :
    HasSeparableQuotient 𝕜 X ↔
    ∃ F : Submodule 𝕜 (StrongDual 𝕜 X), IsClosed (F : Set (StrongDual 𝕜 X)) ∧
      (¬ FiniteDimensional 𝕜 F) ∧
      TopologicalSpace.IsSeparable (Set.range (subspaceEvaluation F)) := by
…

Mentions: OAI.SeparableQuotient.HasSeparableQuotient, OAI.SeparableQuotient.subspaceEvaluation