OAI/NumberTheory/DirichletL/Moments/SecondChildRadialWidth.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SevenEighths.CenteredMomentSecondChildRadialWidth.physicalBlock_live_dyadic_witness line 20
  2. theorem OAI.SevenEighths.CenteredMomentSecondChildRadialWidth.dyadic_log_budget line 46
  3. theorem OAI.SevenEighths.CenteredMomentSecondChildRadialWidth.radial_support_bound line 66
  4. theorem OAI.SevenEighths.CenteredMomentSecondChildRadialWidth.radial_radius_log_budget line 72
  5. theorem OAI.SevenEighths.CenteredMomentSecondChildRadialWidth.radial_point_log_budget line 87
  6. theorem OAI.SevenEighths.CenteredMomentSecondChildRadialWidth.declared_radial_log_budget line 99
  7. theorem OAI.SevenEighths.CenteredMomentSecondChildRadialWidth.whole_radial_norm_budget line 111
  8. theorem OAI.SevenEighths.CenteredMomentSecondChildRadialWidth.fixed_radial_cost_eventually line 127
  9. theorem OAI.SevenEighths.CenteredMomentSecondChildRadialWidth.eventually_whole_radial_width line 137
  10. theorem OAI.SevenEighths.CenteredMomentSecondChildRadialWidth.physical_declared_radial_width_drop line 166