`BookProof.TruncationGapLift.gap_of_le_ritzInf_and_tail` (b : HilbertBasis ℕ ℂ F) (H : finiteModeDomain b →ₗ[ℂ] F) (hsym : SymmetricOn _ H) (hpos : ∀ x : finiteModeDomain b, 0 ≤ qu

Initializing...

`BookProof.TruncationGapLift.gap_of_le_ritzInf_and_tail` (b : HilbertBasis ℕ ℂ F) (H : finiteModeDomain b →ₗ[ℂ] F) (hsym : SymmetricOn _ H) (hpos : ∀ x : finiteModeDomain b, 0 ≤ qu · Prove2Me