OAI/NumberTheory/Ostmann/QuadraticCenter/ActualWitnessMomentsGrid.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.QuadraticCenter.witnessGridArray line 14
2. def OAI.Ostmann.QuadraticCenter.witnessLargeFamily line 18
3. def OAI.Ostmann.QuadraticCenter.witnessNontrivialFamily line 22
4. theorem OAI.Ostmann.QuadraticCenter.witnessLargeFamily_subset line 26
5. theorem OAI.Ostmann.QuadraticCenter.witnessNontrivialFamily_subset line 31
6. theorem OAI.Ostmann.QuadraticCenter.witnessLargeSupport_eq line 36
7. theorem OAI.Ostmann.QuadraticCenter.witnessSubfamily_polynomial line 58
8. theorem OAI.Ostmann.QuadraticCenter.exists_near_witnessGridArray line 68
9. theorem OAI.Ostmann.QuadraticCenter.eventually_witnessLargeFamily_energy line 90