English
If Disjoint μ ν then μ ⟂ ν.
Русский
Если μ и ν парно несовместны, то μ и ν взаимно-сингуларны.
LaTeX
$$$$ \\text{Disjoint}(\\mu, \\nu) \\;\Rightarrow\\; \\mu \\perp_{m} \\nu. $$$$
Lean4
theorem mutuallySingular_of_disjoint (h : Disjoint μ ν) : μ ⟂ₘ ν :=
by
have h' (n : ℕ) : ∃ s, μ s = 0 ∧ ν sᶜ ≤ (1 / 2) ^ n :=
by
convert exists_null_set_measure_lt_of_disjoint h (ε := (1 / 2) ^ (n + 1)) <| pow_pos (by simp) (n + 1)
push_cast
rw [pow_succ, ← mul_assoc, mul_comm, ← mul_assoc]
norm_cast
rw [div_mul_cancel₀, one_mul]
· push_cast
simp
· simp
choose s hs₂ hs₃ using h'
refine Measure.MutuallySingular.mk (t := (⋃ n, s n)ᶜ) (measure_iUnion_null hs₂) ?_ ?_
· rw [compl_iUnion]
refine eq_zero_of_le_mul_pow (ε := 1) (by simp : (1 / 2 : ℝ≥0∞) < 1) <| fun n ↦ ?_
rw [ENNReal.coe_one, one_mul]
exact (measure_mono <| iInter_subset_of_subset n fun _ ht ↦ ht).trans (hs₃ n)
· rw [union_compl_self]
