RegularCoreInvariant.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Translation-invariant measurable fields are constant

For each translation the exceptional null set may differ. Fubini and the measure-preserving shear (s,t) ↦ (s-t,t) nevertheless give a single almost-everywhere constant representative. The operator-valued version uses only countably many dense Hilbert coefficients.

theorem OAI.KadisonKastler.measurable_real_translation_invariant_const line 25
Source documentation
A measurable scalar function invariant under every real translation as an almost-everywhere class is almost everywhere constant.
```
theorem measurable_real_translation_invariant_const (f : ℝ → ℂ)
    (hf : Measurable f)
    (htrans : ∀ s : ℝ, (fun t => f (t + s)) =ᵐ[volume] f) :
    ∃ c : ℂ, f =ᵐ[volume] fun _ => c := by
…
```

theorem OAI.KadisonKastler.aestronglyMeasurable_real_translation_invariant_const line 47

Source documentation

The same conclusion for a scalar almost-everywhere measurable class.

theorem aestronglyMeasurable_real_translation_invariant_const (f : ℝ → ℂ)
    (hf : AEStronglyMeasurable f volume)
    (htrans : ∀ s : ℝ, (fun t => f (t + s)) =ᵐ[volume] f) :
    ∃ c : ℂ, f =ᵐ[volume] fun _ => c := by
…

theorem OAI.KadisonKastler.operatorField_real_translation_invariant_const line 67

Source documentation

Scalar translation invariance of a weakly measurable operator field implies a single almost-everywhere constant bounded operator. No common exceptional set for the original uncountable family of translations is required.

theorem operatorField_real_translation_invariant_const
    (F : ℝ → H →L[ℂ] H)
    (hF : ∀ ξ η : H, AEStronglyMeasurable
      (fun t => inner ℂ η (F t ξ)) volume)
    (htrans : ∀ (s : ℝ) (ξ η : H),
      (fun t => inner ℂ η (F (t + s) ξ)) =ᵐ[volume]
        fun t => inner ℂ η (F t ξ)) :
    ∃ T : H →L[ℂ] H, F =ᵐ[volume] fun _ => T := by
…