English
If μ is finite and s, t are null-measurable, then |μ.real s − μ.real t| ≤ μ.real (s Δ t) provided μ s, μ t ≠ ∞.
Русский
Пусть μ конечна и s, t нуль-измеримы; тогда |μ.real(s) − μ.real(t)| ≤ μ.real(s Δ t), при условии μ(s) ≠ ∞ и μ(t) ≠ ∞.
LaTeX
$$$(\text{NullMeasurableSet}(s, \mu)) \land (\text{NullMeasurableSet}(t, \mu)) \land (\mu(s) \neq \infty) \land (\mu(t) \neq \infty) \Rightarrow |\mu^{\mathbb{R}}(s) - \mu^{\mathbb{R}}(t)| \le \mu^{\mathbb{R}}(s \Delta t)$$
Lean4
theorem abs_measureReal_sub_le_measureReal_symmDiff' (hs : NullMeasurableSet s μ) (ht : NullMeasurableSet t μ)
(hs' : μ s ≠ ∞) (ht' : μ t ≠ ∞) : |μ.real s - μ.real t| ≤ μ.real (s ∆ t) :=
by
simp only [Measure.real]
have hst : μ (s \ t) ≠ ∞ := (measure_lt_top_of_subset diff_subset hs').ne
have hts : μ (t \ s) ≠ ∞ := (measure_lt_top_of_subset diff_subset ht').ne
suffices (μ s).toReal - (μ t).toReal = (μ (s \ t)).toReal - (μ (t \ s)).toReal
by
rw [this, measure_symmDiff_eq hs ht, ENNReal.toReal_add hst hts]
convert abs_sub (μ (s \ t)).toReal (μ (t \ s)).toReal <;> simp
rw [measure_diff' s ht ht', measure_diff' t hs hs',
ENNReal.toReal_sub_of_le measure_le_measure_union_right (measure_union_ne_top hs' ht'),
ENNReal.toReal_sub_of_le measure_le_measure_union_right (measure_union_ne_top ht' hs'), union_comm t s]
abel
