Lᵖ membership of a bounded observable of an a.e.-measurable map

On a finite measure space, a bounded measurable observable of an a.e.-measurable map lies in every Lᵖ. This is the pointwise composition fact underlying the bounded-observable entry point to the L² lane of the Exchangeability roadmap; it carries no probabilistic content and applies to a single map.

• memLp_comp_of_bound — if f is measurable, g is a.e. measurable, and f ∘ g is a.e. bounded, then fun ω => f (g ω) is in Lᵖ for every exponent.

Credit for the reused material goes to Mathlib's MemLp.of_bound.

theorem TauCeti.memLp_comp_of_bound {Ω : Type u_1} {α : Type u_2} {E : Type u_3} [MeasurableSpace Ω] [MeasurableSpace α] [MeasurableSpace E] [NormedAddCommGroup E] [BorelSpace E] [SecondCountableTopology E] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {g : Ω → α} {f : α → E} (hf : Measurable f) (hg : AEMeasurable g μ) (C : ℝ) (hbound : ∀ᵐ (ω : Ω) ∂μ, ‖f (g ω)‖ ≤ C) (p : ENNReal) : MeasureTheory.MemLp (fun (ω : Ω) => f (g ω)) p μ

A bounded measurable observable of an a.e.-measurable map belongs to every Lᵖ on a finite measure space: if f is measurable, g is a.e. measurable, and f ∘ g is a.e. bounded, then fun ω => f (g ω) is in Lᵖ for every exponent.