OAI/NumberTheory/DirichletL/Dictionary/InverseRawCompact.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SevenEighths.DetectorDictionaryInverseRawCompact.inverse_polynomial_all_ideals line 15
2. theorem OAI.SevenEighths.DetectorDictionaryInverseRawCompact.inverse_polynomial_bound line 29
3. lemma OAI.SevenEighths.DetectorDictionaryInverseRawCompact.childLogTest_norm line 56
4. theorem OAI.SevenEighths.DetectorDictionaryInverseRawCompact.inverse_reference_bound line 60
5. theorem OAI.SevenEighths.DetectorDictionaryInverseRawCompact.nonzero_element_rows_card line 76
6. theorem OAI.SevenEighths.DetectorDictionaryInverseRawCompact.reference_energy_linear line 87
7. theorem OAI.SevenEighths.DetectorDictionaryInverseRawCompact.subunit_rows_reference_energy line 107
8. lemma OAI.SevenEighths.DetectorDictionaryInverseRawCompact.scale_le_rows line 119
9. theorem OAI.SevenEighths.DetectorDictionaryInverseRawCompact.small_rows_reference_energy line 129
10. lemma OAI.SevenEighths.DetectorDictionaryInverseRawCompact.raw_majorant_ge_linear line 144
11. theorem OAI.SevenEighths.DetectorDictionaryInverseRawCompact.rawMoment_of_large_rows_ge_one line 157
12. theorem OAI.SevenEighths.DetectorDictionaryInverseRawCompact.rawMoment_of_large_rows line 186