`BookProof.ChapterObservableOperator.observableOp_expectation_real` (k : Fin m → EuclideanSpace ℂ (Fin n)) (v : Fin m → ℝ) (q : EuclideanSpace ℂ (Fin n)) : (expectation (observable

Initializing...

`BookProof.ChapterObservableOperator.observableOp_expectation_real` (k : Fin m → EuclideanSpace ℂ (Fin n)) (v : Fin m → ℝ) (q : EuclideanSpace ℂ (Fin n)) : (expectation (observable · Prove2Me