feat(analysis/convex/integral): Jensen's inequality for integrals (#4225

)

src/analysis/convex/integral.lean

@@ -0,0 +1,116 @@
+/-
+Copyright (c) 2020 Yury G. Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Yury G. Kudryashov
+-/
+import analysis.convex.basic
+import measure_theory.set_integral
+
+/-!
+# Jensen's inequality for integrals
+
+In this file we prove four theorems:
+
+* `convex.smul_integral_mem`: if `μ` is a non-zero finite measure on `α`, `s` is a convex closed set
+  in `E`, and `f` is an integrable function sending `μ`-a.e. points to `s`, then the average value
+  of `f` belongs to `s`: `(μ univ).to_real⁻¹ • ∫ x, f x ∂μ ∈ s`. See also `convex.center_mass_mem`
+  for a finite sum version of this lemma.
+
+* `convex.integral_mem`: if `μ` is a probability measure on `α`, `s` is a convex closed set in `E`,
+  and `f` is an integrable function sending `μ`-a.e. points to `s`, then the expected value of `f`
+  belongs to `s`: `∫ x, f x ∂μ ∈ s`. See also `convex.sum_mem` for a finite sum version of this
+  lemma.
+
+* `convex_on.map_smul_integral_le`: Jensen's inequality: if a function `g : E → ℝ` is convex and
+  continuous on a convex closed set `s`, `μ` is a finite non-zero measure on `α`, and `f : α → E` is
+  a function sending `μ`-a.e. points to `s`, then the value of `g` at the average value of `f` is
+  less than or equal to the average value of `g ∘ f` provided that both `f` and `g ∘ f` are
+  integrable. See also `convex.map_center_mass_le` for a finite sum version of this lemma.
+
+* `convex_on.map_integral_le`: Jensen's inequality: if a function `g : E → ℝ` is convex and
+  continuous on a convex closed set `s`, `μ` is a probability measure on `α`, and `f : α → E` is a
+  function sending `μ`-a.e. points to `s`, then the value of `g` at the expected value of `f` is
+  less than or equal to the expected value of `g ∘ f` provided that both `f` and `g ∘ f` are
+  integrable. See also `convex.map_sum_le` for a finite sum version of this lemma.
+
+## Tags
+
+convex, integral, center mass, Jensen's inequality
+-/
+
+open measure_theory set filter
+open_locale topological_space big_operators
+
+variables {α E : Type*} [measurable_space α] {μ : measure α}
+  [normed_group E] [normed_space ℝ E] [complete_space E]
+  [topological_space.second_countable_topology E] [measurable_space E] [borel_space E]
+
+/-- If `μ` is a non-zero finite measure on `α`, `s` is a convex closed set in `E`, and `f` is an
+integrable function sending `μ`-a.e. points to `s`, then the average value of `f` belongs to `s`:
+`(μ univ).to_real⁻¹ • ∫ x, f x ∂μ ∈ s`. See also `convex.center_mass_mem` for a finite sum version
+of this lemma. -/
+lemma convex.smul_integral_mem [finite_measure μ] {s : set E} (hs : convex s) (hsc : is_closed s)
+  (hμ : μ ≠ 0) {f : α → E} (hfs : ∀ᵐ x ∂μ, f x ∈ s) (hfi : integrable f μ) :
+  (μ univ).to_real⁻¹ • ∫ x, f x ∂μ ∈ s :=
+begin
+  rcases eq_empty_or_nonempty s with rfl|⟨y₀, h₀⟩, { refine (hμ _).elim, simpa using hfs },
+  rw ← hsc.closure_eq at hfs,
+  have hc : integrable (λ _, y₀) μ := integrable_const _,
+  set F : ℕ → simple_func α E := simple_func.approx_on f hfi.measurable s y₀ h₀,
+  have : tendsto (λ n, (F n).integral μ) at_top (𝓝 $ ∫ x, f x ∂μ),
+  { simp only [simple_func.integral_eq_integral _ (simple_func.integrable_approx_on hfi h₀ hc _)],
+    exact tendsto_integral_of_l1 _ hfi
+      (eventually_of_forall $ simple_func.integrable_approx_on hfi h₀ hc)
+      (simple_func.tendsto_approx_on_l1_edist hfi.1 h₀ hfs (hfi.sub hc).2) },
+  refine hsc.mem_of_tendsto (tendsto_const_nhds.smul this) (eventually_of_forall $ λ n, _),
+  have : ∑ y in (F n).range, (μ ((F n) ⁻¹' {y})).to_real = (μ univ).to_real,
+    by rw [← (F n).sum_range_measure_preimage_singleton, @ennreal.to_real_sum _ _
+      (λ y, μ ((F n) ⁻¹' {y})) (λ _ _, (measure_lt_top _ _))],
+  rw [← this, simple_func.integral],
+  refine hs.center_mass_mem (λ _ _, ennreal.to_real_nonneg) _ _,
+  { rw [this, ennreal.to_real_pos_iff, zero_lt_iff_ne_zero, ne.def, measure.measure_univ_eq_zero],
+    exact ⟨hμ, measure_ne_top _ _⟩ },
+  { simp only [simple_func.mem_range],
+    rintros _ ⟨x, rfl⟩,
+    exact simple_func.approx_on_mem hfi.1 h₀ n x }
+end
+
+/-- If `μ` is a probability measure on `α`, `s` is a convex closed set in `E`, and `f` is an
+integrable function sending `μ`-a.e. points to `s`, then the expected value of `f` belongs to `s`:
+`∫ x, f x ∂μ ∈ s`. See also `convex.sum_mem` for a finite sum version of this lemma. -/
+lemma convex.integral_mem [probability_measure μ] {s : set E} (hs : convex s) (hsc : is_closed s)
+  {f : α → E} (hf : ∀ᵐ x ∂μ, f x ∈ s) (hfi : integrable f μ) :
+  ∫ x, f x ∂μ ∈ s :=
+by simpa [measure_univ] using hs.smul_integral_mem hsc (probability_measure.ne_zero μ) hf hfi
+
+/-- Jensen's inequality: if a function `g : E → ℝ` is convex and continuous on a convex closed set
+`s`, `μ` is a finite non-zero measure on `α`, and `f : α → E` is a function sending `μ`-a.e. points
+to `s`, then the value of `g` at the average value of `f` is less than or equal to the average value
+of `g ∘ f` provided that both `f` and `g ∘ f` are integrable. See also `convex.map_center_mass_le`
+for a finite sum version of this lemma. -/
+lemma convex_on.map_smul_integral_le [finite_measure μ] {s : set E} {g : E → ℝ} (hg : convex_on s g)
+  (hgc : continuous_on g s) (hsc : is_closed s) (hμ : μ ≠ 0) {f : α → E} (hfs : ∀ᵐ x ∂μ, f x ∈ s)
+  (hfi : integrable f μ) (hgi : integrable (g ∘ f) μ) :
+  g ((μ univ).to_real⁻¹ • ∫ x, f x ∂μ) ≤ (μ univ).to_real⁻¹ • ∫ x, g (f x) ∂μ :=
+begin
+  set t := {p : E × ℝ | p.1 ∈ s ∧ g p.1 ≤ p.2},
+  have ht_conv : convex t := hg.convex_epigraph,
+  have ht_closed : is_closed t :=
+    (hsc.preimage continuous_fst).is_closed_le (hgc.comp continuous_on_fst (subset.refl _))
+      continuous_on_snd,
+  have ht_mem : ∀ᵐ x ∂μ, (f x, g (f x)) ∈ t := hfs.mono (λ x hx, ⟨hx, le_rfl⟩),
+  simpa [integral_pair hfi hgi]
+    using (ht_conv.smul_integral_mem ht_closed hμ ht_mem (hfi.prod_mk hgi)).2
+end
+
+/-- Jensen's inequality: if a function `g : E → ℝ` is convex and continuous on a convex closed set
+`s`, `μ` is a probability measure on `α`, and `f : α → E` is a function sending `μ`-a.e. points to
+`s`, then the value of `g` at the expected value of `f` is less than or equal to the expected value
+of `g ∘ f` provided that both `f` and `g ∘ f` are integrable. See also `convex.map_sum_le` for a
+finite sum version of this lemma. -/
+lemma convex_on.map_integral_le [probability_measure μ] {s : set E} {g : E → ℝ} (hg : convex_on s g)
+  (hgc : continuous_on g s) (hsc : is_closed s) {f : α → E} (hfs : ∀ᵐ x ∂μ, f x ∈ s)
+  (hfi : integrable f μ) (hgi : integrable (g ∘ f) μ) :
+  g (∫ x, f x ∂μ) ≤ ∫ x, g (f x) ∂μ :=
+by simpa [measure_univ]
+  using hg.map_smul_integral_le hgc hsc (probability_measure.ne_zero μ) hfs hfi hgi

src/analysis/normed_space/basic.lean

@@ -328,6 +328,9 @@ instance prod.normed_group : normed_group (α × β) :=
 
 lemma prod.norm_def (x : α × β) : ∥x∥ = (max ∥x.1∥ ∥x.2∥) := rfl
 
+lemma prod.nnnorm_def (x : α × β) : nnnorm x = max (nnnorm x.1) (nnnorm x.2) :=
+by { have := x.norm_def, simp only [← coe_nnnorm] at this, exact_mod_cast this }
+
 lemma norm_fst_le (x : α × β) : ∥x.1∥ ≤ ∥x∥ :=
 le_max_left _ _
 

src/measure_theory/integration.lean

@@ -128,6 +128,14 @@ is_measurable_cut (λ _ b, b ∈ s) f (λ b, is_measurable.const (b ∈ s))
 protected theorem measurable [measurable_space β] (f : α →ₛ β) : measurable f :=
 λ s _, is_measurable_preimage f s
 
+protected lemma sum_measure_preimage_singleton (f : α →ₛ β) {μ : measure α} (s : finset β) :
+  ∑ y in s, μ (f ⁻¹' {y}) = μ (f ⁻¹' ↑s) :=
+sum_measure_preimage_singleton _ (λ _ _, f.is_measurable_fiber _)
+
+lemma sum_range_measure_preimage_singleton (f : α →ₛ β) (μ : measure α) :
+  ∑ y in f.range, μ (f ⁻¹' {y}) = μ univ :=
+by rw [f.sum_measure_preimage_singleton, coe_range, preimage_range]
+
 /-- If-then-else as a `simple_func`. -/
 def piecewise (s : set α) (hs : is_measurable s) (f g : α →ₛ β) : α →ₛ β :=
 ⟨s.piecewise f g,
@@ -536,8 +544,7 @@ begin
   simp only [lintegral, range_map],
   refine finset.sum_image' _ (assume b hb, _),
   rcases mem_range.1 hb with ⟨a, rfl⟩,
-  rw [map_preimage_singleton, ← sum_measure_preimage_singleton _
-    (λ _ _, f.is_measurable_preimage _), finset.mul_sum],
+  rw [map_preimage_singleton, ← f.sum_measure_preimage_singleton, finset.mul_sum],
   refine finset.sum_congr _ _,
   { congr },
   { assume x, simp only [finset.mem_filter], rintro ⟨_, h⟩, rw h },

src/measure_theory/l1_space.lean

@@ -505,6 +505,14 @@ lemma integrable_norm_iff [opens_measurable_space β] {f : α → β} (hf : meas
   integrable (λa, ∥f a∥) μ ↔ integrable f μ :=
 by simp_rw [integrable, and_iff_right hf, and_iff_right hf.norm, has_finite_integral_norm_iff]
 
+lemma integrable.prod_mk [opens_measurable_space β] [opens_measurable_space γ] {f : α → β}
+  {g : α → γ} (hf : integrable f μ) (hg : integrable g μ) :
+  integrable (λ x, (f x, g x)) μ :=
+⟨hf.measurable.prod_mk hg.measurable,
+  (hf.norm.add' hg.norm).mono $ eventually_of_forall $ λ x,
+  calc max ∥f x∥ ∥g x∥ ≤ ∥f x∥ + ∥g x∥   : max_le_add_of_nonneg (norm_nonneg _) (norm_nonneg _)
+                 ... ≤ ∥(∥f x∥ + ∥g x∥)∥ : le_abs_self _⟩
+
 section pos_part
 /-! ### Lemmas used for defining the positive part of a `L¹` function -/
 

src/measure_theory/measure_space.lean

@@ -1371,6 +1371,9 @@ instance probability_measure.to_finite_measure (μ : measure α) [probability_me
   finite_measure μ :=
 ⟨by simp only [measure_univ, ennreal.one_lt_top]⟩
 
+lemma probability_measure.ne_zero (μ : measure α) [probability_measure μ] : μ ≠ 0 :=
+mt measure.measure_univ_eq_zero.2 $ by simp [measure_univ]
+
 section no_atoms
 
 variables [has_no_atoms μ]

src/measure_theory/set_integral.lean

@@ -596,6 +596,21 @@ L.integral_comp_comm φ.integrable
 
 end continuous_linear_map
 
+variables [borel_space E] [second_countable_topology E] [complete_space E]
+  [measurable_space F] [borel_space F] [second_countable_topology F] [complete_space F]
+
+lemma fst_integral {f : α → E × F} (hf : integrable f μ) :
+  (∫ x, f x ∂μ).1 = ∫ x, (f x).1 ∂μ :=
+((continuous_linear_map.fst ℝ E F).integral_comp_comm hf).symm
+
+lemma snd_integral {f : α → E × F} (hf : integrable f μ) :
+  (∫ x, f x ∂μ).2 = ∫ x, (f x).2 ∂μ :=
+((continuous_linear_map.snd ℝ E F).integral_comp_comm hf).symm
+
+lemma integral_pair {f : α → E} {g : α → F} (hf : integrable f μ) (hg : integrable g μ) :
+  ∫ x, (f x, g x) ∂μ = (∫ x, f x ∂μ, ∫ x, g x ∂μ) :=
+have _ := hf.prod_mk hg, prod.ext (fst_integral this) (snd_integral this)
+
 end
 
 /-