OAI/NumberTheory/Jacobsthal/Paths/CostPrefixTransport.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.Erdos970.NumberTheoryLean.CostPrefixTransport.costKernel_pow_markov line 17
  2. def OAI.Erdos970.NumberTheoryLean.CostPrefixTransport.stateProjection line 25
  3. theorem OAI.Erdos970.NumberTheoryLean.CostPrefixTransport.projection_intertwines line 27
  4. theorem OAI.Erdos970.NumberTheoryLean.CostPrefixTransport.projection_intertwines_pow line 33
  5. theorem OAI.Erdos970.NumberTheoryLean.CostPrefixTransport.costKernel_pow_map_state line 44
  6. theorem OAI.Erdos970.NumberTheoryLean.CostPrefixTransport.stateRatio_ge_half line 51
  7. theorem OAI.Erdos970.NumberTheoryLean.CostPrefixTransport.costKernel_cost_bounds line 56
  8. theorem OAI.Erdos970.NumberTheoryLean.CostPrefixTransport.costKernel_pow_cost_bounds line 70
  9. def OAI.Erdos970.NumberTheoryLean.CostPrefixTransport.inclusiveOccupation line 93
  10. instance OAI.Erdos970.NumberTheoryLean.CostPrefixTransport.inclusiveOccupation_isSFiniteKernel line 95
  11. theorem OAI.Erdos970.NumberTheoryLean.CostPrefixTransport.inclusiveOccupation_translation line 99
  12. theorem OAI.Erdos970.NumberTheoryLean.CostPrefixTransport.inclusive_comp_step line 105
  13. def OAI.Erdos970.NumberTheoryLean.CostPrefixTransport.prefixOccupation line 109
  14. instance OAI.Erdos970.NumberTheoryLean.CostPrefixTransport.prefixOccupation_isSFiniteKernel line 111
  15. theorem OAI.Erdos970.NumberTheoryLean.CostPrefixTransport.full_comp_step_le line 115
  16. theorem OAI.Erdos970.NumberTheoryLean.CostPrefixTransport.full_comp_pow_le line 120
  17. theorem OAI.Erdos970.NumberTheoryLean.CostPrefixTransport.prefixOccupation_le_full line 128