English
Scaling a signed measure by an arbitrary real scalar commutes with taking its Jordan decomposition, with the appropriate sign adjustment.
Русский
Умножение подписанной меры на произвольный действительный скаляр сохраняет разложение Йордана с соответствующим знаком.
LaTeX
$$$$ (r \cdot s).toJordanDecomposition = r \cdot (s.toJordanDecomposition) $$$$
Lean4
theorem toJordanDecomposition_smul_real (s : SignedMeasure α) (r : ℝ) :
(r • s).toJordanDecomposition = r • s.toJordanDecomposition :=
by
by_cases hr : 0 ≤ r
· exact toJordanDecomposition_smul_real_nonneg s r hr
· ext1
· rw [real_smul_posPart_neg _ _ (not_le.1 hr), show r • s = -(-r • s) by rw [neg_smul, neg_neg],
toJordanDecomposition_neg, neg_posPart, toJordanDecomposition_smul_real_nonneg, ← smul_negPart,
real_smul_nonneg]
all_goals exact Left.nonneg_neg_iff.2 (le_of_lt (not_le.1 hr))
· rw [real_smul_negPart_neg _ _ (not_le.1 hr), show r • s = -(-r • s) by rw [neg_smul, neg_neg],
toJordanDecomposition_neg, neg_negPart, toJordanDecomposition_smul_real_nonneg, ← smul_posPart,
real_smul_nonneg]
all_goals exact Left.nonneg_neg_iff.2 (le_of_lt (not_le.1 hr))
