simp only [𝔼,flip.integral]
R : Type
inst✝⁴ : RealScalar R
inst✝³ : MeasureSpace R
X : Type u_1
inst✝² : AddCommGroup X
inst✝¹ : Module R X
inst✝ : Module ℝ X
θ : R
f : Bool → X
⊢ (flip θ).𝔼 f = θ • f true + (1 - θ) • f false
no goals