OAI/NumberTheory/Jacobsthal/Estimates/LowStateHorizon.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos970.NumberTheoryLean.LowStateHorizon.cost_ge_inv_add_one line 16
  2. theorem OAI.Erdos970.NumberTheoryLean.LowStateHorizon.stateRatio_ge_nineteen_twentieths line 25
  3. theorem OAI.Erdos970.NumberTheoryLean.LowStateHorizon.costKernel_time_update line 30
  4. theorem OAI.Erdos970.NumberTheoryLean.LowStateHorizon.harmonicKernel_time_update line 41
  5. def OAI.Erdos970.NumberTheoryLean.LowStateHorizon.lowDomain line 45
  6. theorem OAI.Erdos970.NumberTheoryLean.LowStateHorizon.lowDomain_measurable line 47
  7. def OAI.Erdos970.NumberTheoryLean.LowStateHorizon.lowKernel line 50
  8. theorem OAI.Erdos970.NumberTheoryLean.LowStateHorizon.low_step_clock line 53
  9. theorem OAI.Erdos970.NumberTheoryLean.LowStateHorizon.low_pow_clock line 65
  10. theorem OAI.Erdos970.NumberTheoryLean.LowStateHorizon.low_pow_terminal line 85
  11. theorem OAI.Erdos970.NumberTheoryLean.LowStateHorizon.low_pow_zero_of_clock line 95
  12. def OAI.Erdos970.NumberTheoryLean.LowStateHorizon.sourceHorizon line 117
  13. theorem OAI.Erdos970.NumberTheoryLean.LowStateHorizon.source_low_horizon line 119
  14. theorem OAI.Erdos970.NumberTheoryLean.LowStateHorizon.source_horizon_log_cube line 148
  15. theorem OAI.Erdos970.NumberTheoryLean.LowStateHorizon.tilted_source_horizon line 160
  16. theorem OAI.Erdos970.NumberTheoryLean.LowStateHorizon.harmonic_source_horizon line 165