feat(measure_theory/integral/peak_function): convergence of integral …

…against a sequence of peak functions (#18327)

If a sequence of peak functions `φᵢ` converges uniformly to zero away from a point `x₀`, and `g` is integrable and continuous at `x₀`, then `∫ φᵢ • g` converges to `g x₀`.  We prove this statement and some consequences of it (notably to sequences which are the successive powers of a given function).



Co-authored-by: David Loeffler <d.loeffler.01@cantab.net>
Co-authored-by: loefflerd <d.loeffler.01@cantab.net>

src/measure_theory/function/l1_space.lean

@@ -882,6 +882,20 @@ lemma integrable_smul_iff {c : 𝕜} (hc : c ≠ 0) (f : α → β) :
   integrable (c • f) μ ↔ integrable f μ :=
 and_congr (ae_strongly_measurable_const_smul_iff₀ hc) (has_finite_integral_smul_iff hc f)
 
+lemma integrable.smul_of_top_right {f : α → β} {φ : α → 𝕜}
+  (hf : integrable f μ) (hφ : mem_ℒp φ ∞ μ) :
+  integrable (φ • f) μ :=
+by { rw ← mem_ℒp_one_iff_integrable at hf ⊢, exact mem_ℒp.smul_of_top_right hf hφ }
+
+lemma integrable.smul_of_top_left {f : α → β} {φ : α → 𝕜}
+  (hφ : integrable φ μ) (hf : mem_ℒp f ∞ μ) :
+  integrable (φ • f) μ :=
+by { rw ← mem_ℒp_one_iff_integrable at hφ ⊢, exact mem_ℒp.smul_of_top_left hf hφ }
+
+lemma integrable.smul_const {f : α → 𝕜} (hf : integrable f μ) (c : β) :
+  integrable (λ x, f x • c) μ :=
+hf.smul_of_top_left (mem_ℒp_top_const c)
+
 end normed_space
 
 section normed_space_over_complete_field
@@ -897,6 +911,7 @@ begin
   have : ∀ x : ℝ≥0∞, x = 0 → x < ∞ := by simp,
   simp [hc, or_iff_left_of_imp (this _)]
 end
+
 end normed_space_over_complete_field
 
 section is_R_or_C

src/measure_theory/function/lp_space.lean

@@ -1325,6 +1325,16 @@ lemma mem_ℒp.smul {p q r : ℝ≥0∞} {f : α → E} {φ : α → 𝕜}
 ⟨hφ.1.smul hf.1, (snorm_smul_le_mul_snorm hf.1 hφ.1 hpqr).trans_lt
   (ennreal.mul_lt_top hφ.snorm_ne_top hf.snorm_ne_top)⟩
 
+lemma mem_ℒp.smul_of_top_right {p : ℝ≥0∞} {f : α → E} {φ : α → 𝕜}
+  (hf : mem_ℒp f p μ) (hφ : mem_ℒp φ ∞ μ) :
+  mem_ℒp (φ • f) p μ :=
+by { apply hf.smul hφ, simp only [ennreal.div_top, zero_add] }
+
+lemma mem_ℒp.smul_of_top_left {p : ℝ≥0∞} {f : α → E} {φ : α → 𝕜}
+  (hf : mem_ℒp f ∞ μ) (hφ : mem_ℒp φ p μ) :
+  mem_ℒp (φ • f) p μ :=
+by { apply hf.smul hφ, simp only [ennreal.div_top, add_zero] }
+
 end normed_space
 
 section monotonicity

src/measure_theory/integral/bochner.lean

@@ -770,6 +770,10 @@ integral_zero α E
 
 variables {α E}
 
+lemma integrable_of_integral_eq_one {f : α → ℝ} (h : ∫ x, f x ∂μ = 1) :
+  integrable f μ :=
+by { contrapose h, rw integral_undef h, exact zero_ne_one }
+
 lemma integral_add (hf : integrable f μ) (hg : integrable g μ) :
   ∫ a, f a + g a ∂μ = ∫ a, f a ∂μ + ∫ a, g a ∂μ :=
 begin