OAI/NumberTheory/DirichletL/MeanSquare/PolynomialHeight.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CompletedHeight.polynomial_reflected_branch_series line 85
  2. theorem OAI.CompletedHeight.polynomial_reflected_fiber_fixed_scale line 123
  3. theorem OAI.CompletedHeight.polynomial_branch_energy line 174
  4. theorem OAI.CompletedHeight.polynomial_fiber_energy line 191
  5. theorem OAI.CompletedHeight.polynomial_energy_of_exact_models line 238
  6. theorem OAI.CompletedHeight.polynomial_mean_square_of_exact_reflection line 293
  7. theorem OAI.CompletedHeight.polynomial_short_completed_average line 362
  8. theorem OAI.CompletedHeight.completed_mean_square_norm_height line 439
  9. theorem OAI.CompletedHeight.short_completed_average_norm_height line 454
  10. lemma OAI.CompletedHeight.logPhase_triple line 482
  11. lemma OAI.CompletedHeight.columnWeight_normHeight line 486
  12. lemma OAI.CompletedHeight.cubeWeight_normHeight line 497
  13. lemma OAI.CompletedHeight.summand_normHeight line 512
  14. theorem OAI.CompletedHeight.completedT_normHeight line 537
  15. theorem OAI.CompletedHeight.completedT_normHeight_norm line 542
  16. theorem OAI.CompletedHeight.shortCompletedSum_normHeight line 547
  17. theorem OAI.CompletedHeight.shortCompletedSum_normHeight_norm line 566
  18. theorem OAI.CompletedHeight.completed_mean_square_twist line 578
  19. theorem OAI.CompletedHeight.short_completed_average_twist line 595