OAI/NumberTheory/DirichletL/MeanSquare/UniformPolynomialHeight.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CompletedHeight.uniform_polynomial_reflected_branch_series line 86
  2. theorem OAI.CompletedHeight.uniform_polynomial_reflected_fiber_fixed_scale line 127
  3. theorem OAI.CompletedHeight.uniform_polynomial_branch_energy line 181
  4. theorem OAI.CompletedHeight.uniform_polynomial_fiber_energy line 201
  5. theorem OAI.CompletedHeight.uniform_polynomial_energy_of_exact_models line 251
  6. theorem OAI.CompletedHeight.uniform_polynomial_mean_square_of_exact_reflection line 309
  7. theorem OAI.CompletedHeight.uniform_polynomial_short_completed_average line 381
  8. theorem OAI.CompletedHeight.completed_mean_square_uniform_height line 458
  9. theorem OAI.CompletedHeight.short_completed_average_uniform_height line 476
  10. theorem OAI.CompletedHeight.completed_mean_square_uniform_twist line 497
  11. theorem OAI.CompletedHeight.short_completed_average_uniform_twist line 516
  12. def OAI.CompletedUnitRows.rowUnit line 554
  13. lemma OAI.CompletedUnitRows.rowUnit_spec line 557
  14. def OAI.CompletedUnitRows.unitIdealPoint line 566
  15. lemma OAI.CompletedUnitRows.unitIdealPoint_inj line 568
  16. theorem OAI.CompletedUnitRows.sum_nonzero_element_le_units line 574
  17. lemma OAI.CompletedUnitRows.image_span_nonzero_norm line 599
  18. lemma OAI.CompletedUnitRows.unit_card line 606