OAI/Analysis/FiniteFactor/CrossedProduct/NormalRiesz.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FiniteFactor.sourceNormalRieszLinear line 8
  2. theorem OAI.FiniteFactor.sourceNormalRieszLinear_bound line 24
  3. def OAI.FiniteFactor.sourceNormalRieszFunctional line 34
  4. def OAI.FiniteFactor.sourceNormalRieszVector line 39
  5. theorem OAI.FiniteFactor.sourceNormalRieszVector_inner line 44
  6. theorem OAI.FiniteFactor.sourceNormalRieszVector_norm line 56
  7. def OAI.FiniteFactor.sourceNormalRieszOperator line 65

    Source documentation

    Every functional on the constructed Banach space gives an actual bounded operator by Riesz representation. Membership in the source algebra is proved separately by commutation, not assumed here.

    def sourceNormalRieszOperator (θ : SourceCoordinate → ℝ)
    (F : StrongDual ℂ (SourceNormalPredualSpace θ)) :
    SourceHilbert SourceCoordinate →L[ℂ] SourceHilbert SourceCoordinate :=
…

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

  8. theorem OAI.FiniteFactor.sourceNormalRieszOperator_inner line 83
  9. theorem OAI.FiniteFactor.sourceNormalRieszOperator_norm line 88