`BookProof.ChapterAttentionOutput.norm_observableExpectation_sub_le` (p q : Fin m → ℝ) {v : Fin m → E} {C : ℝ} (hv : ∀ j, ‖v j‖ ≤ C) : ‖observableExpectation p v

Initializing...

`BookProof.ChapterAttentionOutput.norm_observableExpectation_sub_le` (p q : Fin m → ℝ) {v : Fin m → E} {C : ℝ} (hv : ∀ j, ‖v j‖ ≤ C) : ‖observableExpectation p v - observableExpect · Prove2Me