OAI/Analysis/FiniteFactor/CrossedProduct/VacuumFunctional.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteFactor.sourceVacuum line 13

   Source documentation

   The constant e_0 field in the actual L2(X times Z) source model.

   Also declared: ComparatorChallenges/ProductBrown.lean:510 (same declaration text).

   def sourceVacuum : SourceHilbert SourceCoordinate :=
   …

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

2. theorem OAI.FiniteFactor.sourceVacuum_norm line 40

   Also declared: ComparatorChallenges/ProductBrown.lean:537 (same declaration text).

3. abbrev OAI.FiniteFactor.sourceVacuumFunctional line 86

   Also declared: ComparatorChallenges/ProductBrown.lean:583 (same declaration text).

4. theorem OAI.FiniteFactor.sourceVacuumFunctional_one line 108
5. theorem OAI.FiniteFactor.sourceVacuumFunctional_add line 111
6. theorem OAI.FiniteFactor.sourceVacuumFunctional_smul line 115
7. theorem OAI.FiniteFactor.sourceVacuumFunctional_bound line 120
8. theorem OAI.FiniteFactor.sourceVacuumFunctional_square line 129
9. theorem OAI.FiniteFactor.sourceVacuumFunctional_square_nonneg line 134
10. theorem OAI.FiniteFactor.sourceVacuumFunctional_normal line 143

    Source documentation

    Normality here is continuity for the actual ultraweak topology defined by absolutely summable vector functionals, specialized to the source Hilbert space.

    theorem sourceVacuumFunctional_normal :
        @Continuous _ _ (ultraweakTopology (SourceHilbert SourceCoordinate)) inferInstance sourceVacuumFunctional :=
    …

    Mentions: OAI.FiniteFactor.ultraweakTopology, OAI.FiniteFactor.SourceHilbert, OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceVacuumFunctional

11. def OAI.FiniteFactor.sourceAlgebraUltraweakTopology line 147
12. theorem OAI.FiniteFactor.sourceVacuumFunctional_algebra_normal line 153