`BookProof.ScalaronDensitized.physConfOp_quadForm_ge` (halpha : 0 < alpha) (f : physConfCore M alpha) : -(M ^ 4 / (16 * alpha)) * ‖(f : Lp ℂ 2 physMeasure)‖ ^ 2 ≤ quadForm ((physCo

Initializing...

`BookProof.ScalaronDensitized.physConfOp_quadForm_ge` (halpha : 0 < alpha) (f : physConfCore M alpha) : -(M ^ 4 / (16 * alpha)) * ‖(f : Lp ℂ 2 physMeasure)‖ ^ 2 ≤ quadForm ((physCo · Prove2Me