OAI/Analysis/FiniteFactor/CrossedProduct/ColumnSquareMass.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteFactor.sourceColumn line 11
2. theorem OAI.FiniteFactor.sourceColumn_coordinate_measurable line 15
3. theorem OAI.FiniteFactor.sourceColumn_square_hasSum line 22
4. theorem OAI.FiniteFactor.sourceColumn_square_mass line 32

   Source documentation

   Actual endpoint square mass: integrable, and at most one. The shift is a bijection of all integers; no finite coefficient cutoff is introduced.

   theorem sourceColumn_square_mass (θ : SourceCoordinate → ℝ)
       {p : SourceHilbert SourceCoordinate →L[ℂ] SourceHilbert SourceCoordinate}
       (hp : p ∈ sourceAlgebra θ) (hproj : IsStarProjection p) (j : ℕ) (b : Bool) (n : ℤ) :
       Integrable (fun ω => ∑' k : ℤ,
         ‖sourceColumn p b (sourceBiasedEndpoint (fun _ => b) ω) (n+k)‖^2) (sourceBiasedLaw j) ∧
       (∫ ω, (∑' k : ℤ, ‖sourceColumn p b (sourceBiasedEndpoint (fun _ => b) ω) (n+k)‖^2)
         ∂sourceBiasedLaw j) ≤ 1 := by
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceHilbert, OAI.FiniteFactor.sourceAlgebra, OAI.FiniteFactor.sourceColumn, OAI.FiniteFactor.sourceBiasedEndpoint, OAI.FiniteFactor.sourceBiasedLaw