OAI/Analysis/FiniteFactor/CrossedProduct/FiberEnergy.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteFactor.sourceFiberEnergy line 12

   Source documentation

   Squared fiber norm of an actual source L2 vector. Fubini proves finiteness and identifies it with the square-summable coordinate norm almost everywhere.

   def sourceFiberEnergy (f : SourceHilbert SourceCoordinate) (x : SourceCoordinate → ℝ) : ℝ :=
   …

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

2. theorem OAI.FiniteFactor.source_norm_sq_integrable line 15
3. theorem OAI.FiniteFactor.sourceFiberEnergy_integrable line 19
4. theorem OAI.FiniteFactor.sourceFiberEnergy_nonneg line 23
5. theorem OAI.FiniteFactor.source_norm_sq_integral line 26
6. theorem OAI.FiniteFactor.source_norm_sq_energy line 34
7. theorem OAI.FiniteFactor.sourceFiberEnergy_indicator line 40

   Source documentation

   Measurable localization commutes with taking the squared fiber norm.

   theorem sourceFiberEnergy_indicator (A : Set (SourceCoordinate → ℝ)) (hA : MeasurableSet A)
       (f : SourceHilbert SourceCoordinate) :
       sourceFiberEnergy (sourceScalar (sourceBaseIndicator A hA) f) =ᵐ[sourceBaseMeasure]
         A.indicator (sourceFiberEnergy f) := by
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceHilbert, OAI.FiniteFactor.sourceFiberEnergy, OAI.FiniteFactor.sourceScalar, OAI.FiniteFactor.sourceBaseIndicator, OAI.FiniteFactor.sourceBaseMeasure

8. theorem OAI.FiniteFactor.sourceScalar_indicator_norm_sq line 59
9. theorem OAI.FiniteFactor.sourceAlgebra_fiberEnergy_le line 66