simp [rand_simp,flip.measure]
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
⊢ ∫' x, f x ∂(flip θ).ℙ = θ • f true + (1 - θ) • f false
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
⊢ ∫' x,
      f
        x ∂(ENNReal.ofReal (Scalar.toReal R θ) • Measure.dirac true +
        ENNReal.ofReal (Scalar.toReal R (1 - θ)) • Measure.dirac false) =
    θ • f true + (1 - θ) • f false