Commit 2023-11-02 08:18 9fa322ac

feat: properties of rnDeriv (#7675) Various results about rnDeriv, notably rnDeriv_add, rnDeriv_smul_left and rnDeriv_smul_right. These results describe the Radon-Nikodym derivatives of sums and scaling of measures. These lemmas were already there for signed measures, but not for Measure. The proofs for signed measures use that addition is cancelative (μ + ν₁ = μ + ν₂ ↔ ν₁ = ν₂). This is not true in general for measures, but is true when μ is mutually singular with the two other measures or when μ is sigma-finite, which is enough for these proofs.