`BookProof.FockNumberPreservingGap.number_quadForm_ge` {u : FockAlg} (h0 : u 0 = 0) : ‖toLp u‖ ^ 2 ≤ (inner ℂ (toLp u) (toLp (dGamma numberCol u)) : ℂ).re

Initializing...

`BookProof.FockNumberPreservingGap.number_quadForm_ge` {u : FockAlg} (h0 : u 0 = 0) : ‖toLp u‖ ^ 2 ≤ (inner ℂ (toLp u) (toLp (dGamma numberCol u)) : ℂ).re · Prove2Me