Integrals of Lᵖ functions against bounded multipliers on finite-measure sets

If h ∈ Lᵖ, 1 ≤ p, vanishes a.e. off a set W of finite measure and k is a scalar multiplier a.e. bounded by B on W, then k • h is integrable and, by Hölder's inequality on W,

‖∫ k • h‖ ≤ B μ(W) ^ (1 - 1/p) ‖h‖_p

(TauCeti.integrable_smul_and_norm_integral_smul_le). This is the estimate that makes h ↦ ∫ k • h continuous on Lᵖ functions supported in W, used to pass to the limit in kernel integrals ∫ K(x - y) h(y) dy for x away from the support of h (TauCeti.tendsto_integral_smul_of_tendsto_eLpNorm_sub).

theorem TauCeti.integrable_smul_and_norm_integral_smul_le {α : Type u_1} {F : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] [NormedSpace ℝ F] {𝕜 : Type u_3} [NormedRing 𝕜] [Module 𝕜 F] [IsBoundedSMul 𝕜 F] {k : α → 𝕜} {W : Set α} (hμW : μ W ≠ ⊤) {B : ℝ} (hB : 0 ≤ B) (hk : MeasureTheory.AEStronglyMeasurable k (μ.restrict W)) (hkB : ∀ᵐ (y : α) ∂μ.restrict W, ‖k y‖ ≤ B) {p : ENNReal} (hp : 1 ≤ p) {h : α → F} (hh : MeasureTheory.MemLp h p μ) (h0 : ∀ᵐ (y : α) ∂μ, y ∉ W → h y = 0) : MeasureTheory.Integrable (fun (y : α) => k y • h y) μ ∧ ‖∫ (y : α), k y • h y ∂μ‖ ≤ B * (μ W ^ (1 - 1 / p.toReal) * MeasureTheory.eLpNorm h p μ).toReal

If k is a.e. bounded by B on a set W of finite measure, and h ∈ Lᵖ, 1 ≤ p, vanishes a.e. off W, then k • h is integrable and, by Hölder's inequality on W, ‖∫ k • h‖ ≤ B μ(W) ^ (1 - 1/p) ‖h‖_p.

theorem TauCeti.tendsto_integral_smul_of_tendsto_eLpNorm_sub {α : Type u_1} {F : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] [NormedSpace ℝ F] {𝕜 : Type u_3} [NormedRing 𝕜] [Module 𝕜 F] [IsBoundedSMul 𝕜 F] {ι : Type u_4} {l : Filter ι} {k : α → 𝕜} {W : Set α} (hμW : μ W ≠ ⊤) {B : ℝ} (hB : 0 ≤ B) (hk : MeasureTheory.AEStronglyMeasurable k (μ.restrict W)) (hkB : ∀ᵐ (y : α) ∂μ.restrict W, ‖k y‖ ≤ B) {p : ENNReal} (hp : 1 ≤ p) {φ : ι → α → F} {f : α → F} (hφ : ∀ᶠ (i : ι) in l, MeasureTheory.MemLp (φ i) p μ) (hf : MeasureTheory.MemLp f p μ) (hφ0 : ∀ᶠ (i : ι) in l, ∀ᵐ (y : α) ∂μ, y ∉ W → φ i y = 0) (hf0 : ∀ᵐ (y : α) ∂μ, y ∉ W → f y = 0) (hlim : Filter.Tendsto (fun (i : ι) => MeasureTheory.eLpNorm (φ i - f) p μ) l (nhds 0)) : Filter.Tendsto (fun (i : ι) => ∫ (y : α), k y • φ i y ∂μ) l (nhds (∫ (y : α), k y • f y ∂μ))

Continuity of kernel integrals in Lᵖ. Let k be a.e. bounded by B on a set W of finite measure, and let φ i and f be in Lᵖ, 1 ≤ p, and vanish a.e. off W (for φ i, membership in Lᵖ and vanishing hold eventually along l). If φ i → f in Lᵖ, then ∫ k • φ i → ∫ k • f.