Theorem: SciLean.Rand.flip.E (SciLean/Core/Rand/Distributions/Flip.lean)

State before:
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
Tactic:
simp only [𝔼,flip.integral]
State after:
no goals