English
If s = t + μ.withDensityᵥ f with hf measurable and htμ mutually singular, then the Jordan decomposition of s equals the constructed Jordan decomposition from t and μ.withDensityᵥ f.
Русский
Если s = t + μ.withDensityᵥ f с измеримой f и htμ взаимно сингулярно, то джорданово разложение s совпадает с сконструированным из t и μ.withDensityᵥ f.
LaTeX
$$$s = t + μ.withDensityᵥ f \Rightarrow s.toJordanDecomposition = @JordanDecomposition.mk( \n t.toJordanDecomposition.posPart + μ.withDensity f,\n t.toJordanDecomposition.negPart + μ.withDensity(-f),\n ..., mutuallySingular = ...) $$$
Lean4
theorem toJordanDecomposition_eq_of_eq_add_withDensity {f : α → ℝ} (hf : Measurable f) (hfi : Integrable f μ)
(htμ : t ⟂ᵥ μ.toENNRealVectorMeasure) (hadd : s = t + μ.withDensityᵥ f) :
s.toJordanDecomposition =
@JordanDecomposition.mk α _ (t.toJordanDecomposition.posPart + μ.withDensity fun x => ENNReal.ofReal (f x))
(t.toJordanDecomposition.negPart + μ.withDensity fun x => ENNReal.ofReal (-f x))
(by haveI := isFiniteMeasure_withDensity_ofReal hfi.2; infer_instance)
(by haveI := isFiniteMeasure_withDensity_ofReal hfi.neg.2; infer_instance)
(jordanDecomposition_add_withDensity_mutuallySingular hf htμ) :=
by
haveI := isFiniteMeasure_withDensity_ofReal hfi.2
haveI := isFiniteMeasure_withDensity_ofReal hfi.neg.2
refine toJordanDecomposition_eq ?_
simp_rw [JordanDecomposition.toSignedMeasure, hadd]
ext i hi
rw [VectorMeasure.sub_apply, toSignedMeasure_apply_measurable hi, toSignedMeasure_apply_measurable hi,
measureReal_add_apply, measureReal_add_apply, add_sub_add_comm, ← toSignedMeasure_apply_measurable hi, ←
toSignedMeasure_apply_measurable hi, ← VectorMeasure.sub_apply, ← JordanDecomposition.toSignedMeasure,
toSignedMeasure_toJordanDecomposition, VectorMeasure.add_apply, ← toSignedMeasure_apply_measurable hi, ←
toSignedMeasure_apply_measurable hi, withDensityᵥ_eq_withDensity_pos_part_sub_withDensity_neg_part hfi,
VectorMeasure.sub_apply]
