OAI/Analysis/FiniteFactor/CrossedProduct/NormalFunctionalSpace.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.FiniteFactor.SourceAlgebraSpace line 11
2. def OAI.FiniteFactor.sourceAlgebraInclusion line 13
3. def OAI.FiniteFactor.sourceVectorFunctional line 18

   Source documentation

   An actual vector functional restricted to the original source algebra.

   def sourceVectorFunctional (θ : SourceCoordinate → ℝ)
       (ξ η : SourceHilbert SourceCoordinate) : StrongDual ℂ (SourceAlgebraSpace θ) :=
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceHilbert, OAI.FiniteFactor.SourceAlgebraSpace

4. theorem OAI.FiniteFactor.sourceVectorFunctional_apply line 23
5. theorem OAI.FiniteFactor.sourceVectorFunctional_norm line 28
6. theorem OAI.FiniteFactor.sourceVectorFunctional_continuous line 41
7. abbrev OAI.FiniteFactor.sourceNormalFunctionalSpace line 50

   Source documentation

   The norm-closed span of actual vector functionals. This constructs a Banach space; identifying its whole dual with the source algebra is a separate surjectivity theorem, not part of this definition.

   abbrev sourceNormalFunctionalSpace (θ : SourceCoordinate → ℝ) :
       Submodule ℂ (StrongDual ℂ (SourceAlgebraSpace θ)) :=
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceAlgebraSpace

8. instance OAI.FiniteFactor.sourceNormalFunctionalSpace_complete line 55
9. instance OAI.FiniteFactor.sourceNormalFunctionalSpace_separable line 60
10. theorem OAI.FiniteFactor.sourceVectorFunctional_mem line 69
11. def OAI.FiniteFactor.SourceNormalPredualSpace line 75

    Source documentation

    A named carrier keeps the inherited Banach-space structures coherent in iterated continuous duals. Its underlying set is exactly the closed span.

    def SourceNormalPredualSpace (θ : SourceCoordinate → ℝ) : Type :=
    …

    Mentions: OAI.FiniteFactor.SourceCoordinate

12. instance OAI.FiniteFactor.sourceNormalPredualSpace_normedGroup line 78
13. instance OAI.FiniteFactor.sourceNormalPredualSpace_normedSpace line 84
14. instance OAI.FiniteFactor.sourceNormalPredualSpace_complete line 90
15. instance OAI.FiniteFactor.sourceNormalPredualSpace_separable line 94
16. def OAI.FiniteFactor.sourceNormalEvaluation line 99

    Source documentation

    Evaluation by each actual algebra element on the constructed space.

    def sourceNormalEvaluation (θ : SourceCoordinate → ℝ) (A : SourceAlgebraSpace θ) :
        StrongDual ℂ (SourceNormalPredualSpace θ) := by
    …

    Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceAlgebraSpace, OAI.FiniteFactor.SourceNormalPredualSpace

17. theorem OAI.FiniteFactor.sourceNormalEvaluation_vector line 104
18. theorem OAI.FiniteFactor.sourceNormalEvaluation_injective line 110

    Source documentation

    The constructed functionals separate the original algebra elements.

    theorem sourceNormalEvaluation_injective (θ : SourceCoordinate → ℝ) :
        Function.Injective (sourceNormalEvaluation θ) := by
    …

    Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceNormalEvaluation