OAI/NumberTheory/DirichletL/Moments/SecondExceptionalFamily.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SevenEighths.CenteredMomentSecondExceptionalFamily.span_thirty_six_norm line 24
  2. theorem OAI.SevenEighths.CenteredMomentSecondExceptionalFamily.reflected_modulus_bound line 29
  3. theorem OAI.SevenEighths.CenteredMomentSecondExceptionalFamily.common_subproduct_dvd_left line 35
  4. theorem OAI.SevenEighths.CenteredMomentSecondExceptionalFamily.common_subproduct_dvd_right line 49
  5. theorem OAI.SevenEighths.CenteredMomentSecondExceptionalFamily.selected_nonunit_product line 63
  6. theorem OAI.SevenEighths.CenteredMomentSecondExceptionalFamily.selected_nonunit_dvd line 74
  7. theorem OAI.SevenEighths.CenteredMomentSecondExceptionalFamily.selected_nonunit_norm line 82
  8. structure OAI.SevenEighths.CenteredMomentSecondExceptionalFamily.Family line 93
  9. theorem OAI.SevenEighths.CenteredMomentSecondExceptionalFamily.exists_exceptional_family line 113
  10. theorem OAI.SevenEighths.CenteredMomentSecondExceptionalFamily.Family.nonexceptional_iff line 138
  11. theorem OAI.SevenEighths.CenteredMomentSecondExceptionalFamily.Family.inducing_iff line 144
  12. theorem OAI.SevenEighths.CenteredMomentSecondExceptionalFamily.Family.paired_inducing_iff line 152
  13. theorem OAI.SevenEighths.CenteredMomentSecondExceptionalFamily.Family.both_inducing line 162
  14. theorem OAI.SevenEighths.CenteredMomentSecondExceptionalFamily.Family.reflected_height_eq line 174
  15. theorem OAI.SevenEighths.CenteredMomentSecondExceptionalFamily.Family.live_both_inducing line 187
  16. theorem OAI.SevenEighths.CenteredMomentSecondExceptionalFamily.Family.physical_conductor_bounds line 198
  17. def OAI.SevenEighths.CenteredMomentSecondExceptionalFamily.expandedConductor line 215
  18. def OAI.SevenEighths.CenteredMomentSecondExceptionalFamily.expandedFactor line 219
  19. theorem OAI.SevenEighths.CenteredMomentSecondExceptionalFamily.expanded_conductor_bounds line 223
  20. theorem OAI.SevenEighths.CenteredMomentSecondExceptionalFamily.eventually_expanded_conductor_caps line 257
  21. theorem OAI.SevenEighths.CenteredMomentSecondExceptionalFamily.live_norm_le_four_radius line 293
  22. theorem OAI.SevenEighths.CenteredMomentSecondExceptionalFamily.eventually_live_expanded_conductor_caps line 305