`BookProof.SqueezedGaussStates.coordComboSum_opCoef_le` (α γ v : ℝ) (M : ℕ) (hv : 4 * v ^ 2 < 1) : coordComboSum (opCoef α γ v M) 1 M ≤ ((kappa α γ v) ^ 2 / (1

Initializing...

`BookProof.SqueezedGaussStates.coordComboSum_opCoef_le` (α γ v : ℝ) (M : ℕ) (hv : 4 * v ^ 2 < 1) : coordComboSum (opCoef α γ v M) 1 M ≤ ((kappa α γ v) ^ 2 / (1 - 4 * v ^ 2) + α ^ 2 · Prove2Me