feat: port Analysis.Convex.Measure (#4911)

Mathlib.lean

@@ -541,6 +541,7 @@ import Mathlib.Analysis.Convex.Integral
 import Mathlib.Analysis.Convex.Jensen
 import Mathlib.Analysis.Convex.Join
 import Mathlib.Analysis.Convex.KreinMilman
+import Mathlib.Analysis.Convex.Measure
 import Mathlib.Analysis.Convex.Normed
 import Mathlib.Analysis.Convex.PartitionOfUnity
 import Mathlib.Analysis.Convex.Quasiconvex

Mathlib/Analysis/Convex/Measure.lean

@@ -0,0 +1,94 @@
+/-
+Copyright (c) 2022 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov
+
+! This file was ported from Lean 3 source module analysis.convex.measure
+! leanprover-community/mathlib commit fd5edc43dc4f10b85abfe544b88f82cf13c5f844
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.Analysis.Convex.Topology
+import Mathlib.Analysis.NormedSpace.AddTorsorBases
+import Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
+
+/-!
+# Convex sets are null-measurable
+
+Let `E` be a finite dimensional real vector space, let `μ` be a Haar measure on `E`, let `s` be a
+convex set in `E`. Then the frontier of `s` has measure zero (see `Convex.add_haar_frontier`), hence
+`s` is a `NullMeasurableSet` (see `Convex.nullMeasurableSet`).
+-/
+
+
+open MeasureTheory MeasureTheory.Measure Set Metric Filter
+
+open FiniteDimensional (finrank)
+
+open scoped Topology NNReal ENNReal
+
+variable {E : Type _} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E]
+  [FiniteDimensional ℝ E] (μ : Measure E) [IsAddHaarMeasure μ] {s : Set E}
+
+namespace Convex
+
+/-- Haar measure of the frontier of a convex set is zero. -/
+theorem add_haar_frontier (hs : Convex ℝ s) : μ (frontier s) = 0 := by
+  /- If `s` is included in a hyperplane, then `frontier s ⊆ closure s` is included in the same
+    hyperplane, hence it has measure zero. -/
+  cases' ne_or_eq (affineSpan ℝ s) ⊤ with hspan hspan
+  · refine' measure_mono_null _ (add_haar_affineSubspace _ _ hspan)
+    exact frontier_subset_closure.trans
+      (closure_minimal (subset_affineSpan _ _) (affineSpan ℝ s).closed_of_finiteDimensional)
+  rw [← hs.interior_nonempty_iff_affineSpan_eq_top] at hspan
+  rcases hspan with ⟨x, hx⟩
+  /- Without loss of generality, `s` is bounded. Indeed, `∂s ⊆ ⋃ n, ∂(s ∩ ball x (n + 1))`, hence it
+    suffices to prove that `∀ n, μ (s ∩ ball x (n + 1)) = 0`; the latter set is bounded.
+    -/
+  suffices H : ∀ t : Set E, Convex ℝ t → x ∈ interior t → Bounded t → μ (frontier t) = 0
+  · let B : ℕ → Set E := fun n => ball x (n + 1)
+    have : μ (⋃ n : ℕ, frontier (s ∩ B n)) = 0 := by
+      refine' measure_iUnion_null fun n =>
+        H _ (hs.inter (convex_ball _ _)) _ (bounded_ball.mono (inter_subset_right _ _))
+      rw [interior_inter, isOpen_ball.interior_eq]
+      exact ⟨hx, mem_ball_self (add_pos_of_nonneg_of_pos n.cast_nonneg zero_lt_one)⟩
+    refine' measure_mono_null (fun y hy => _) this; clear this
+    set N : ℕ := ⌊dist y x⌋₊
+    refine' mem_iUnion.2 ⟨N, _⟩
+    have hN : y ∈ B N := by simp [Nat.lt_floor_add_one]
+    suffices : y ∈ frontier (s ∩ B N) ∩ B N; exact this.1
+    rw [frontier_inter_open_inter isOpen_ball]
+    exact ⟨hy, hN⟩
+  intro s hs hx hb
+  /- Since `s` is bounded, we have `μ (interior s) ≠ ∞`, hence it suffices to prove
+    `μ (closure s) ≤ μ (interior s)`. -/
+  replace hb : μ (interior s) ≠ ∞
+  exact (hb.mono interior_subset).measure_lt_top.ne
+  suffices μ (closure s) ≤ μ (interior s) by
+    rwa [frontier, measure_diff interior_subset_closure isOpen_interior.measurableSet hb,
+      tsub_eq_zero_iff_le]
+  /- Due to `Convex.closure_subset_image_homothety_interior_of_one_lt`, for any `r > 1` we have
+    `closure s ⊆ homothety x r '' interior s`, hence `μ (closure s) ≤ r ^ d * μ (interior s)`,
+    where `d = finrank ℝ E`. -/
+  set d : ℕ := FiniteDimensional.finrank ℝ E
+  have : ∀ r : ℝ≥0, 1 < r → μ (closure s) ≤ ↑(r ^ d) * μ (interior s) := by
+    intro r hr
+    refine' (measure_mono <|
+      hs.closure_subset_image_homothety_interior_of_one_lt hx r hr).trans_eq _
+    rw [add_haar_image_homothety, ← NNReal.coe_pow, NNReal.abs_eq, ENNReal.ofReal_coe_nnreal]
+  have : ∀ᶠ (r : ℝ≥0) in 𝓝[>] 1, μ (closure s) ≤ ↑(r ^ d) * μ (interior s) :=
+    mem_of_superset self_mem_nhdsWithin this
+  -- Taking the limit as `r → 1`, we get `μ (closure s) ≤ μ (interior s)`.
+  refine' ge_of_tendsto _ this
+  refine' (((ENNReal.continuous_mul_const hb).comp
+    (ENNReal.continuous_coe.comp (continuous_pow d))).tendsto' _ _ _).mono_left nhdsWithin_le_nhds
+  simp
+#align convex.add_haar_frontier Convex.add_haar_frontier
+
+/-- A convex set in a finite dimensional real vector space is null measurable with respect to an
+additive Haar measure on this space. -/
+protected theorem nullMeasurableSet (hs : Convex ℝ s) : NullMeasurableSet s μ :=
+  nullMeasurableSet_of_null_frontier (hs.add_haar_frontier μ)
+#align convex.null_measurable_set Convex.nullMeasurableSet
+
+end Convex