-
Notifications
You must be signed in to change notification settings - Fork 259
/
Measure.lean
89 lines (77 loc) · 4.43 KB
/
Measure.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
/-
Copyright (c) 2022 Yury Kudryashov. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yury Kudryashov
-/
import Mathlib.Analysis.Convex.Topology
import Mathlib.Analysis.NormedSpace.AddTorsorBases
import Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
#align_import analysis.convex.measure from "leanprover-community/mathlib"@"fd5edc43dc4f10b85abfe544b88f82cf13c5f844"
/-!
# 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.addHaar_frontier`), hence
`s` is a `NullMeasurableSet` (see `Convex.nullMeasurableSet`).
-/
open MeasureTheory MeasureTheory.Measure Set Metric Filter Bornology
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 addHaar_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 ?_ (addHaar_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 → IsBounded t → μ (frontier t) = 0 by
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 _ _)) ?_ (isBounded_ball.subset 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 [B, N, Nat.lt_floor_add_one]
suffices y ∈ frontier (s ∩ B N) ∩ B N from 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) ≠ ∞ := (hb.subset 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) := fun r hr ↦ by
refine (measure_mono <|
hs.closure_subset_image_homothety_interior_of_one_lt hx r hr).trans_eq ?_
rw [addHaar_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.addHaar_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.addHaar_frontier μ)
#align convex.null_measurable_set Convex.nullMeasurableSet
end Convex