`BookProof.ScalaronDensitized.densConfOp_quadForm_ge` (halpha : 0 < alpha) (f : densConfCore M alpha) : -(M ^ 4 / (16 * alpha)) * ‖(f : Lp ℂ 2 qgSrcMeasure)‖ ^ 2 ≤ quadForm ((densC

Initializing...

`BookProof.ScalaronDensitized.densConfOp_quadForm_ge` (halpha : 0 < alpha) (f : densConfCore M alpha) : -(M ^ 4 / (16 * alpha)) * ‖(f : Lp ℂ 2 qgSrcMeasure)‖ ^ 2 ≤ quadForm ((densC · Prove2Me