OAI/NumberTheory/Jacobsthal/Estimates/JointReturnCylinder.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.kernel_comp_comap line 15
  2. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.kernelProjection_power line 23
  3. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.survivingHistory_zero line 36
  4. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawKilledPair_kernel_projection line 44
  5. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawCapturedPair_kernel_projection line 52
  6. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.survivingHistory_kernel_projection line 60
  7. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.fullPairReturn line 74
  8. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.firstReturnHistory_kernel_projection line 77
  9. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.costKilled_kernel_projection line 84
  10. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.costCaptured_kernel_projection line 89
  11. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.firstReturn_fullPair_projection line 94
  12. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.firstReturnHistory_endpoint line 103
  13. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.returnCylinderTo line 120
  14. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.returnCylinderTo_exact line 125
  15. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.avoidOddReturns_first_pair line 128
  16. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.returnCylinderTo_first_pair line 159
  17. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.returnCylinderTo_retains_past line 170
  18. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.returnCylinderTo_retains_coordinate line 175
  19. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.keepFirstEvenUpdate line 194
  20. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.keepFirstEvenUpdate_measurable line 196
  21. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.firstEvenReturnContinuation line 199
  22. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.firstEvenReturnContinuation_isFiniteKernel line 202
  23. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.firstEvenReturnContinuation_apply line 206
  24. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.firstEvenReturnContinuation_lintegral line 214
  25. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.capturedFirstPair line 224
  26. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.killedFirstPair line 227
  27. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.capturedFirstPair_isFiniteKernel line 230
  28. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.killedFirstPair_isFiniteKernel line 234
  29. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.sourceReturnTerm line 238
  30. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.sourceReturnTerm_isFiniteKernel line 242
  31. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.capturedFirstPair_forget line 245
  32. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.killedFirstPair_forget line 250
  33. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.firstEvenReturnContinuation_forget line 255
  34. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.sourceReturnTerm_forget line 261
  35. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.fullPairKilled_pow_isFiniteKernel line 293
  36. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.fullPairReturn_isFiniteKernel line 298
  37. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.returnPairReward line 302
  38. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.returnPairReward_measurable line 305
  39. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.sourceReturnTerm_succ_reward line 314
  40. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.killedFirstPair_trace line 332
  41. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.capturedFirstPair_trace line 341
  42. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawKilledFirstPair_trace line 350
  43. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawCapturedFirstPair_trace line 362
  44. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawCyclePairEval line 386
  45. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawCyclePairEval_measurable line 389
  46. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.returnCylinderTo_projection line 392
  47. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawRemainder_pair_reward line 398
  48. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.firstReturnHistory_joint line 419