`BookProof.ScalaronFock.qgManyPotential_apply` (M alpha : ℝ) (n : ℕ) (x : qgSector n) : qgManyPotential M alpha n x = ∑ j : Fin n, (confV M alpha (x (j, 0)) + starobinskyV M alpha

Initializing...

`BookProof.ScalaronFock.qgManyPotential_apply` (M alpha : ℝ) (n : ℕ) (x : qgSector n) : qgManyPotential M alpha n x = ∑ j : Fin n, (confV M alpha (x (j, 0)) + starobinskyV M alpha · Prove2Me