English
If m is a metric outer measure, then every Borel set t is Carathéodory-measurable: for any s, μ(s ∩ t) + μ(s \\ t) = μ(s).
Русский
Если μ — метрическая внешняя мера, то любоe борелевское множество t является Карпатейодоровым измеримым: для любого s верно μ(s ∩ t) + μ(s \\ t) = μ(s).
LaTeX
$$μ.isCaratheodory_iff_le.2 ∀ s, μ(s ∩ t) + μ(s \\ t) = μ s for t борелевское$$
Lean4
/-- Caratheodory theorem. If `m` is a metric outer measure, then every Borel measurable set `t` is
Caratheodory measurable: for any (not necessarily measurable) set `s` we have
`μ (s ∩ t) + μ (s \ t) = μ s`. -/
theorem borel_le_caratheodory (hm : IsMetric μ) : borel X ≤ μ.caratheodory :=
by
rw [borel_eq_generateFrom_isClosed]
refine MeasurableSpace.generateFrom_le fun t ht => μ.isCaratheodory_iff_le.2 fun s => ?_
set S : ℕ → Set X := fun n => {x ∈ s | (↑n)⁻¹ ≤ infEdist x t}
have Ssep (n) : Metric.AreSeparated (S n) t :=
⟨n⁻¹, ENNReal.inv_ne_zero.2 (ENNReal.natCast_ne_top _), fun x hx y hy ↦ hx.2.trans <| infEdist_le_edist_of_mem hy⟩
have Ssep' : ∀ n, Metric.AreSeparated (S n) (s ∩ t) := fun n => (Ssep n).mono Subset.rfl inter_subset_right
have S_sub : ∀ n, S n ⊆ s \ t := fun n => subset_inter inter_subset_left (Ssep n).subset_compl_right
have hSs : ∀ n, μ (s ∩ t) + μ (S n) ≤ μ s := fun n =>
calc
μ (s ∩ t) + μ (S n) = μ (s ∩ t ∪ S n) := Eq.symm <| hm _ _ <| (Ssep' n).symm
_ ≤ μ (s ∩ t ∪ s \ t) := (μ.mono <| union_subset_union_right _ <| S_sub n)
_ = μ s := by rw [inter_union_diff]
have iUnion_S : ⋃ n, S n = s \ t :=
by
refine Subset.antisymm (iUnion_subset S_sub) ?_
rintro x ⟨hxs, hxt⟩
rw [mem_iff_infEdist_zero_of_closed ht] at hxt
rcases ENNReal.exists_inv_nat_lt hxt with ⟨n, hn⟩
exact
mem_iUnion.2
⟨n, hxs, hn.le⟩
/- Now we have `∀ n, μ (s ∩ t) + μ (S n) ≤ μ s` and we need to prove
`μ (s ∩ t) + μ (⋃ n, S n) ≤ μ s`. We can't pass to the limit because
`μ` is only an outer measure. -/
by_cases htop : μ (s \ t) = ∞
· rw [htop, add_top, ← htop]
exact μ.mono diff_subset
suffices μ (⋃ n, S n) ≤ ⨆ n, μ (S n) by
calc
μ (s ∩ t) + μ (s \ t) = μ (s ∩ t) + μ (⋃ n, S n) := by rw [iUnion_S]
_ ≤ μ (s ∩ t) + ⨆ n, μ (S n) := by gcongr
_ = ⨆ n, μ (s ∩ t) + μ (S n) := ENNReal.add_iSup ..
_ ≤ μ s := iSup_le hSs
have : ∀ n, S n ⊆ S (n + 1) := fun n x hx => ⟨hx.1, le_trans (ENNReal.inv_le_inv.2 <| Nat.cast_le.2 n.le_succ) hx.2⟩
refine (μ.iUnion_nat_of_monotone_of_tsum_ne_top this ?_).le; clear this
rw [← tsum_even_add_odd ENNReal.summable ENNReal.summable, ENNReal.add_ne_top]
suffices ∀ a, (∑' k : ℕ, μ (S (2 * k + 1 + a) \ S (2 * k + a))) ≠ ∞ from
⟨by simpa using this 0, by simpa using this 1⟩
refine fun r => ne_top_of_le_ne_top htop ?_
rw [← iUnion_S, ENNReal.tsum_eq_iSup_nat, iSup_le_iff]
intro n
rw [← hm.finset_iUnion_of_pairwise_separated]
· exact μ.mono (iUnion_subset fun i => iUnion_subset fun _ x hx => mem_iUnion.2 ⟨_, hx.1⟩)
suffices ∀ i j, i < j → Metric.AreSeparated (S (2 * i + 1 + r)) (s \ S (2 * j + r)) from fun i _ j _ hij =>
hij.lt_or_gt.elim (fun h => (this i j h).mono inter_subset_left fun x hx => by exact ⟨hx.1.1, hx.2⟩) fun h =>
(this j i h).symm.mono (fun x hx => by exact ⟨hx.1.1, hx.2⟩) inter_subset_left
intro i j hj
have A : ((↑(2 * j + r))⁻¹ : ℝ≥0∞) < (↑(2 * i + 1 + r))⁻¹ := by rw [ENNReal.inv_lt_inv, Nat.cast_lt]; omega
refine ⟨(↑(2 * i + 1 + r))⁻¹ - (↑(2 * j + r))⁻¹, by simpa [tsub_eq_zero_iff_le] using A, fun x hx y hy => ?_⟩
have : infEdist y t < (↑(2 * j + r))⁻¹ := not_le.1 fun hle => hy.2 ⟨hy.1, hle⟩
rcases infEdist_lt_iff.mp this with ⟨z, hzt, hyz⟩
have hxz : (↑(2 * i + 1 + r))⁻¹ ≤ edist x z := le_infEdist.1 hx.2 _ hzt
apply ENNReal.le_of_add_le_add_right hyz.ne_top
refine le_trans ?_ (edist_triangle _ _ _)
refine (add_le_add le_rfl hyz.le).trans (Eq.trans_le ?_ hxz)
rw [tsub_add_cancel_of_le A.le]
