OAI/NumberTheory/DirichletL/MeanSquare/DiagonalDensity.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.InitialMeanSquare.initial_diagonal_fixed_profile line 87
2. theorem OAI.InitialMeanSquare.initial_normalized_diagonal line 111
3. def OAI.InitialMeanSquare.initialFrequencyCutoff line 138
4. theorem OAI.InitialMeanSquare.initialFrequencyCutoff_zero line 141
5. theorem OAI.InitialMeanSquare.initialFrequencyCutoff_valid line 144
6. theorem OAI.InitialMeanSquare.initial_tail_polynomial line 180
7. def OAI.InitialMeanSquare.initialTailHeight line 212
8. theorem OAI.InitialMeanSquare.initialTailHeight_pos line 215
9. theorem OAI.InitialMeanSquare.initial_tail_fixed_profile line 218
10. def OAI.InitialMeanSquare.initialErrorWindow line 254
11. def OAI.InitialMeanSquare.initialErrorCutoff line 256
12. theorem OAI.InitialMeanSquare.initialErrorCutoff_zero line 260
13. def OAI.InitialMeanSquare.initialErrorFrequencyBound line 263
14. theorem OAI.InitialMeanSquare.initialErrorCutoff_norm_bound line 267
15. theorem OAI.InitialMeanSquare.initial_normalized_errors line 288
16. theorem OAI.InitialMeanSquare.outside_mean_square_source_with_errors line 323
17. theorem OAI.InitialMeanSquare.initial_nonzero_source_norm_le_squarefree_bins line 384
18. def OAI.InitialMeanSquare.initialSquarefreeBinCost line 426
19. theorem OAI.InitialMeanSquare.initial_nonzero_source_squarefree_transfer line 441
20. theorem OAI.InitialMeanSquare.initialSquarefreeBinCost_of_canonical_bound line 502
21. theorem OAI.InitialMeanSquare.positive_nested_density_transfer line 571
22. theorem OAI.InitialMeanSquare.initial_source_density_transfer line 615