feat(measure_theory/measure/finite_measure_weak_convergence): Prove o…

…ne implication of portmanteau theorem, convergence implies a limsup condition for measures of closed sets. (#14116)

This PR contains the proof of one implication of portmanteau theorem characterizing weak convergence: it is shown that weak convergence implies that for any closed set the limsup of measures is at most the limit measure.



Co-authored-by: kkytola <39528102+kkytola@users.noreply.github.com>

src/measure_theory/integral/lebesgue.lean

@@ -1053,6 +1053,17 @@ by rw [lintegral_const, measure.restrict_apply_univ]
 lemma set_lintegral_one (s) : ∫⁻ a in s, 1 ∂μ = μ s :=
 by rw [set_lintegral_const, one_mul]
 
+lemma set_lintegral_const_lt_top [is_finite_measure μ] (s : set α) {c : ℝ≥0∞} (hc : c ≠ ∞) :
+  ∫⁻ a in s, c ∂μ < ∞ :=
+begin
+  rw lintegral_const,
+  exact ennreal.mul_lt_top hc (measure_ne_top (μ.restrict s) univ),
+end
+
+lemma lintegral_const_lt_top [is_finite_measure μ] {c : ℝ≥0∞} (hc : c ≠ ∞) :
+  ∫⁻ a, c ∂μ < ∞ :=
+by simpa only [measure.restrict_univ] using set_lintegral_const_lt_top univ hc
+
 section
 
 variable (μ)

src/measure_theory/integral/set_integral.lean

@@ -6,6 +6,7 @@ Authors: Zhouhang Zhou, Yury Kudryashov
 import measure_theory.integral.integrable_on
 import measure_theory.integral.bochner
 import order.filter.indicator_function
+import topology.metric_space.thickened_indicator
 
 /-!
 # Set integral
@@ -962,3 +963,30 @@ lemma set_integral_with_density_eq_set_integral_smul₀ {f : α → ℝ≥0} {s
 by rw [restrict_with_density hs, integral_with_density_eq_integral_smul₀ hf]
 
 end
+
+section thickened_indicator
+
+variables [pseudo_emetric_space α]
+
+lemma measure_le_lintegral_thickened_indicator_aux
+  (μ : measure α) {E : set α} (E_mble : measurable_set E) (δ : ℝ) :
+  μ E ≤ ∫⁻ a, (thickened_indicator_aux δ E a : ℝ≥0∞) ∂μ :=
+begin
+  convert_to lintegral μ (E.indicator (λ _, (1 : ℝ≥0∞)))
+              ≤ lintegral μ (thickened_indicator_aux δ E),
+  { rw [lintegral_indicator _ E_mble],
+    simp only [lintegral_one, measure.restrict_apply, measurable_set.univ, univ_inter], },
+  { apply lintegral_mono,
+    apply indicator_le_thickened_indicator_aux, },
+end
+
+lemma measure_le_lintegral_thickened_indicator
+  (μ : measure α) {E : set α} (E_mble : measurable_set E) {δ : ℝ} (δ_pos : 0 < δ) :
+  μ E ≤ ∫⁻ a, (thickened_indicator δ_pos E a : ℝ≥0∞) ∂μ :=
+begin
+  convert measure_le_lintegral_thickened_indicator_aux μ E_mble δ,
+  dsimp,
+  simp only [thickened_indicator_aux_lt_top.ne, ennreal.coe_to_nnreal, ne.def, not_false_iff],
+end
+
+end thickened_indicator

src/measure_theory/measure/finite_measure_weak_convergence.lean

@@ -4,9 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kalle Kytölä
 -/
 import measure_theory.measure.measure_space
-import measure_theory.integral.bochner
+import measure_theory.integral.set_integral
 import topology.continuous_function.bounded
 import topology.algebra.module.weak_dual
+import topology.metric_space.thickened_indicator
 
 /-!
 # Weak convergence of (finite) measures
@@ -42,7 +43,14 @@ The main definitions are the
    common textbook definition of weak convergence of measures.
 
 TODO:
-* Portmanteau theorem.
+* Portmanteau theorem:
+  * `finite_measure.limsup_measure_closed_le_of_tendsto` proves one implication.
+    The current formulation assumes `pseudo_emetric_space`. The only reason is to have
+    bounded continuous pointwise approximations to the indicator function of a closed set. Clearly
+    for example metrizability or pseudo-emetrizability would be sufficient assumptions. The
+    typeclass assumptions should be later adjusted in a way that takes into account use cases, but
+    the proof will presumably remain essentially the same.
+  * Prove the rest of the implications.
 
 ## Notations
 
@@ -328,6 +336,80 @@ begin
            ennreal.tendsto_coe, ennreal.to_nnreal_coe],
 end
 
+/-- A bounded convergence theorem for a finite measure:
+If bounded continuous non-negative functions are uniformly bounded by a constant and tend to a
+limit, then their integrals against the finite measure tend to the integral of the limit.
+This formulation assumes:
+ * the functions tend to a limit along a countably generated filter;
+ * the limit is in the almost everywhere sense;
+ * boundedness holds almost everywhere;
+ * integration is `lintegral`, i.e., the functions and their integrals are `ℝ≥0∞`-valued.
+-/
+lemma tendsto_lintegral_nn_filter_of_le_const {ι : Type*} {L : filter ι} [L.is_countably_generated]
+  (μ : finite_measure α) {fs : ι → (α →ᵇ ℝ≥0)} {c : ℝ≥0}
+  (fs_le_const : ∀ᶠ i in L, ∀ᵐ (a : α) ∂(μ : measure α), fs i a ≤ c) {f : α → ℝ≥0}
+  (fs_lim : ∀ᵐ (a : α) ∂(μ : measure α), tendsto (λ i, fs i a) L (𝓝 (f a))) :
+  tendsto (λ i, (∫⁻ a, fs i a ∂(μ : measure α))) L (𝓝 (∫⁻ a, (f a) ∂(μ : measure α))) :=
+begin
+  simpa only using tendsto_lintegral_filter_of_dominated_convergence (λ _, c)
+    (eventually_of_forall ((λ i, (ennreal.continuous_coe.comp (fs i).continuous).measurable)))
+    _ ((@lintegral_const_lt_top _ _ (μ : measure α) _ _ (@ennreal.coe_ne_top c)).ne) _,
+  { simpa only [ennreal.coe_le_coe] using fs_le_const, },
+  { simpa only [ennreal.tendsto_coe] using fs_lim, },
+end
+
+/-- A bounded convergence theorem for a finite measure:
+If a sequence of bounded continuous non-negative functions are uniformly bounded by a constant
+and tend pointwise to a limit, then their integrals (`lintegral`) against the finite measure tend
+to the integral of the limit.
+
+A related result with more general assumptions is `tendsto_lintegral_nn_filter_of_le_const`.
+-/
+lemma tendsto_lintegral_nn_of_le_const (μ : finite_measure α) {fs : ℕ → (α →ᵇ ℝ≥0)} {c : ℝ≥0}
+  (fs_le_const : ∀ n a, fs n a ≤ c) {f : α → ℝ≥0}
+  (fs_lim : ∀ a, tendsto (λ n, fs n a) at_top (𝓝 (f a))) :
+  tendsto (λ n, (∫⁻ a, fs n a ∂(μ : measure α))) at_top (𝓝 (∫⁻ a, (f a) ∂(μ : measure α))) :=
+tendsto_lintegral_nn_filter_of_le_const μ
+  (eventually_of_forall (λ n, eventually_of_forall (fs_le_const n))) (eventually_of_forall fs_lim)
+
+/-- A bounded convergence theorem for a finite measure:
+If bounded continuous non-negative functions are uniformly bounded by a constant and tend to a
+limit, then their integrals against the finite measure tend to the integral of the limit.
+This formulation assumes:
+ * the functions tend to a limit along a countably generated filter;
+ * the limit is in the almost everywhere sense;
+ * boundedness holds almost everywhere;
+ * integration is the pairing against non-negative continuous test functions (`test_against_nn`).
+
+A related result using `lintegral` for integration is `tendsto_lintegral_nn_filter_of_le_const`.
+-/
+lemma tendsto_test_against_nn_filter_of_le_const {ι : Type*} {L : filter ι}
+  [L.is_countably_generated] {μ : finite_measure α} {fs : ι → (α →ᵇ ℝ≥0)} {c : ℝ≥0}
+  (fs_le_const : ∀ᶠ i in L, ∀ᵐ (a : α) ∂(μ : measure α), fs i a ≤ c) {f : α →ᵇ ℝ≥0}
+  (fs_lim : ∀ᵐ (a : α) ∂(μ : measure α), tendsto (λ i, fs i a) L (𝓝 (f a))) :
+  tendsto (λ i, μ.test_against_nn (fs i)) L (𝓝 (μ.test_against_nn f)) :=
+begin
+  apply (ennreal.tendsto_to_nnreal
+         (μ.lintegral_lt_top_of_bounded_continuous_to_nnreal f).ne).comp,
+  exact finite_measure.tendsto_lintegral_nn_filter_of_le_const μ fs_le_const fs_lim,
+end
+
+/-- A bounded convergence theorem for a finite measure:
+If a sequence of bounded continuous non-negative functions are uniformly bounded by a constant
+and tend pointwise to a limit, then their integrals (`test_against_nn`) against the finite measure
+tend to the integral of the limit.
+
+Related results:
+ * `tendsto_test_against_nn_filter_of_le_const`: more general assumptions
+ * `tendsto_lintegral_nn_of_le_const`: using `lintegral` for integration.
+-/
+lemma tendsto_test_against_nn_of_le_const {μ : finite_measure α}
+  {fs : ℕ → (α →ᵇ ℝ≥0)} {c : ℝ≥0} (fs_le_const : ∀ n a, fs n a ≤ c) {f : α →ᵇ ℝ≥0}
+  (fs_lim : ∀ a, tendsto (λ n, fs n a) at_top (𝓝 (f a))) :
+  tendsto (λ n, μ.test_against_nn (fs n)) at_top (𝓝 (μ.test_against_nn f)) :=
+tendsto_test_against_nn_filter_of_le_const
+  (eventually_of_forall (λ n, eventually_of_forall (fs_le_const n))) (eventually_of_forall fs_lim)
+
 end finite_measure
 
 /-- Probability measures are defined as the subtype of measures that have the property of being
@@ -447,4 +529,112 @@ end
 
 end probability_measure
 
+section convergence_implies_limsup_closed_le
+
+/-- If bounded continuous functions tend to the indicator of a measurable set and are
+uniformly bounded, then their integrals against a finite measure tend to the measure of the set.
+This formulation assumes:
+ * the functions tend to a limit along a countably generated filter;
+ * the limit is in the almost everywhere sense;
+ * boundedness holds almost everywhere.
+-/
+lemma measure_of_cont_bdd_of_tendsto_filter_indicator {ι : Type*} {L : filter ι}
+  [L.is_countably_generated] [topological_space α] [opens_measurable_space α]
+  (μ : finite_measure α) {c : ℝ≥0} {E : set α} (E_mble : measurable_set E)
+  (fs : ι → (α →ᵇ ℝ≥0)) (fs_bdd : ∀ᶠ i in L, ∀ᵐ (a : α) ∂(μ : measure α), fs i a ≤ c)
+  (fs_lim : ∀ᵐ (a : α) ∂(μ : measure α),
+            tendsto (λ (i : ι), (coe_fn : (α →ᵇ ℝ≥0) → (α → ℝ≥0)) (fs i) a) L
+                    (𝓝 (indicator E (λ x, (1 : ℝ≥0)) a))) :
+  tendsto (λ n, lintegral (μ : measure α) (λ a, fs n a)) L (𝓝 ((μ : measure α) E)) :=
+begin
+  convert finite_measure.tendsto_lintegral_nn_filter_of_le_const μ fs_bdd fs_lim,
+  have aux : ∀ a, indicator E (λ x, (1 : ℝ≥0∞)) a = ↑(indicator E (λ x, (1 : ℝ≥0)) a),
+  from λ a, by simp only [ennreal.coe_indicator, ennreal.coe_one],
+  simp_rw [←aux, lintegral_indicator _ E_mble],
+  simp only [lintegral_one, measure.restrict_apply, measurable_set.univ, univ_inter],
+end
+
+/-- If a sequence of bounded continuous functions tends to the indicator of a measurable set and
+the functions are uniformly bounded, then their integrals against a finite measure tend to the
+measure of the set.
+
+A similar result with more general assumptions is `measure_of_cont_bdd_of_tendsto_filter_indicator`.
+-/
+lemma measure_of_cont_bdd_of_tendsto_indicator
+  [topological_space α] [opens_measurable_space α]
+  (μ : finite_measure α) {c : ℝ≥0} {E : set α} (E_mble : measurable_set E)
+  (fs : ℕ → (α →ᵇ ℝ≥0)) (fs_bdd : ∀ n a, fs n a ≤ c)
+  (fs_lim : tendsto (λ (n : ℕ), (coe_fn : (α →ᵇ ℝ≥0) → (α → ℝ≥0)) (fs n))
+            at_top (𝓝 (indicator E (λ x, (1 : ℝ≥0))))) :
+  tendsto (λ n, lintegral (μ : measure α) (λ a, fs n a)) at_top (𝓝 ((μ : measure α) E)) :=
+begin
+  have fs_lim' : ∀ a, tendsto (λ (n : ℕ), (fs n a : ℝ≥0))
+                 at_top (𝓝 (indicator E (λ x, (1 : ℝ≥0)) a)),
+  by { rw tendsto_pi_nhds at fs_lim, exact λ a, fs_lim a, },
+  apply measure_of_cont_bdd_of_tendsto_filter_indicator μ E_mble fs
+      (eventually_of_forall (λ n, eventually_of_forall (fs_bdd n))) (eventually_of_forall fs_lim'),
+end
+
+/-- The integrals of thickenined indicators of a closed set against a finite measure tend to the
+measure of the closed set if the thickening radii tend to zero.
+-/
+lemma tendsto_lintegral_thickened_indicator_of_is_closed
+  {α : Type*} [measurable_space α] [pseudo_emetric_space α] [opens_measurable_space α]
+  (μ : finite_measure α) {F : set α} (F_closed : is_closed F) {δs : ℕ → ℝ}
+  (δs_pos : ∀ n, 0 < δs n) (δs_lim : tendsto δs at_top (𝓝 0)) :
+  tendsto (λ n, lintegral (μ : measure α) (λ a, (thickened_indicator (δs_pos n) F a : ℝ≥0∞)))
+          at_top (𝓝 ((μ : measure α) F)) :=
+begin
+  apply measure_of_cont_bdd_of_tendsto_indicator μ F_closed.measurable_set
+          (λ n, thickened_indicator (δs_pos n) F)
+          (λ n a, thickened_indicator_le_one (δs_pos n) F a),
+  have key := thickened_indicator_tendsto_indicator_closure δs_pos δs_lim F,
+  rwa F_closed.closure_eq at key,
+end
+
+/-- One implication of the portmanteau theorem:
+Weak convergence of finite measures implies that the limsup of the measures of any closed set is
+at most the measure of the closed set under the limit measure.
+-/
+lemma finite_measure.limsup_measure_closed_le_of_tendsto
+  {α ι : Type*} {L : filter ι}
+  [measurable_space α] [pseudo_emetric_space α] [opens_measurable_space α]
+  {μ : finite_measure α} {μs : ι → finite_measure α}
+  (μs_lim : tendsto μs L (𝓝 μ)) {F : set α} (F_closed : is_closed F) :
+  L.limsup (λ i, (μs i : measure α) F) ≤ (μ : measure α) F :=
+begin
+  by_cases L = ⊥,
+  { simp only [h, limsup, filter.map_bot, Limsup_bot, ennreal.bot_eq_zero, zero_le], },
+  apply ennreal.le_of_forall_pos_le_add,
+  intros ε ε_pos μ_F_finite,
+  set δs := λ (n : ℕ), (1 : ℝ) / (n+1) with def_δs,
+  have δs_pos : ∀ n, 0 < δs n, from λ n, nat.one_div_pos_of_nat,
+  have δs_lim : tendsto δs at_top (𝓝 0), from tendsto_one_div_add_at_top_nhds_0_nat,
+  have key₁ := tendsto_lintegral_thickened_indicator_of_is_closed μ F_closed δs_pos δs_lim,
+  have room₁ : (μ : measure α) F < (μ : measure α) F + ε / 2,
+  { apply ennreal.lt_add_right (measure_lt_top (μ : measure α) F).ne
+          ((ennreal.div_pos_iff.mpr
+              ⟨(ennreal.coe_pos.mpr ε_pos).ne.symm, ennreal.two_ne_top⟩).ne.symm), },
+  rcases eventually_at_top.mp (eventually_lt_of_tendsto_lt room₁ key₁) with ⟨M, hM⟩,
+  have key₂ := finite_measure.tendsto_iff_forall_lintegral_tendsto.mp
+                μs_lim (thickened_indicator (δs_pos M) F),
+  have room₂ : lintegral (μ : measure α) (λ a, thickened_indicator (δs_pos M) F a)
+                < lintegral (μ : measure α) (λ a, thickened_indicator (δs_pos M) F a) + ε / 2,
+  { apply ennreal.lt_add_right
+          (finite_measure.lintegral_lt_top_of_bounded_continuous_to_nnreal μ _).ne
+          ((ennreal.div_pos_iff.mpr
+              ⟨(ennreal.coe_pos.mpr ε_pos).ne.symm, ennreal.two_ne_top⟩).ne.symm), },
+  have ev_near := eventually.mono (eventually_lt_of_tendsto_lt room₂ key₂) (λ n, le_of_lt),
+  have aux := λ n, le_trans (measure_le_lintegral_thickened_indicator
+                            (μs n : measure α) F_closed.measurable_set (δs_pos M)),
+  have ev_near' := eventually.mono ev_near aux,
+  apply (filter.limsup_le_limsup ev_near').trans,
+  haveI : ne_bot L, from ⟨h⟩,
+  rw limsup_const,
+  apply le_trans (add_le_add (hM M rfl.le).le (le_refl (ε/2 : ℝ≥0∞))),
+  simp only [add_assoc, ennreal.add_halves, le_refl],
+end
+
+end convergence_implies_limsup_closed_le
+
 end measure_theory

src/topology/metric_space/thickened_indicator.lean

@@ -98,6 +98,15 @@ lemma thickened_indicator_aux_mono {δ₁ δ₂ : ℝ} (hle : δ₁ ≤ δ₂) (
   thickened_indicator_aux δ₁ E ≤ thickened_indicator_aux δ₂ E :=
 λ _, tsub_le_tsub (@rfl ℝ≥0∞ 1).le (ennreal.div_le_div rfl.le (of_real_le_of_real hle))
 
+lemma indicator_le_thickened_indicator_aux (δ : ℝ) (E : set α) :
+  E.indicator (λ _, (1 : ℝ≥0∞)) ≤ thickened_indicator_aux δ E :=
+begin
+  intro a,
+  by_cases a ∈ E,
+  { simp only [h, indicator_of_mem, thickened_indicator_aux_one δ E h, le_refl], },
+  { simp only [h, indicator_of_not_mem, not_false_iff, zero_le], },
+end
+
 lemma thickened_indicator_aux_subset (δ : ℝ) {E₁ E₂ : set α} (subset : E₁ ⊆ E₂) :
   thickened_indicator_aux δ E₁ ≤ thickened_indicator_aux δ E₂ :=
 λ _, tsub_le_tsub (@rfl ℝ≥0∞ 1).le (ennreal.div_le_div (inf_edist_anti subset) rfl.le)
@@ -196,6 +205,15 @@ lemma thickened_indicator_zero
   thickened_indicator δ_pos E x = 0 :=
 by rw [thickened_indicator_apply, thickened_indicator_aux_zero δ_pos E x_out, zero_to_nnreal]
 
+lemma indicator_le_thickened_indicator {δ : ℝ} (δ_pos : 0 < δ) (E : set α) :
+  E.indicator (λ _, (1 : ℝ≥0)) ≤ thickened_indicator δ_pos E :=
+begin
+  intro a,
+  by_cases a ∈ E,
+  { simp only [h, indicator_of_mem, thickened_indicator_one δ_pos E h, le_refl], },
+  { simp only [h, indicator_of_not_mem, not_false_iff, zero_le], },
+end
+
 lemma thickened_indicator_mono {δ₁ δ₂ : ℝ}
   (δ₁_pos : 0 < δ₁) (δ₂_pos : 0 < δ₂) (hle : δ₁ ≤ δ₂) (E : set α) :
   ⇑(thickened_indicator δ₁_pos E) ≤ thickened_indicator δ₂_pos E :=