OAI/NumberTheory/DirichletL/MeanSquare/RetainedDensity.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.InitialMeanSquare.initialLogLabel_ge_one line 84
  2. lemma OAI.InitialMeanSquare.initialLogColumn_pos line 89
  3. lemma OAI.InitialMeanSquare.initialLogColumn_le line 93
  4. lemma OAI.InitialMeanSquare.initialLogLabel_cap line 98
  5. theorem OAI.InitialMeanSquare.initial_radial_invariant line 116
  6. theorem OAI.InitialMeanSquare.initial_large_threshold line 148
  7. theorem OAI.InitialMeanSquare.initial_large_bin_geometry line 181
  8. theorem OAI.InitialMeanSquare.initial_density_elementary_squared_mass line 247
  9. theorem OAI.InitialMeanSquare.HasInitialCanonicalDensity.retained_density line 287
  10. theorem OAI.InitialMeanSquare.initial_log_harmonic_small_power line 399
  11. theorem OAI.InitialMeanSquare.initial_row_log_budget line 428
  12. theorem OAI.InitialMeanSquare.HasInitialCanonicalDensity.retained_source line 467
  13. theorem OAI.InitialMeanSquare.HasInitialCanonicalDensity.nonzero_source_bound line 617