Lᵖ bounds for bounded functions supported in a set

A function bounded by C and supported in a set s has eLpNorm f p μ ≤ μ s ^ (1/p) C (MeasureTheory.eLpNorm_le_of_ae_bound_of_support_subset). This sharpens Mathlib's MeasureTheory.eLpNorm_le_of_ae_bound, which has the measure of the whole space in place of μ s, and is the usual way to bound the Lᵖ norm of a compactly supported function. The same bound for the norm of the class in Lᵖ(μ) is MeasureTheory.MemLp.norm_toLp_le_of_support_subset.

theorem MeasureTheory.eLpNorm_le_of_ae_bound_of_support_subset {α : Type u_1} {F : Type u_2} [MeasurableSpace α] [NormedAddCommGroup F] {μ : Measure α} {f : α → F} {s : Set α} {C : ℝ} {p : ENNReal} (hf : AEStronglyMeasurable f μ) (hfs : Function.support f ⊆ s) (hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C) : eLpNorm f p μ ≤ μ s ^ p.toReal⁻¹ * ENNReal.ofReal C

A function bounded by C almost everywhere and supported in a set s has Lᵖ seminorm at most μ s ^ (1/p) C.

theorem MeasureTheory.MemLp.norm_toLp_le_of_support_subset {α : Type u_1} {F : Type u_2} [MeasurableSpace α] [NormedAddCommGroup F] {μ : Measure α} {f : α → F} {p : ENNReal} (hf : MemLp f p μ) {s : Set α} (hs : μ s ≠ ⊤) (hfs : Function.support f ⊆ s) {C : ℝ} (hC : 0 ≤ C) (hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C) : ‖toLp f hf‖ ≤ (μ s ^ p.toReal⁻¹).toReal * C

The Lᵖ(μ) class of a function supported in a set s of finite measure and bounded by C almost everywhere has norm at most μ(s)^(1/p) C.