OAI/NumberTheory/DirichletL/Inversion/InitialQuotientGeometry.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.InverseInitialQuotientGeometry.sourceWeight line 17
  2. def OAI.SevenEighths.InverseInitialQuotientGeometry.retained line 22
  3. def OAI.SevenEighths.InverseInitialQuotientGeometry.quotientSet line 26
  4. theorem OAI.SevenEighths.InverseInitialQuotientGeometry.retained_sum line 30
  5. theorem OAI.SevenEighths.InverseInitialQuotientGeometry.retained_phase_independent line 45
  6. theorem OAI.SevenEighths.InverseInitialQuotientGeometry.quotientSet_nonzero line 62
  7. theorem OAI.SevenEighths.InverseInitialQuotientGeometry.quotientSet_eq_initial line 70
  8. theorem OAI.SevenEighths.InverseInitialQuotientGeometry.quotient_norm_eq line 81
  9. theorem OAI.SevenEighths.InverseInitialQuotientGeometry.retained_norm_windows line 96
  10. theorem OAI.SevenEighths.InverseInitialQuotientGeometry.retained_quotient_bound line 114
  11. theorem OAI.SevenEighths.InverseInitialQuotientGeometry.endpoint_threshold line 141
  12. theorem OAI.SevenEighths.InverseInitialQuotientGeometry.quotientSet_empty_iff line 151
  13. theorem OAI.SevenEighths.InverseInitialQuotientGeometry.retained_empty_sum line 155
  14. theorem OAI.SevenEighths.InverseInitialQuotientGeometry.nonempty_radius line 165
  15. def OAI.SevenEighths.InverseInitialQuotientGeometry.normalizedMass line 177
  16. theorem OAI.SevenEighths.InverseInitialQuotientGeometry.normalized_mass_bound line 180
  17. theorem OAI.SevenEighths.InverseInitialQuotientGeometry.retained_normalized_mass line 208
  18. theorem OAI.SevenEighths.InverseInitialQuotientGeometry.retained_normalized_mass_pi line 226
  19. theorem OAI.SevenEighths.InverseInitialQuotientGeometry.radical_norm_le line 247
  20. theorem OAI.SevenEighths.InverseInitialQuotientGeometry.radical_product_bound line 252
  21. def OAI.SevenEighths.InverseInitialQuotientGeometry.assignedCenter line 263
  22. theorem OAI.SevenEighths.InverseInitialQuotientGeometry.assigned_register line 265
  23. def OAI.SevenEighths.InverseInitialQuotientGeometry.assignedElement line 276
  24. theorem OAI.SevenEighths.InverseInitialQuotientGeometry.assigned_norm_bound line 278
  25. theorem OAI.SevenEighths.InverseInitialQuotientGeometry.assigned_norm_power line 291
  26. theorem OAI.SevenEighths.InverseInitialQuotientGeometry.retained_assigned_puncture_bound line 306
  27. theorem OAI.SevenEighths.InverseInitialQuotientGeometry.span_source_puncture line 332
  28. def OAI.SevenEighths.InverseInitialQuotientGeometry.punctureLength line 340
  29. theorem OAI.SevenEighths.InverseInitialQuotientGeometry.retained_puncture_length_bound line 345
  30. theorem OAI.SevenEighths.InverseInitialQuotientGeometry.retained_initial_margins line 382
  31. theorem OAI.SevenEighths.InverseInitialQuotientGeometry.all_endpoint_threshold line 416
  32. theorem OAI.SevenEighths.InverseInitialQuotientGeometry.retained_nonempty_radius line 428
  33. theorem OAI.SevenEighths.InverseInitialQuotientGeometry.assigned_cutoffs_of_term line 443
  34. theorem OAI.SevenEighths.InverseInitialQuotientGeometry.retained_assigned_term line 459