OAI/NumberTheory/DirichletL/Inversion/SecondFibers.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.SevenEighths.InverseSecondFibers.OuterTriple line 14
  2. structure OAI.SevenEighths.InverseSecondFibers.SecondTuple line 19
  3. structure OAI.SevenEighths.InverseSecondFibers.Valid line 30
  4. lemma OAI.SevenEighths.InverseSecondFibers.poisson_divisor_source line 46
  5. lemma OAI.SevenEighths.InverseSecondFibers.core_dvd_label line 52
  6. lemma OAI.SevenEighths.InverseSecondFibers.common_label_dvd line 66
  7. lemma OAI.SevenEighths.InverseSecondFibers.cube_product_dvd_square line 73
  8. lemma OAI.SevenEighths.InverseSecondFibers.cube_radical_dvd line 80
  9. lemma OAI.SevenEighths.InverseSecondFibers.cube_factor_dvd_target line 88
  10. lemma OAI.SevenEighths.InverseSecondFibers.core_dvd_outer_label line 94
  11. lemma OAI.SevenEighths.InverseSecondFibers.core_ne_zero line 107
  12. theorem OAI.SevenEighths.InverseSecondFibers.valid_key_injective line 127
  13. theorem OAI.SevenEighths.InverseSecondFibers.valid_tuple_card_le line 151
  14. lemma OAI.SevenEighths.InverseSecondFibers.divisor_card_sq_le line 200
  15. theorem OAI.SevenEighths.InverseSecondFibers.valid_tuple_card_le_separated line 204
  16. theorem OAI.SevenEighths.InverseSecondFibers.valid_tuple_card_le_slot_cap line 229
  17. theorem OAI.SevenEighths.InverseSecondFibers.valid_label_squarefree line 242
  18. theorem OAI.SevenEighths.InverseSecondFibers.cube_quotient_norm_sq_le line 264
  19. theorem OAI.SevenEighths.InverseSecondFibers.cube_quotient_norm_le line 285
  20. def OAI.SevenEighths.InverseSecondFibers.originalSource line 293
  21. def OAI.SevenEighths.InverseSecondFibers.sourceTriples line 300
  22. theorem OAI.SevenEighths.InverseSecondFibers.mem_sourceTriples line 306
  23. theorem OAI.SevenEighths.InverseSecondFibers.sourceTriples_property line 316
  24. theorem OAI.SevenEighths.InverseSecondFibers.sourceTriples_cube_norm_le line 325
  25. def OAI.SevenEighths.InverseSecondFibers.secondFiber line 340
  26. theorem OAI.SevenEighths.InverseSecondFibers.secondFiber_outer_mem line 347
  27. theorem OAI.SevenEighths.InverseSecondFibers.secondFiber_empty_of_not_sourceTriple line 356
  28. theorem OAI.SevenEighths.InverseSecondFibers.secondFiber_card_le line 367
  29. theorem OAI.SevenEighths.InverseSecondFibers.secondFiber_weight_bound line 379