Lean4
/-- If a function `f : α → β` is such that the level sets `{f < p}` and `{q < f}` have measurable
supersets which are disjoint up to measure zero when `p < q`, then `f` is almost-everywhere
measurable. It is even enough to have this for `p` and `q` in a countable dense set. -/
theorem aemeasurable_of_exist_almost_disjoint_supersets {α : Type*} {m : MeasurableSpace α} (μ : Measure α) {β : Type*}
[CompleteLinearOrder β] [DenselyOrdered β] [TopologicalSpace β] [OrderTopology β] [SecondCountableTopology β]
[MeasurableSpace β] [BorelSpace β] (s : Set β) (s_count : s.Countable) (s_dense : Dense s) (f : α → β)
(h :
∀ p ∈ s,
∀ q ∈ s,
p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ μ (u ∩ v) = 0) :
AEMeasurable f μ := by
classical
haveI : Encodable s := s_count.toEncodable
have h' :
∀ p q,
∃ u v,
MeasurableSet u ∧
MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ (p ∈ s → q ∈ s → p < q → μ (u ∩ v) = 0) :=
by
intro p q
by_cases H : p ∈ s ∧ q ∈ s ∧ p < q
· rcases h p H.1 q H.2.1 H.2.2 with ⟨u, v, hu, hv, h'u, h'v, hμ⟩
exact ⟨u, v, hu, hv, h'u, h'v, fun _ _ _ => hμ⟩
· refine ⟨univ, univ, MeasurableSet.univ, MeasurableSet.univ, subset_univ _, subset_univ _, fun ps qs pq => ?_⟩
simp only [not_and] at H
exact (H ps qs pq).elim
choose! u v huv using h'
let u' : β → Set α := fun p => ⋂ q ∈ s ∩ Ioi p, u p q
have u'_meas : ∀ i, MeasurableSet (u' i) := by
intro i
exact MeasurableSet.biInter (s_count.mono inter_subset_left) fun b _ => (huv i b).1
let f' : α → β := fun x => ⨅ i : s, piecewise (u' i) (fun _ => (i : β)) (fun _ => (⊤ : β)) x
have f'_meas : Measurable f' := by fun_prop (disch := simp_all)
let t := ⋃ (p : s) (q : ↥(s ∩ Ioi p)), u' p ∩ v p q
have μt : μ t ≤ 0 :=
calc
μ t ≤ ∑' (p : s) (q : ↥(s ∩ Ioi p)), μ (u' p ∩ v p q) :=
by
refine (measure_iUnion_le _).trans ?_
refine ENNReal.tsum_le_tsum fun p => ?_
haveI := (s_count.mono (s.inter_subset_left (t := Ioi ↑p))).to_subtype
apply measure_iUnion_le
_ ≤ ∑' (p : s) (q : ↥(s ∩ Ioi p)), μ (u p q ∩ v p q) :=
by
gcongr with p q
exact biInter_subset_of_mem q.2
_ = ∑' (p : s) (_ : ↥(s ∩ Ioi p)), (0 : ℝ≥0∞) := by grind
_ = 0 := by simp only [tsum_zero]
have ff' : ∀ᵐ x ∂μ, f x = f' x :=
by
have : ∀ᵐ x ∂μ, x ∉ t := by
have : μ t = 0 := le_antisymm μt bot_le
change μ _ = 0
convert this
ext y
simp only [mem_setOf_eq, mem_compl_iff, not_notMem]
filter_upwards [this] with x hx
apply (iInf_eq_of_forall_ge_of_forall_gt_exists_lt _ _).symm
· intro i
by_cases H : x ∈ u' i
swap
· simp only [H, le_top, not_false_iff, piecewise_eq_of_notMem]
simp only [H, piecewise_eq_of_mem]
contrapose! hx
obtain ⟨r, ⟨xr, rq⟩, rs⟩ : ∃ r, r ∈ Ioo (i : β) (f x) ∩ s :=
dense_iff_inter_open.1 s_dense (Ioo i (f x)) isOpen_Ioo (nonempty_Ioo.2 hx)
have A : x ∈ v i r := (huv i r).2.2.2.1 rq
refine mem_iUnion.2 ⟨i, ?_⟩
refine mem_iUnion.2 ⟨⟨r, ⟨rs, xr⟩⟩, ?_⟩
exact ⟨H, A⟩
· intro q hq
obtain ⟨r, ⟨xr, rq⟩, rs⟩ : ∃ r, r ∈ Ioo (f x) q ∩ s :=
dense_iff_inter_open.1 s_dense (Ioo (f x) q) isOpen_Ioo (nonempty_Ioo.2 hq)
refine ⟨⟨r, rs⟩, ?_⟩
have A : x ∈ u' r := mem_biInter fun i _ => (huv r i).2.2.1 xr
simp only [A, rq, piecewise_eq_of_mem]
exact ⟨f', f'_meas, ff'⟩
