OAI/NumberTheory/Jacobsthal/Estimates/RawInitialEven.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.lookaheadInputCost line 14
  2. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.lookaheadInputCost_measurable line 19
  3. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.sourceBranchWitness_mass line 24
  4. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.sourceLookahead_lintegral line 31
  5. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.sourceLookahead_cost_law line 62
  6. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawLookaheadCostLaw line 84
  7. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawLookaheadCostLaw_eq line 88
  8. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawWaitingWordTerm line 111
  9. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawSpacingWordTerm line 114
  10. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawWaitingWordTerm_eq line 117
  11. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawSpacingWordTerm_eq line 122
  12. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawWaitingCostLaw line 128
  13. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawSpacingCostLaw line 131
  14. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawWaitingCostLaw_eq line 134
  15. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawSpacingCostLaw_eq line 141
  16. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawAllocatedCostLaws_mass_one line 148
  17. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.sourceCycleWitness_endpoint line 167
  18. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawReturnEndpointState line 175
  19. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawReturnEndpointState_measurable line 178
  20. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawReturnTrace_endpoint line 181
  21. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawReturnPastState line 194
  22. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawReturnPastState_measurable line 197
  23. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawReturnPastState_ae line 210
  24. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawReturnTrace_input_endpoint line 221
  25. abbrev OAI.Erdos970.Erdos970Dependency.MarkedVisits.RawContinuationTrace line 240
  26. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawContinuationKernel line 242
  27. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawContinuationKernel_isFiniteKernel line 248
  28. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawContinuationSignature line 253
  29. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawContinuationSignature_measurable line 257
  30. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawContinuation_signature line 261
  31. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawExtension_last_step line 296
  32. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawFirstOdd_draw_law line 304
  33. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.oddCostStates line 309
  34. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.oddCostStates_measurable line 311
  35. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.embedOdd_mem_oddCostStates line 314
  36. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.embed_decodeReturnedOdd_of_oddCostStates line 316
  37. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawFirstOdd_ae_odd line 324
  38. abbrev OAI.Erdos970.Erdos970Dependency.MarkedVisits.RawInitialEvenTrace line 332
  39. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawInitialEvenKernel line 334
  40. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawInitialEvenKernel_isFiniteKernel line 337
  41. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.initialOddReturnJoint line 341
  42. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.initialOddReturnJoint_isMarkovKernel line 344
  43. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.embedOddPair line 348
  44. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.embedOddPair_measurable line 350
  45. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawInitialEven_joint_signature line 353
  46. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawInitialEvenDuration line 390
  47. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawInitialEvenDuration_positive line 393
  48. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawInitialEven_mass_one line 398