Commit 2024-02-26 07:32 e903c3fc

feat: lemmas about kernel.withDensity (#10799) Add a few simp lemmas about withDensity of constant functions 1 and 0, and the 3 more interesting lemmas

• withDensity_add_right: withDensity κ (f + g) = withDensity κ f + withDensity κ g
• withDensity_sub_add_cancel: withDensity κ (fun a x ↦ f a x - g a x) + withDensity κ g = withDensity κ f
• withDensity_mul: withDensity κ (fun a x ↦ f a x * g a x) = withDensity (withDensity κ fun a x ↦ f a x) g