Exact source: MathlibAnnex/MeasureTheory/Function/AEConstant.lean
Pinned GitHub source · Raw UTF-8 source
Back to Identifying constants on an open overlap · Back to From local to global almost-everywhere constancy
1import Mathlib.MeasureTheory.Measure.OpenPos2import Mathlib.MeasureTheory.Measure.Restrict3import Mathlib.Topology.Compactness.Lindelof4import Mathlib.Tactic56/-! Almost-everywhere constant functions and topological gluing.7The codomain is an arbitrary type. Countable gluing uses no topology or8measurability assumption on the cover members. The topological theorem only9uses positivity on nonempty open sets and the Lindelöf property of the domain.10The parent RET2 source was independently elaborated; this bounded repair11revision is qualified by the exact build evidence accompanying this source. -/12noncomputable section13open Set MeasureTheory Filter TopologicalSpace14open scoped ENNReal Topology15namespace MathlibAnnex1617section Measurable18variable {X Y : Type*} [MeasurableSpace X] (μ : Measure X)1920/-- Equality to one constant, almost everywhere on a restricted measure. -/21def AEConstantOn (u : X → Y) (U : Set X) (c : Y) : Prop :=22 ∀ᵐ x ∂μ.restrict U, u x = c2324/-- Countable local exceptional sets can be joined; an uncountable union is not used. -/25theorem aeConstantOn_of_countableCover26 {U : Set X} {u : X → Y} {c : Y}27 {ι : Type*} {V : ι → Set X} {T : Set ι}28 (hT : T.Countable) (hcover : U ⊆ ⋃ i ∈ T, V i)29 (hae : ∀ i ∈ T, AEConstantOn μ u (V i) c) :30 AEConstantOn μ u U c := by31 letI : Encodable T := hT.toEncodable32 apply ae_iff.mpr33 let bad : Set X := {x | u x ≠ c}34 have hcover' : U ⊆ ⋃ i : T, V i := by35 intro x hx36 rcases mem_iUnion₂.mp (hcover hx) with ⟨i, hiT, hxi⟩37 exact mem_iUnion.mpr ⟨⟨i, hiT⟩, hxi⟩38 have hle₁ : μ.restrict U ≤ μ.restrict (⋃ i : T, V i) :=39 Measure.restrict_mono hcover' le_rfl40 have hle₂ : μ.restrict (⋃ i : T, V i) ≤41 Measure.sum (fun i : T => μ.restrict (V i)) := Measure.restrict_iUnion_le42 have hsum : (Measure.sum (fun i : T => μ.restrict (V i))) bad = 0 := by43 rw [Measure.sum_apply_of_countable]44 exact ENNReal.tsum_eq_zero.mpr fun i => by45 simpa only [bad] using ae_iff.mp (hae i i.property)46 change (μ.restrict U) bad = 047 exact nonpos_iff_eq_zero.mp (((hle₁.trans hle₂) bad).trans_eq hsum)48end Measurable4950section Topological51variable {X Y : Type*} [MeasurableSpace X] [TopologicalSpace X]52variable (μ : Measure X)5354/-- A local equality with explicit open-neighborhood and constant witnesses. -/55structure LocalAEConstantAt (U : Set X) (u : X → Y) (x : X) where56 neighborhood : Set X57 isOpen_neighborhood : IsOpen neighborhood58 mem_neighborhood : x ∈ neighborhood59 neighborhood_subset : neighborhood ⊆ U60 constant : Y61 ae_eq : AEConstantOn μ u neighborhood constant6263/-- Points admitting a neighborhood with a specified a.e. constant. -/64def constantRegion (U : Set X) (u : X → Y) (c : Y) : Set X :=65 {x | x ∈ U ∧ ∃ V, IsOpen V ∧ x ∈ V ∧ V ⊆ U ∧ AEConstantOn μ u V c}6667theorem isOpen_constantRegion {U : Set X} {u : X → Y} {c : Y} :68 IsOpen (constantRegion μ U u c) := by69 rw [isOpen_iff_forall_mem_open]70 intro x hx71 rcases hx.2 with ⟨V, hVo, hxV, hVU, hVc⟩72 refine ⟨V, ?_, hVo, hxV⟩73 intro y hy74 exact ⟨hVU hy, V, hVo, hy, hVU, hVc⟩7576/-- A countable subcover is needed only for the domain, not for the entire space. -/77theorem aeConstantOn_of_everywhere_local78 {U : Set X} (hL : IsLindelof U) {u : X → Y} {c : Y}79 (hlocal : ∀ x ∈ U,80 ∃ V, IsOpen V ∧ x ∈ V ∧ V ⊆ U ∧ AEConstantOn μ u V c) :81 AEConstantOn μ u U c := by82 let I := {x : X // x ∈ U}83 choose V hVo hxV hVU hVc using fun x : I => hlocal x x.property84 have hcover : U ⊆ ⋃ x : I, V x := by85 intro y hy86 exact mem_iUnion.mpr ⟨⟨y, hy⟩, hxV ⟨y, hy⟩⟩87 rcases hL.elim_countable_subcover V hVo hcover with ⟨T, hTcount, hTcover⟩88 exact aeConstantOn_of_countableCover μ hTcount hTcover (fun i _ => hVc i)8990variable [μ.IsOpenPosMeasure]9192/-- Positivity of an open overlap identifies its two a.e. constants. -/93theorem aeConstants_eq_of_open_overlap94 {u : X → Y} {V W : Set X} {c d : Y}95 (hVo : IsOpen V) (hWo : IsOpen W) (hVW : (V ∩ W).Nonempty)96 (hc : AEConstantOn μ u V c) (hd : AEConstantOn μ u W d) : c = d := by97 have hpos : 0 < μ (V ∩ W) := (hVo.inter hWo).measure_pos μ hVW98 have hc' : ∀ᵐ y ∂μ.restrict (V ∩ W), u y = c :=99 ae_restrict_of_ae_restrict_of_subset inter_subset_left hc100 have hd' : ∀ᵐ y ∂μ.restrict (V ∩ W), u y = d :=101 ae_restrict_of_ae_restrict_of_subset inter_subset_right hd102 obtain ⟨y, _, hyc, hyd⟩ :=103 Measure.exists_mem_of_measure_ne_zero_of_ae104 (μ := μ) (s := V ∩ W) (ne_of_gt hpos) (hc'.and hd')105 exact hyc.symm.trans hyd106107theorem isOpen_constantRegion_compl108 {U : Set X} {u : X → Y} {c₀ : Y}109 (hlocal : ∀ x ∈ U, Nonempty (LocalAEConstantAt μ U u x)) :110 IsOpen (U \ constantRegion μ U u c₀) := by111 rw [isOpen_iff_forall_mem_open]112 intro x hx113 rcases hlocal x hx.1 with ⟨Lx⟩114 refine ⟨Lx.neighborhood, ?_, Lx.isOpen_neighborhood, Lx.mem_neighborhood⟩115 intro y hy116 refine ⟨Lx.neighborhood_subset hy, ?_⟩117 intro hyS118 rcases hyS.2 with ⟨W, hWo, hyW, hWU, hWc⟩119 have hconst : Lx.constant = c₀ :=120 aeConstants_eq_of_open_overlap μ Lx.isOpen_neighborhood hWo ⟨y, hy, hyW⟩ Lx.ae_eq hWc121 have hxS : x ∈ constantRegion μ U u c₀ := by122 refine ⟨Lx.neighborhood_subset Lx.mem_neighborhood, Lx.neighborhood,123 Lx.isOpen_neighborhood, Lx.mem_neighborhood, Lx.neighborhood_subset, ?_⟩124 simpa [hconst] using Lx.ae_eq125 exact hx.2 hxS126127/-- Preconnectedness suffices once one nonempty constant region is specified. -/128theorem constantRegion_eq_of_preconnected129 {U : Set X} (hU : IsPreconnected U) {u : X → Y} {c₀ : Y}130 (hlocal : ∀ x ∈ U, Nonempty (LocalAEConstantAt μ U u x))131 (hne : (constantRegion μ U u c₀).Nonempty) : constantRegion μ U u c₀ = U := by132 have hSopen := isOpen_constantRegion μ (U := U) (u := u) (c := c₀)133 have hCopen := isOpen_constantRegion_compl μ (c₀ := c₀) hlocal134 have hSsub : constantRegion μ U u c₀ ⊆ U := fun _ hx => hx.1135 have hdis : Disjoint (constantRegion μ U u c₀) (U \ constantRegion μ U u c₀) :=136 Set.disjoint_left.2 fun _ hxS hxC => hxC.2 hxS137 have hcover : U ⊆ constantRegion μ U u c₀ ∪ (U \ constantRegion μ U u c₀) := by138 intro y hy139 by_cases hyS : y ∈ constantRegion μ U u c₀140 · exact Or.inl hyS141 · exact Or.inr ⟨hy, hyS⟩142 rcases hU.subset_or_subset hSopen hCopen hdis hcover with hUS | hUC143 · exact Set.Subset.antisymm hSsub hUS144 · exfalso145 rcases hne with ⟨y, hyS⟩146 exact (hUC (hSsub hyS)).2 hyS147148/-- General local-to-global a.e. constancy on a connected Lindelöf domain. -/149theorem exists_aeConstantOn_of_local150 {U : Set X} (hU : IsConnected U) (hL : IsLindelof U) {u : X → Y}151 (hlocal : ∀ x ∈ U, Nonempty (LocalAEConstantAt μ U u x)) :152 ∃ c : Y, AEConstantOn μ u U c := by153 rcases hU.nonempty with ⟨x₀, hx₀⟩154 rcases hlocal x₀ hx₀ with ⟨L₀⟩155 have hxregion : x₀ ∈ constantRegion μ U u L₀.constant :=156 ⟨hx₀, L₀.neighborhood, L₀.isOpen_neighborhood, L₀.mem_neighborhood,157 L₀.neighborhood_subset, L₀.ae_eq⟩158 have hregion := constantRegion_eq_of_preconnected μ hU.2 hlocal ⟨x₀, hxregion⟩159 refine ⟨L₀.constant, aeConstantOn_of_everywhere_local μ hL ?_⟩160 intro x hx161 have hxS : x ∈ constantRegion μ U u L₀.constant := by simpa [hregion] using hx162 exact hxS.2163164/-- Empty domains are permitted when the codomain has a possible constant. -/165theorem exists_aeConstantOn_of_local_preconnected [Nonempty Y]166 {U : Set X} (hU : IsPreconnected U) (hL : IsLindelof U) {u : X → Y}167 (hlocal : ∀ x ∈ U, Nonempty (LocalAEConstantAt μ U u x)) :168 ∃ c : Y, AEConstantOn μ u U c := by169 classical170 rcases U.eq_empty_or_nonempty with rfl | hne171 · exact ⟨Classical.choice ‹Nonempty Y›, by simp [AEConstantOn]⟩172 · exact exists_aeConstantOn_of_local μ ⟨hne, hU⟩ hL hlocal173174end Topological175end MathlibAnnex