Monotonicity and subadditivity of eLpNorm in the measure

For 1 ≤ p, the Lᵖ seminorm is subadditive in the measure: eLpNorm f p (μ + ν) ≤ eLpNorm f p μ + eLpNorm f p ν (MeasureTheory.eLpNorm_add_measure_le). For p < ∞ this is the inequality (a + b) ^ (1 / p) ≤ a ^ (1 / p) + b ^ (1 / p), and for p = ∞ the essential supremum for μ + ν is the maximum of the two essential suprema. Mathlib has the equality for p = 1 (MeasureTheory.eLpNorm_one_add_measure); for p < 1 the inequality fails.

Restricting to a finite union of sets gives the form used to pass from local estimates to an estimate on a set covered by finitely many pieces (MeasureTheory.eLpNorm_restrict_biUnion_finset_le): eLpNorm f p (μ.restrict (⋃ i ∈ t, s i)) ≤ ∑ i ∈ t, eLpNorm f p (μ.restrict (s i)). No measurability of the sets is needed. The same bound holds on any set covered by finitely many pieces (MeasureTheory.eLpNorm_restrict_le_sum_of_subset_iUnion), so a function in Lᵖ on each piece is in Lᵖ on the covered set (MeasureTheory.MemLp.restrict_of_subset_iUnion).

For the real-valued norm lpNorm, monotonicity in the measure needs f ∈ Lᵖ(μ), since lpNorm is 0 off Lᵖ (MeasureTheory.lpNorm_mono_measure).

Main declarations

• MeasureTheory.lpNorm_mono_measure: monotonicity of lpNorm in the measure.
• MeasureTheory.eLpNorm_add_measure_le: subadditivity in the measure.
• MeasureTheory.eLpNorm_add_measure_rpow_le: the p-th power of the Lᵖ seminorm is subadditive in the measure, at every p : ℝ≥0∞ (a pseudometrizable codomain with an extended norm suffices).
• MeasureTheory.eLpNorm_restrict_biUnion_finset_le: subadditivity over a finite union.
• MeasureTheory.eLpNorm_restrict_le_sum_of_subset_iUnion: subadditivity over a finite cover.
• MeasureTheory.MemLp.restrict_of_subset_iUnion: Lᵖ on each piece of a finite cover gives Lᵖ on the covered set.

theorem MeasureTheory.eLpNorm_add_measure_rpow_le {α : Type u_1} {ε : Type u_2} [MeasurableSpace α] [TopologicalSpace ε] [ENorm ε] [TopologicalSpace.PseudoMetrizableSpace ε] {p : ENNReal} (f : α → ε) (μ ν : Measure α) : eLpNorm f p (μ + ν) ^ p.toReal ≤ eLpNorm f p μ ^ p.toReal + eLpNorm f p ν ^ p.toReal

The p-th power of the Lᵖ seminorm is subadditive under adding measures. For p = 0 or p = ∞, p.toReal = 0 and the bound reduces to 1 ≤ 1 + 1. No measurability is assumed: if the function is not almost everywhere strongly measurable for one of the measures, its seminorm there is ∞. The codomain needs a pseudometrizable topology and an extended norm.

theorem MeasureTheory.lpNorm_mono_measure {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ ν : Measure α} {E : Type u_3} [NormedAddCommGroup E] {f : α → E} (hf : MemLp f p μ) (hνμ : ν ≤ μ) : lpNorm f p ν ≤ lpNorm f p μ

Monotonicity of lpNorm in the measure. If f ∈ Lᵖ(μ) and ν ≤ μ, then lpNorm f p ν ≤ lpNorm f p μ.

theorem MeasureTheory.eLpNorm_add_measure_le {α : Type u_1} {ε : Type u_2} {m : MeasurableSpace α} [TopologicalSpace ε] [ContinuousENorm ε] [TopologicalSpace.PseudoMetrizableSpace ε] {p : ENNReal} {μ ν : Measure α} (f : α → ε) (hp : 1 ≤ p) : eLpNorm f p (μ + ν) ≤ eLpNorm f p μ + eLpNorm f p ν

Subadditivity of eLpNorm in the measure. For 1 ≤ p, eLpNorm f p (μ + ν) ≤ eLpNorm f p μ + eLpNorm f p ν.

theorem MeasureTheory.eLpNorm_restrict_biUnion_finset_le {α : Type u_1} {ε : Type u_2} {m : MeasurableSpace α} [TopologicalSpace ε] [ContinuousENorm ε] [TopologicalSpace.PseudoMetrizableSpace ε] {p : ENNReal} {μ : Measure α} {ι : Type u_3} (f : α → ε) (hp : 1 ≤ p) (t : Finset ι) (s : ι → Set α) : eLpNorm f p (μ.restrict (⋃ i ∈ t, s i)) ≤ ∑ i ∈ t, eLpNorm f p (μ.restrict (s i))

Subadditivity of eLpNorm over a finite union. For 1 ≤ p, the Lᵖ seminorm of f on a finite union of sets is at most the sum of its Lᵖ seminorms on the pieces. The sets need not be measurable or disjoint.

theorem MeasureTheory.eLpNorm_restrict_le_sum_of_subset_iUnion {α : Type u_1} {ε : Type u_2} {m : MeasurableSpace α} [TopologicalSpace ε] [ContinuousENorm ε] [TopologicalSpace.PseudoMetrizableSpace ε] {p : ENNReal} {μ : Measure α} {ι : Type u_3} [Fintype ι] (f : α → ε) (hp : 1 ≤ p) {s : Set α} {t : ι → Set α} (hs : s ⊆ ⋃ (i : ι), t i) : eLpNorm f p (μ.restrict s) ≤ ∑ i : ι, eLpNorm f p (μ.restrict (t i))

Subadditivity of eLpNorm over a finite cover. For 1 ≤ p, the Lᵖ seminorm of f on a set covered by finitely many sets is at most the sum of its Lᵖ seminorms on the pieces.

theorem MeasureTheory.MemLp.restrict_of_subset_iUnion {α : Type u_1} {ε : Type u_2} {m : MeasurableSpace α} [TopologicalSpace ε] [ContinuousENorm ε] [TopologicalSpace.PseudoMetrizableSpace ε] {p : ENNReal} {μ : Measure α} {ι : Type u_3} [Finite ι] {f : α → ε} {s : Set α} {t : ι → Set α} (hs : s ⊆ ⋃ (i : ι), t i) (hf : ∀ (i : ι), MemLp f p (μ.restrict (t i))) : MemLp f p (μ.restrict s)

A function in Lᵖ on each of finitely many sets is in Lᵖ on every set they cover.