English
If μ and ν are disjoint measures, then for any ε > 0 there exists a set s with μ(s) = 0 and ν(s^c) ≤ 2ε.
Русский
Пусть μ и ν — попарно непересекающиеся меры. Тогда для любого ε > 0 существует множество s такое, что μ(s) = 0 и ν(s^c) ≤ 2ε.
LaTeX
$$$$ \\exists s\\; (\\mu s = 0) \\land (\\nu s^{c} \\le 2 \\varepsilon). $$$$
Lean4
theorem exists_null_set_measure_lt_of_disjoint (h : Disjoint μ ν) {ε : ℝ≥0} (hε : 0 < ε) :
∃ s, μ s = 0 ∧ ν sᶜ ≤ 2 * ε :=
by
have h₁ : (μ ⊓ ν) univ = 0 := le_bot_iff.1 (h (inf_le_left (b := ν)) inf_le_right) ▸ rfl
simp_rw [Measure.inf_apply MeasurableSet.univ, inter_univ] at h₁
have h₂ : ∀ n : ℕ, ∃ t, μ t + ν tᶜ < ε * (1 / 2) ^ n :=
by
intro n
obtain ⟨m, ⟨t, ht₁, rfl⟩, hm₂⟩ : ∃ x ∈ {m | ∃ t, m = μ t + ν tᶜ}, x < ε * (1 / 2 : ℝ≥0∞) ^ n :=
by
refine exists_lt_of_csInf_lt ⟨ν univ, ∅, by simp⟩ <| h₁ ▸ ENNReal.mul_pos ?_ (by simp)
norm_cast
exact hε.ne.symm
exact ⟨t, hm₂⟩
choose t ht₂ using h₂
refine ⟨⋂ n, t n, ?_, ?_⟩
·
refine
eq_zero_of_le_mul_pow (by simp) fun n ↦
((measure_mono <| iInter_subset_of_subset n fun _ ht ↦ ht).trans (le_add_right le_rfl)).trans (ht₂ n).le
· rw [compl_iInter, (by simp [ENNReal.tsum_mul_left, mul_comm] : 2 * (ε : ℝ≥0∞) = ∑' (n : ℕ), ε * (1 / 2 : ℝ≥0∞) ^ n)]
refine (measure_iUnion_le _).trans ?_
exact ENNReal.summable.tsum_le_tsum (fun n ↦ (le_add_left le_rfl).trans (ht₂ n).le) ENNReal.summable
