OAI/NumberTheory/TwoPoint/Bounds/LiouvilleQuadraticIdentity.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Testing the actual weighted matrix leaves twice L times the ambient retained directed-edge correlation.

  1. theorem OAI.TwoPointCorrelations.maskedLiouville_quadratic line 14