Exact source: Mathlib/MeasureTheory/Measure/OpenPos.lean
Pinned GitHub source · Raw UTF-8 source
Back to A continuous function with zero weak gradient is constant
1/-2Copyright (c) 2022 Yury Kudryashov. All rights reserved.3Released under Apache 2.0 license as described in the file LICENSE.4Authors: Yury Kudryashov5-/6module78public import Mathlib.MeasureTheory.Constructions.BorelSpace.Basic9public import Mathlib.MeasureTheory.Measure.Typeclasses.NoAtoms10public import Mathlib.MeasureTheory.Measure.Typeclasses.Probability1112/-!13# Measures positive on nonempty opens1415In this file we define a typeclass for measures that are positive on nonempty opens, see16`MeasureTheory.Measure.IsOpenPosMeasure`. Examples include (additive) Haar measures, as well as17measures that have positive density with respect to a Haar measure. We also prove some basic facts18about these measures.1920-/2122public section232425open Topology ENNReal MeasureTheory2627open Set Function Filter2829namespace MeasureTheory3031namespace Measure3233section Basic3435variable {X Y : Type*} [TopologicalSpace X] {m : MeasurableSpace X} [TopologicalSpace Y]36 [T2Space Y] (μ ν : Measure X)3738/-- A measure is said to be `IsOpenPosMeasure` if it is positive on nonempty open sets. -/39class IsOpenPosMeasure : Prop where40 open_pos : ∀ U : Set X, IsOpen U → U.Nonempty → μ U ≠ 04142variable [IsOpenPosMeasure μ] {s U F : Set X} {x : X}4344theorem _root_.IsOpen.measure_ne_zero (hU : IsOpen U) (hne : U.Nonempty) : μ U ≠ 0 :=45 IsOpenPosMeasure.open_pos U hU hne4647theorem _root_.IsOpen.measure_pos (hU : IsOpen U) (hne : U.Nonempty) : 0 < μ U :=48 (hU.measure_ne_zero μ hne).bot_lt4950instance (priority := 100) [Nonempty X] : NeZero μ :=51 ⟨measure_univ_pos.mp <| isOpen_univ.measure_pos μ univ_nonempty⟩5253theorem _root_.IsOpen.measure_pos_iff (hU : IsOpen U) : 0 < μ U ↔ U.Nonempty :=54 ⟨fun h => nonempty_iff_ne_empty.2 fun he => h.ne' <| he.symm ▸ measure_empty, hU.measure_pos μ⟩5556theorem _root_.IsOpen.measure_eq_zero_iff (hU : IsOpen U) : μ U = 0 ↔ U = ∅ := by57 simpa only [not_lt, nonpos_iff_eq_zero, not_nonempty_iff_eq_empty] using58 not_congr (hU.measure_pos_iff μ)5960theorem measure_pos_of_nonempty_interior (h : (interior s).Nonempty) : 0 < μ s :=61 (isOpen_interior.measure_pos μ h).trans_le (measure_mono interior_subset)6263theorem measure_pos_of_mem_nhds (h : s ∈ 𝓝 x) : 0 < μ s :=64 measure_pos_of_nonempty_interior _ ⟨x, mem_interior_iff_mem_nhds.2 h⟩6566theorem isOpenPosMeasure_smul {c : ℝ≥0∞} (h : c ≠ 0) : IsOpenPosMeasure (c • μ) :=67 ⟨fun _U Uo Une => mul_ne_zero h (Uo.measure_ne_zero μ Une)⟩6869variable {μ ν}7071protected theorem AbsolutelyContinuous.isOpenPosMeasure (h : μ ≪ ν) : IsOpenPosMeasure ν :=72 ⟨fun _U ho hne h₀ => ho.measure_ne_zero μ hne (h h₀)⟩7374theorem _root_.LE.le.isOpenPosMeasure (h : μ ≤ ν) : IsOpenPosMeasure ν :=75 h.absolutelyContinuous.isOpenPosMeasure7677theorem _root_.IsOpen.measure_zero_iff_eq_empty (hU : IsOpen U) :78 μ U = 0 ↔ U = ∅ :=79 ⟨fun h ↦ (hU.measure_eq_zero_iff μ).mp h, fun h ↦ by simp [h]⟩8081theorem _root_.IsOpen.ae_eq_empty_iff_eq (hU : IsOpen U) :82 U =ᵐ[μ] (∅ : Set X) ↔ U = ∅ := by83 rw [ae_eq_empty, hU.measure_zero_iff_eq_empty]8485/-- An open null set w.r.t. an `IsOpenPosMeasure` is empty. -/86theorem _root_.IsOpen.eq_empty_of_measure_zero (hU : IsOpen U) (h₀ : μ U = 0) : U = ∅ :=87 (hU.measure_eq_zero_iff μ).mp h₀8889theorem _root_.IsClosed.ae_eq_univ_iff_eq (hF : IsClosed F) :90 F =ᵐ[μ] univ ↔ F = univ := by91 refine ⟨fun h ↦ ?_, fun h ↦ by rw [h]⟩92 rwa [ae_eq_univ, hF.isOpen_compl.measure_eq_zero_iff μ, compl_empty_iff] at h9394theorem _root_.IsClosed.measure_eq_univ_iff_eq [OpensMeasurableSpace X] [IsFiniteMeasure μ]95 (hF : IsClosed F) :96 μ F = μ univ ↔ F = univ := by97 rw [← ae_eq_univ_iff_measure_eq hF.measurableSet.nullMeasurableSet, hF.ae_eq_univ_iff_eq]9899theorem _root_.IsClosed.measure_eq_one_iff_eq_univ [OpensMeasurableSpace X] [IsProbabilityMeasure μ]100 (hF : IsClosed F) :101 μ F = 1 ↔ F = univ := by102 rw [← measure_univ (μ := μ), hF.measure_eq_univ_iff_eq]103104/-- A null set has empty interior. -/105theorem interior_eq_empty_of_null (hs : μ s = 0) : interior s = ∅ :=106 isOpen_interior.eq_empty_of_measure_zero <| measure_mono_null interior_subset hs107108/-- A property satisfied almost everywhere is satisfied on a dense subset. -/109theorem dense_of_ae {p : X → Prop} (hp : ∀ᵐ x ∂μ, p x) : Dense {x | p x} := by110 rw [dense_iff_closure_eq, closure_eq_compl_interior_compl, compl_univ_iff]111 exact μ.interior_eq_empty_of_null hp112113/-- If two functions are a.e. equal on an open set and are continuous on this set, then they are114equal on this set. -/115theorem eqOn_open_of_ae_eq {f g : X → Y} (h : f =ᵐ[μ.restrict U] g) (hU : IsOpen U)116 (hf : ContinuousOn f U) (hg : ContinuousOn g U) : EqOn f g U := by117 replace h := ae_imp_of_ae_restrict h118 simp only [ae_iff, Classical.not_imp] at h119 have : IsOpen (U ∩ { a | f a ≠ g a }) := by120 refine isOpen_iff_mem_nhds.mpr fun a ha => inter_mem (hU.mem_nhds ha.1) ?_121 rcases ha with ⟨ha : a ∈ U, ha' : (f a, g a) ∈ (diagonal Y)ᶜ⟩122 exact123 (hf.continuousAt (hU.mem_nhds ha)).prodMk_nhds (hg.continuousAt (hU.mem_nhds ha))124 (isClosed_diagonal.isOpen_compl.mem_nhds ha')125 replace := (this.eq_empty_of_measure_zero h).le126 exact fun x hx => Classical.not_not.1 fun h => this ⟨hx, h⟩127128/-- If two continuous functions are a.e. equal, then they are equal. -/129theorem eq_of_ae_eq {f g : X → Y} (h : f =ᵐ[μ] g) (hf : Continuous f) (hg : Continuous g) : f = g :=130 suffices EqOn f g univ from funext fun _ => this trivial131 eqOn_open_of_ae_eq (ae_restrict_of_ae h) isOpen_univ hf.continuousOn hg.continuousOn132133theorem eqOn_of_ae_eq {f g : X → Y} (h : f =ᵐ[μ.restrict s] g) (hf : ContinuousOn f s)134 (hg : ContinuousOn g s) (hU : s ⊆ closure (interior s)) : EqOn f g s :=135 have : interior s ⊆ s := interior_subset136 (eqOn_open_of_ae_eq (ae_restrict_of_ae_restrict_of_subset this h) isOpen_interior (hf.mono this)137 (hg.mono this)).of_subset_closure138 hf hg this hU139140variable (μ) in141theorem _root_.Continuous.ae_eq_iff_eq {f g : X → Y} (hf : Continuous f) (hg : Continuous g) :142 f =ᵐ[μ] g ↔ f = g :=143 ⟨fun h => eq_of_ae_eq h hf hg, fun h => h ▸ EventuallyEq.rfl⟩144145theorem _root_.Continuous.isOpenPosMeasure_map [OpensMeasurableSpace X]146 {Z : Type*} [TopologicalSpace Z] [MeasurableSpace Z] [BorelSpace Z]147 {f : X → Z} (hf : Continuous f) (hf_surj : Function.Surjective f) :148 (Measure.map f μ).IsOpenPosMeasure := by149 refine ⟨fun U hUo hUne => ?_⟩150 rw [Measure.map_apply hf.measurable hUo.measurableSet]151 exact (hUo.preimage hf).measure_ne_zero μ (hf_surj.nonempty_preimage.mpr hUne)152153protected theorem IsOpenPosMeasure.comap [BorelSpace X]154 {Z : Type*} [TopologicalSpace Z] {mZ : MeasurableSpace Z} [BorelSpace Z]155 (μ : Measure Z) [IsOpenPosMeasure μ] {f : X → Z} (hf : IsOpenEmbedding f) :156 (μ.comap f).IsOpenPosMeasure where157 open_pos U hU Une := by158 rw [hf.measurableEmbedding.comap_apply]159 exact IsOpenPosMeasure.open_pos _ (hf.isOpen_iff_image_isOpen.mp hU) (Une.image f)160161end Basic162163section LinearOrder164165variable {X Y : Type*} [TopologicalSpace X] [LinearOrder X] [OrderTopology X]166 {m : MeasurableSpace X} [TopologicalSpace Y] [T2Space Y] (μ : Measure X) [IsOpenPosMeasure μ]167168theorem measure_Ioi_pos [NoMaxOrder X] (a : X) : 0 < μ (Ioi a) :=169 isOpen_Ioi.measure_pos μ nonempty_Ioi170171theorem measure_Iio_pos [NoMinOrder X] (a : X) : 0 < μ (Iio a) :=172 isOpen_Iio.measure_pos μ nonempty_Iio173174theorem measure_Ioo_pos [DenselyOrdered X] {a b : X} : 0 < μ (Ioo a b) ↔ a < b :=175 (isOpen_Ioo.measure_pos_iff μ).trans nonempty_Ioo176177theorem measure_Ioo_eq_zero [DenselyOrdered X] {a b : X} : μ (Ioo a b) = 0 ↔ b ≤ a :=178 (isOpen_Ioo.measure_eq_zero_iff μ).trans (Ioo_eq_empty_iff.trans not_lt)179180theorem eqOn_Ioo_of_ae_eq {a b : X} {f g : X → Y} (hfg : f =ᵐ[μ.restrict (Ioo a b)] g)181 (hf : ContinuousOn f (Ioo a b)) (hg : ContinuousOn g (Ioo a b)) : EqOn f g (Ioo a b) :=182 eqOn_of_ae_eq hfg hf hg Ioo_subset_closure_interior183184theorem eqOn_Ioc_of_ae_eq [DenselyOrdered X] {a b : X} {f g : X → Y}185 (hfg : f =ᵐ[μ.restrict (Ioc a b)] g) (hf : ContinuousOn f (Ioc a b))186 (hg : ContinuousOn g (Ioc a b)) : EqOn f g (Ioc a b) :=187 eqOn_of_ae_eq hfg hf hg (Ioc_subset_closure_interior _ _)188189theorem eqOn_Ico_of_ae_eq [DenselyOrdered X] {a b : X} {f g : X → Y}190 (hfg : f =ᵐ[μ.restrict (Ico a b)] g) (hf : ContinuousOn f (Ico a b))191 (hg : ContinuousOn g (Ico a b)) : EqOn f g (Ico a b) :=192 eqOn_of_ae_eq hfg hf hg (Ico_subset_closure_interior _ _)193194theorem eqOn_Icc_of_ae_eq [DenselyOrdered X] {a b : X} (hne : a ≠ b) {f g : X → Y}195 (hfg : f =ᵐ[μ.restrict (Icc a b)] g) (hf : ContinuousOn f (Icc a b))196 (hg : ContinuousOn g (Icc a b)) : EqOn f g (Icc a b) :=197 eqOn_of_ae_eq hfg hf hg (closure_interior_Icc hne).symm.subset198199end LinearOrder200201end Measure202203end MeasureTheory204205open MeasureTheory MeasureTheory.Measure206207namespace Metric208209variable {X : Type*} [PseudoMetricSpace X] {m : MeasurableSpace X} (μ : Measure X)210 [IsOpenPosMeasure μ]211212theorem measure_ball_pos (x : X) {r : ℝ} (hr : 0 < r) : 0 < μ (ball x r) :=213 isOpen_ball.measure_pos μ (nonempty_ball.2 hr)214215/-- See also `Metric.measure_closedBall_pos_iff`. -/216theorem measure_closedBall_pos (x : X) {r : ℝ} (hr : 0 < r) : 0 < μ (closedBall x r) :=217 (measure_ball_pos μ x hr).trans_le (measure_mono ball_subset_closedBall)218219@[simp] lemma measure_closedBall_pos_iff {X : Type*} [MetricSpace X] {m : MeasurableSpace X}220 (μ : Measure X) [IsOpenPosMeasure μ] [NoAtoms μ] {x : X} {r : ℝ} :221 0 < μ (closedBall x r) ↔ 0 < r := by222 refine ⟨fun h ↦ ?_, measure_closedBall_pos μ x⟩223 contrapose! h224 rw [(subsingleton_closedBall x h).measure_zero μ]225226end Metric227228namespace Metric229230variable {X : Type*} [PseudoEMetricSpace X] {m : MeasurableSpace X} (μ : Measure X)231 [IsOpenPosMeasure μ]232233theorem measure_eball_pos (x : X) {r : ℝ≥0∞} (hr : r ≠ 0) : 0 < μ (eball x r) :=234 isOpen_eball.measure_pos μ ⟨x, mem_eball_self hr.bot_lt⟩235236theorem measure_closedEBall_pos (x : X) {r : ℝ≥0∞} (hr : r ≠ 0) : 0 < μ (closedEBall x r) :=237 (measure_eball_pos μ x hr).trans_le (measure_mono eball_subset_closedEBall)238239end Metric240241@[deprecated (since := "2026-01-24")]242alias EMetric.measure_ball_pos := Metric.measure_eball_pos243244@[deprecated (since := "2026-01-24")]245alias EMetric.measure_closedBall_pos := Metric.measure_closedEBall_pos246247section MeasureZero248/-! ## Meagre sets and measure zero249In general, neither of meagre and measure zero implies the other.250- The set of Liouville numbers is a Lebesgue measure zero subset of ℝ, but is not meagre.251 (In fact, its complement is meagre. See `Real.disjoint_residual_ae`.)252253- The complement of the set of Liouville numbers in $[0,1]$ is meagre and has measure 1.254 For another counterexample, for all $α ∈ (0,1)$, there is a generalised Cantor set $C ⊆ [0,1]$255 of measure `α`. Cantor sets are nowhere dense (hence meagre). Taking a countable union of256 fat Cantor sets whose measure approaches 1 even yields a meagre set of measure 1.257258However, with respect to a measure which is positive on non-empty open sets, *closed* measure259zero sets are nowhere dense and σ-compact measure zero sets in a Hausdorff space are meagre.260-/261262variable {X : Type*} [TopologicalSpace X] [MeasurableSpace X] {s : Set X}263 {μ : Measure X} [IsOpenPosMeasure μ]264265/-- A *closed* measure zero subset is nowhere dense. (Closedness is required: for instance, the266rational numbers are countable (thus have measure zero), but are dense (hence not nowhere dense).)267-/268lemma IsNowhereDense.of_isClosed_null (h₁s : IsClosed s) (h₂s : μ s = 0) :269 IsNowhereDense s := h₁s.isNowhereDense_iff.mpr (interior_eq_empty_of_null h₂s)270271/-- A σ-compact measure zero subset is meagre.272(More generally, every Fσ set of measure zero is meagre.) -/273lemma IsMeagre.of_isSigmaCompact_null [T2Space X] (h₁s : IsSigmaCompact s) (h₂s : μ s = 0) :274 IsMeagre s := by275 rcases h₁s with ⟨K, hcompact, hcover⟩276 have h (n : ℕ) : IsNowhereDense (K n) := by277 have : μ (K n) = 0 := measure_mono_null (hcover ▸ subset_iUnion K n) h₂s278 exact .of_isClosed_null (hcompact n).isClosed this279 rw [isMeagre_iff_countable_union_isNowhereDense]280 exact ⟨range K, fun t ⟨n, hn⟩ ↦ hn ▸ h n, countable_range K, hcover.symm.subset⟩281282end MeasureZero