feat(measure_theory/constructions/borel_space): a set with μ (∂ s) = 0 is null measurable (#13322)

Author: urkud

src/measure_theory/constructions/borel_space.lean

@@ -378,15 +378,26 @@ end
 
 variables {α' : Type*} [topological_space α'] [measurable_space α']
 
-lemma measure_interior_of_null_bdry {μ : measure α'} {s : set α'}
-  (h_nullbdry : μ (frontier s) = 0) : μ (interior s) = μ s :=
-measure_eq_measure_smaller_of_between_null_diff
-  interior_subset subset_closure h_nullbdry
-
-lemma measure_closure_of_null_bdry {μ : measure α'} {s : set α'}
-  (h_nullbdry : μ (frontier s) = 0) : μ (closure s) = μ s :=
-(measure_eq_measure_larger_of_between_null_diff
-  interior_subset subset_closure h_nullbdry).symm
+lemma interior_ae_eq_of_null_frontier {μ : measure α'} {s : set α'}
+  (h : μ (frontier s) = 0) : interior s =ᵐ[μ] s :=
+interior_subset.eventually_le.antisymm $
+  subset_closure.eventually_le.trans (ae_le_set.2 h)
+
+lemma measure_interior_of_null_frontier {μ : measure α'} {s : set α'}
+  (h : μ (frontier s) = 0) : μ (interior s) = μ s :=
+measure_congr (interior_ae_eq_of_null_frontier h)
+
+lemma null_measurable_set_of_null_frontier {s : set α} {μ : measure α}
+  (h : μ (frontier s) = 0) : null_measurable_set s μ :=
+⟨interior s, is_open_interior.measurable_set, (interior_ae_eq_of_null_frontier h).symm⟩
+
+lemma closure_ae_eq_of_null_frontier {μ : measure α'} {s : set α'}
+  (h : μ (frontier s) = 0) : closure s =ᵐ[μ] s :=
+((ae_le_set.2 h).trans interior_subset.eventually_le).antisymm $ subset_closure.eventually_le
+
+lemma measure_closure_of_null_frontier {μ : measure α'} {s : set α'}
+  (h : μ (frontier s) = 0) : μ (closure s) = μ s :=
+measure_congr (closure_ae_eq_of_null_frontier h)
 
 section preorder
 variables [preorder α] [order_closed_topology α] {a b x : α}