OAI/Analysis/FiniteFactor/Matrix/Integrals.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteFactor.source_fiber_restrict line 10
2. theorem OAI.FiniteFactor.source_fiber_integral line 17
3. theorem OAI.FiniteFactor.source_fiber_integrable line 25
4. theorem OAI.FiniteFactor.sourceMatrixEntry_measurable line 33
5. theorem OAI.FiniteFactor.sourceMatrixEntry_integrable line 39
6. theorem OAI.FiniteFactor.sourceMatrixEntry_setIntegral line 44
7. theorem OAI.FiniteFactor.sourceVacuumFunctional_matrixIntegral line 53

   Source documentation

   The displayed trace integral is the actual previously proved normal state.

   theorem sourceVacuumFunctional_matrixIntegral
       (H : SourceHilbert SourceCoordinate →L[ℂ] SourceHilbert SourceCoordinate) :
       sourceVacuumFunctional H = ∫ x, sourceMatrixEntry H 0 0 x ∂sourceBaseMeasure := by
   …

   Mentions: OAI.FiniteFactor.SourceHilbert, OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceVacuumFunctional, OAI.FiniteFactor.sourceMatrixEntry, OAI.FiniteFactor.sourceBaseMeasure

8. theorem OAI.FiniteFactor.sourceMatrixEntry_star line 60

   Source documentation

   Adjoint matrix coefficients agree almost everywhere, on the actual source base.

   theorem sourceMatrixEntry_star (θ : SourceCoordinate → ℝ)
       {H : SourceHilbert SourceCoordinate →L[ℂ] SourceHilbert SourceCoordinate}
       (hH : H ∈ sourceAlgebra θ) (k n : ℤ) :
       sourceMatrixEntry (star H) k n =ᵐ[sourceBaseMeasure]
         fun x => star (sourceMatrixEntry H n k x) := by
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceHilbert, OAI.FiniteFactor.sourceAlgebra, OAI.FiniteFactor.sourceMatrixEntry, OAI.FiniteFactor.sourceBaseMeasure