OAI/Analysis/KadisonKastler/ShiftInvariantFunctions.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Scalar functions on the invariant sigma algebra

The invariant measurable structure has exactly the essentially bounded scalar functions fixed by the shift. The countable rational cuts below turn invariance of measurable sets into simultaneous pointwise equality.

  1. theorem OAI.KadisonKastler.real_fixed_of_measurable_shiftInvariantSigma line 22
  2. theorem OAI.KadisonKastler.complex_fixed_of_measurable_shiftInvariantSigma line 36
  3. theorem OAI.KadisonKastler.scalarInfinity_fixed_iff_measurable_shiftInvariantSigma line 44
  4. theorem OAI.KadisonKastler.scalarInfinity_fixed_mem_lpMeas line 58
  5. theorem OAI.KadisonKastler.scalarInfinity_fixed_of_aestronglyMeasurable line 65
  6. def OAI.KadisonKastler.fixedScalarToInvariant line 76

    Source documentation

    Descending a fixed scalar class changes neither its values nor its norm.

    def fixedScalarToInvariant (hS : Measure.QuasiMeasurePreserving S μ μ)
    (f : ScalarLInfinity μ) (hf : scalarInfinityPullback S hS f = f) :
    @Lp X ℂ (shiftInvariantSigma μ S) _ ⊤ (shiftInvariantMeasure μ S) :=
…

    Mentions: OAI.KadisonKastler.ScalarLInfinity, OAI.KadisonKastler.scalarInfinityPullback, OAI.KadisonKastler.shiftInvariantSigma, OAI.KadisonKastler.shiftInvariantMeasure

  7. theorem OAI.KadisonKastler.fixedScalarToInvariant_ae line 82
  8. theorem OAI.KadisonKastler.fixedScalarToInvariant_norm line 87