English
The congruence for the negation instance holds; the coercions align with equality under negation.
Русский
Сохранение конгруэнтности для инстанса отрицания; коэрцирование согласуется с равенством при отрицании.
LaTeX
$$$Eq MeasureTheory.VectorMeasure.instNeg MeasureTheory.VectorMeasure.instNeg$$$
Lean4
/-- A finite measure coerced into a real function is a signed measure. -/
@[simps]
def toSignedMeasure (μ : Measure α) [hμ : IsFiniteMeasure μ] : SignedMeasure α
where
measureOf' := fun s : Set α => if MeasurableSet s then μ.real s else 0
empty' := by simp
not_measurable' _ hi := if_neg hi
m_iUnion' f hf₁
hf₂ := by
simp only [*, MeasurableSet.iUnion hf₁, if_true, measure_iUnion hf₂ hf₁, measureReal_def]
rw [ENNReal.tsum_toReal_eq]
exacts [(summable_measure_toReal hf₁ hf₂).hasSum, fun _ ↦ measure_ne_top _ _]
