OAI/NumberTheory/Jacobsthal/Paths/FlaggedHarmonicPaths.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Erdos970.NumberTheoryLean.FlaggedHarmonicPaths.FlagState line 17
  2. abbrev OAI.Erdos970.NumberTheoryLean.FlaggedHarmonicPaths.ExponentState line 18
  3. def OAI.Erdos970.NumberTheoryLean.FlaggedHarmonicPaths.flagUpdate line 20
  4. theorem OAI.Erdos970.NumberTheoryLean.FlaggedHarmonicPaths.flagUpdate_joint_measurable line 23
  5. theorem OAI.Erdos970.NumberTheoryLean.FlaggedHarmonicPaths.flagUpdate_measurable line 31
  6. def OAI.Erdos970.NumberTheoryLean.FlaggedHarmonicPaths.kernel line 38
  7. instance OAI.Erdos970.NumberTheoryLean.FlaggedHarmonicPaths.kernel_isSFinite line 43
  8. theorem OAI.Erdos970.NumberTheoryLean.FlaggedHarmonicPaths.kernel_eq_map line 47
  9. theorem OAI.Erdos970.NumberTheoryLean.FlaggedHarmonicPaths.kernel_map_state line 59
  10. def OAI.Erdos970.NumberTheoryLean.FlaggedHarmonicPaths.coordinates line 65
  11. theorem OAI.Erdos970.NumberTheoryLean.FlaggedHarmonicPaths.coordinates_measurable line 68
  12. def OAI.Erdos970.NumberTheoryLean.FlaggedHarmonicPaths.initial line 72
  13. theorem OAI.Erdos970.NumberTheoryLean.FlaggedHarmonicPaths.gap_div_currentExponent line 75
  14. theorem OAI.Erdos970.NumberTheoryLean.FlaggedHarmonicPaths.initial_coordinates line 81
  15. theorem OAI.Erdos970.NumberTheoryLean.FlaggedHarmonicPaths.coordinates_update line 86
  16. theorem OAI.Erdos970.NumberTheoryLean.FlaggedHarmonicPaths.kernel_map_coordinates line 96
  17. theorem OAI.Erdos970.NumberTheoryLean.FlaggedHarmonicPaths.kernel_map_coordinates_le line 111