`BookProof.ChapterMackeyQuasiInvariant.proj_coeFn` (μ : Measure X) {E : Set X} (hE : MeasurableSet E) (f : Lp K 2 μ) : (proj μ hE f : X → K) =ᵐ[μ] E.indicator (f : X → K)

Initializing...

`BookProof.ChapterMackeyQuasiInvariant.proj_coeFn` (μ : Measure X) {E : Set X} (hE : MeasurableSet E) (f : Lp K 2 μ) : (proj μ hE f : X → K) =ᵐ[μ] E.indicator (f : X → K) · Prove2Me