feat(measure_theory/integral/average): average of constant functions (#…

…16776)

Also make the API more coherent, by renaming `average_def'` to `average_eq` to match `set_average_eq`. And rename `lintegral_to_real_le_lintegral_nnnorm` to `lintegral_of_real_le_lintegral_nnnorm`.

src/analysis/convex/integral.lean

@@ -327,8 +327,8 @@ begin
     simp only [average_congr this, pi.zero_apply, average_zero],
     exact or.inl this },
   by_cases hfi : integrable f μ, swap,
-    by simp [average_def', integral_undef hfi, hC0, ennreal.to_real_pos_iff],
-  cases (le_top : μ univ ≤ ∞).eq_or_lt with hμt hμt, { simp [average_def', hμt, hC0] },
+    by simp [average_eq, integral_undef hfi, hC0, ennreal.to_real_pos_iff],
+  cases (le_top : μ univ ≤ ∞).eq_or_lt with hμt hμt, { simp [average_eq, hμt, hC0] },
   haveI : is_finite_measure μ := ⟨hμt⟩,
   replace h_le : ∀ᵐ x ∂μ, f x ∈ closed_ball (0 : E) C, by simpa only [mem_closed_ball_zero_iff],
   simpa only [interior_closed_ball _ hC0.ne', mem_ball_zero_iff]
@@ -347,7 +347,7 @@ begin
   have hμ : 0 < (μ univ).to_real,
     by simp [ennreal.to_real_pos_iff, pos_iff_ne_zero, h₀, measure_lt_top],
   refine (ae_eq_const_or_norm_average_lt_of_norm_le_const h_le).imp_right (λ H, _),
-  rwa [average_def', norm_smul, norm_inv, real.norm_eq_abs, abs_of_pos hμ,
+  rwa [average_eq, norm_smul, norm_inv, real.norm_eq_abs, abs_of_pos hμ,
     ← div_eq_inv_mul, div_lt_iff' hμ] at H
 end
 

src/analysis/normed/group/basic.lean

@@ -658,6 +658,9 @@ nnreal.coe_le_coe.1 $ norm_add_le g h
 @[simp] lemma nnnorm_neg (g : E) : ∥-g∥₊ = ∥g∥₊ :=
 nnreal.eq $ norm_neg g
 
+lemma nnnorm_sub_le (g h : E) : ∥g - h∥₊ ≤ ∥g∥₊ + ∥h∥₊ :=
+nnreal.coe_le_coe.1 $ norm_sub_le g h
+
 lemma nndist_nnnorm_nnnorm_le (g h : E) : nndist ∥g∥₊ ∥h∥₊ ≤ ∥g - h∥₊ :=
 nnreal.coe_le_coe.1 $ dist_norm_norm_le g h
 

src/measure_theory/function/l1_space.lean

@@ -509,6 +509,10 @@ lemma integrable_smul_measure {f : α → β} {c : ℝ≥0∞} (h₁ : c ≠ 0)
 ⟨λ h, by simpa only [smul_smul, ennreal.inv_mul_cancel h₁ h₂, one_smul]
   using h.smul_measure (ennreal.inv_ne_top.2 h₁), λ h, h.smul_measure h₂⟩
 
+lemma integrable_inv_smul_measure {f : α → β} {c : ℝ≥0∞} (h₁ : c ≠ 0) (h₂ : c ≠ ∞) :
+  integrable f (c⁻¹ • μ) ↔ integrable f μ :=
+integrable_smul_measure (by simpa using h₂) (by simpa using h₁)
+
 lemma integrable.to_average {f : α → β} (h : integrable f μ) :
   integrable f ((μ univ)⁻¹ • μ) :=
 begin

src/measure_theory/integral/average.lean

@@ -71,10 +71,10 @@ by rw [average, smul_zero, integral_zero_measure]
 
 @[simp] lemma average_neg (f : α → E) : ⨍ x, -f x ∂μ = -⨍ x, f x ∂μ := integral_neg f
 
-lemma average_def (f : α → E) : ⨍ x, f x ∂μ = ∫ x, f x ∂((μ univ)⁻¹ • μ) := rfl
+lemma average_eq' (f : α → E) : ⨍ x, f x ∂μ = ∫ x, f x ∂((μ univ)⁻¹ • μ) := rfl
 
-lemma average_def' (f : α → E) : ⨍ x, f x ∂μ = (μ univ).to_real⁻¹ • ∫ x, f x ∂μ :=
-by rw [average_def, integral_smul_measure, ennreal.to_real_inv]
+lemma average_eq (f : α → E) : ⨍ x, f x ∂μ = (μ univ).to_real⁻¹ • ∫ x, f x ∂μ :=
+by rw [average_eq', integral_smul_measure, ennreal.to_real_inv]
 
 lemma average_eq_integral [is_probability_measure μ] (f : α → E) :
   ⨍ x, f x ∂μ = ∫ x, f x ∂μ :=
@@ -85,19 +85,23 @@ by rw [average, measure_univ, inv_one, one_smul]
 begin
   cases eq_or_ne μ 0 with hμ hμ,
   { rw [hμ, integral_zero_measure, average_zero_measure, smul_zero] },
-  { rw [average_def', smul_inv_smul₀],
+  { rw [average_eq, smul_inv_smul₀],
     refine (ennreal.to_real_pos _ $ measure_ne_top _ _).ne',
     rwa [ne.def, measure_univ_eq_zero] }
 end
 
 lemma set_average_eq (f : α → E) (s : set α) :
   ⨍ x in s, f x ∂μ = (μ s).to_real⁻¹ • ∫ x in s, f x ∂μ :=
-by rw [average_def', restrict_apply_univ]
+by rw [average_eq, restrict_apply_univ]
+
+lemma set_average_eq' (f : α → E) (s : set α) :
+  ⨍ x in s, f x ∂μ = ∫ x, f x ∂((μ s)⁻¹ • μ.restrict s) :=
+by simp only [average_eq', restrict_apply_univ]
 
 variable {μ}
 
 lemma average_congr {f g : α → E} (h : f =ᵐ[μ] g) : ⨍ x, f x ∂μ = ⨍ x, g x ∂μ :=
-by simp only [average_def', integral_congr_ae h]
+by simp only [average_eq, integral_congr_ae h]
 
 lemma average_add_measure [is_finite_measure μ] {ν : measure α} [is_finite_measure ν] {f : α → E}
   (hμ : integrable f μ) (hν : integrable f ν) :
@@ -107,7 +111,7 @@ lemma average_add_measure [is_finite_measure μ] {ν : measure α} [is_finite_me
 begin
   simp only [div_eq_inv_mul, mul_smul, measure_smul_average, ← smul_add,
     ← integral_add_measure hμ hν, ← ennreal.to_real_add (measure_ne_top μ _) (measure_ne_top ν _)],
-  rw [average_def', measure.add_apply]
+  rw [average_eq, measure.add_apply]
 end
 
 lemma average_pair {f : α → E} {g : α → F} (hfi : integrable f μ) (hgi : integrable g μ) :
@@ -162,4 +166,17 @@ by simpa only [union_compl_self, restrict_univ]
   using average_union_mem_open_segment ae_disjoint_compl_right hs.compl hs₀ hsc₀
     (measure_ne_top _ _) (measure_ne_top _ _) hfi.integrable_on hfi.integrable_on
 
+@[simp] lemma average_const [is_finite_measure μ] [h : μ.ae.ne_bot] (c : E) :
+  ⨍ x, c ∂μ = c :=
+by simp only [average_eq, integral_const, measure.restrict_apply, measurable_set.univ, one_smul,
+  univ_inter, smul_smul, ← ennreal.to_real_inv, ← ennreal.to_real_mul, ennreal.inv_mul_cancel,
+  measure_ne_top μ univ, ne.def, measure_univ_eq_zero, ae_ne_bot.1 h, not_false_iff,
+  ennreal.one_to_real]
+
+lemma set_average_const {s : set α} (hs₀ : μ s ≠ 0) (hs : μ s ≠ ∞) (c : E) :
+  ⨍ x in s, c ∂μ = c :=
+by simp only [set_average_eq, integral_const, measure.restrict_apply, measurable_set.univ,
+  univ_inter, smul_smul, ← ennreal.to_real_inv, ← ennreal.to_real_mul,
+  ennreal.inv_mul_cancel hs₀ hs, ennreal.one_to_real, one_smul]
+
 end measure_theory

src/measure_theory/integral/integrable_on.lean

@@ -249,7 +249,7 @@ end
 lemma integrable.lintegral_lt_top {f : α → ℝ} (hf : integrable f μ) :
   ∫⁻ x, ennreal.of_real (f x) ∂μ < ∞ :=
 calc ∫⁻ x, ennreal.of_real (f x) ∂μ
-    ≤ ∫⁻ x, ↑∥f x∥₊ ∂μ : lintegral_to_real_le_lintegral_nnnorm f
+    ≤ ∫⁻ x, ↑∥f x∥₊ ∂μ : lintegral_of_real_le_lintegral_nnnorm f
 ... < ∞ : hf.2
 
 lemma integrable_on.set_lintegral_lt_top {f : α → ℝ} {s : set α} (hf : integrable_on f s μ) :

src/measure_theory/integral/lebesgue.lean

@@ -1227,7 +1227,7 @@ lemma set_lintegral_congr_fun {f g : α → ℝ≥0∞} {s : set α} (hs : measu
   ∫⁻ x in s, f x ∂μ = ∫⁻ x in s, g x ∂μ :=
 by { rw lintegral_congr_ae, rw eventually_eq, rwa ae_restrict_iff' hs, }
 
-lemma lintegral_to_real_le_lintegral_nnnorm (f : α → ℝ) :
+lemma lintegral_of_real_le_lintegral_nnnorm (f : α → ℝ) :
   ∫⁻ x, ennreal.of_real (f x) ∂μ ≤ ∫⁻ x, ∥f x∥₊ ∂μ :=
 begin
   simp_rw ← of_real_norm_eq_coe_nnnorm,