Hölder's inequality for a function supported in a set

Let w vanish almost everywhere off a set A of finite measure. For exponents r, s > 0 with 1/r + 1/s ≤ 1, Hölder's inequality with the three exponents r, s and (1 - 1/r - 1/s)⁻¹, the last applied to the indicator of A, gives

‖∫ f • w‖ ≤ ‖f‖_{Lʳ} ‖w‖_{Lˢ} μ(A) ^ (1 - 1/r - 1/s).

The factor μ(A) ^ (1 - 1/r - 1/s) is what makes the inequality useful when A is small. In Stampacchia's and De Giorgi's methods, w is a truncation (u - k)⁺, A is the superlevel set {u > k}, and the power of its measure is the source of the superlinear gain that drives the iteration.

Main declarations

• TauCeti.MeasureTheory.norm_integral_smul_le_eLpNorm_mul_eLpNorm_mul_measureReal_rpow: the inequality.

theorem TauCeti.MeasureTheory.norm_integral_smul_le_eLpNorm_mul_eLpNorm_mul_measureReal_rpow {Ω : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [NormedRing 𝕜] [NormedAddCommGroup E] [NormedSpace ℝ E] [MulActionWithZero 𝕜 E] [IsBoundedSMul 𝕜 E] {f : Ω → 𝕜} {w : Ω → E} {r s : NNReal} (hr : 0 < r) (hs : 0 < s) (hrs : (↑r)⁻¹ + (↑s)⁻¹ ≤ 1) (hf : MeasureTheory.MemLp f (↑r) μ) (hw : MeasureTheory.MemLp w (↑s) μ) {A : Set Ω} (hAfin : μ A ≠ ⊤) (hwA : ∀ᵐ (x : Ω) ∂μ, x ∉ A → w x = 0) : ‖∫ (x : Ω), f x • w x ∂μ‖ ≤ (MeasureTheory.eLpNorm f (↑r) μ).toReal * (MeasureTheory.eLpNorm w (↑s) μ).toReal * μ.real A ^ (1 - (↑r)⁻¹ - (↑s)⁻¹)

Hölder's inequality for a function vanishing off a set. Let 0 < r, 0 < s with 1/r + 1/s ≤ 1, let f ∈ Lʳ and w ∈ Lˢ, and suppose that w vanishes almost everywhere off a set A of finite measure. Then

‖∫ f • w‖ ≤ ‖f‖_{Lʳ} ‖w‖_{Lˢ} μ(A) ^ (1 - 1/r - 1/s).