OAI/NumberTheory/Jacobsthal/Estimates/OnePairCost.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.Erdos970Dependency.InvariantCostBound.evenCost line 18
  2. def OAI.Erdos970.Erdos970Dependency.InvariantCostBound.oddCost line 19
  3. def OAI.Erdos970.Erdos970Dependency.InvariantCostBound.evenMajor line 20
  4. def OAI.Erdos970.Erdos970Dependency.InvariantCostBound.oddMajor line 21
  5. theorem OAI.Erdos970.Erdos970Dependency.InvariantCostBound.cost_le_inv line 23
  6. theorem OAI.Erdos970.Erdos970Dependency.InvariantCostBound.evenCost_nonneg line 28
  7. theorem OAI.Erdos970.Erdos970Dependency.InvariantCostBound.oddCost_nonneg line 34
  8. theorem OAI.Erdos970.Erdos970Dependency.InvariantCostBound.evenCost_le_major line 40
  9. theorem OAI.Erdos970.Erdos970Dependency.InvariantCostBound.oddCost_le_major line 52
  10. theorem OAI.Erdos970.Erdos970Dependency.InvariantCostBound.evenMajor_integrable line 68
  11. theorem OAI.Erdos970.Erdos970Dependency.InvariantCostBound.oddMajor_integrable line 71
  12. theorem OAI.Erdos970.Erdos970Dependency.InvariantCostBound.evenCost_integrable line 74
  13. theorem OAI.Erdos970.Erdos970Dependency.InvariantCostBound.oddCost_integrable line 81
  14. theorem OAI.Erdos970.Erdos970Dependency.InvariantCostBound.even_cost_bound line 88
  15. theorem OAI.Erdos970.Erdos970Dependency.InvariantCostBound.odd_cost_bound line 93
  16. theorem OAI.Erdos970.Erdos970Dependency.InvariantCostBound.even_cost_pos line 98
  17. def OAI.Erdos970.Erdos970Dependency.InvariantCostBound.costMass line 107
  18. theorem OAI.Erdos970.Erdos970Dependency.InvariantCostBound.costMass_pos line 109
  19. theorem OAI.Erdos970.Erdos970Dependency.InvariantCostBound.costMass_le line 112
  20. def OAI.Erdos970.Erdos970Dependency.RawStateCost.stateCost line 130
  21. theorem OAI.Erdos970.Erdos970Dependency.RawStateCost.stateCost_measurable line 132
  22. theorem OAI.Erdos970.Erdos970Dependency.RawStateCost.stateCost_bounds line 134
  23. theorem OAI.Erdos970.Erdos970Dependency.RawStateCost.stateCost_integrable line 141
  24. theorem OAI.Erdos970.Erdos970Dependency.RawStateCost.integral_evenMeasure line 147
  25. theorem OAI.Erdos970.Erdos970Dependency.RawStateCost.integral_oddMeasure line 155
  26. theorem OAI.Erdos970.Erdos970Dependency.RawStateCost.even_lifted_cost line 163
  27. theorem OAI.Erdos970.Erdos970Dependency.RawStateCost.odd_lifted_cost line 171
  28. theorem OAI.Erdos970.Erdos970Dependency.RawStateCost.state_cost_integral line 179
  29. theorem OAI.Erdos970.Erdos970Dependency.RawStateCost.occupation_increment_integrable line 195
  30. theorem OAI.Erdos970.Erdos970Dependency.RawStateCost.occupation_increment_integral line 199
  31. def OAI.Erdos970.Erdos970Dependency.OnePairCost.pairIncrement line 218
  32. theorem OAI.Erdos970.Erdos970Dependency.OnePairCost.increment_test_measurable line 221
  33. theorem OAI.Erdos970.Erdos970Dependency.OnePairCost.age_test_measurable line 224
  34. theorem OAI.Erdos970.Erdos970Dependency.OnePairCost.pairIncrement_measurable line 227
  35. theorem OAI.Erdos970.Erdos970Dependency.OnePairCost.even_increment_measurable line 229
  36. theorem OAI.Erdos970.Erdos970Dependency.OnePairCost.odd_increment_measurable line 233
  37. theorem OAI.Erdos970.Erdos970Dependency.OnePairCost.pairIncrement_formula line 237
  38. theorem OAI.Erdos970.Erdos970Dependency.OnePairCost.paired_age_balance line 251
  39. theorem OAI.Erdos970.Erdos970Dependency.OnePairCost.captured_killed_age_balance line 267