OAI/Probability/MemoryPrecision/RealContinuation.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MemoryPrecision.BlockCount line 19
  2. lemma OAI.MemoryPrecision.blockCount_mul_ge line 20
  3. lemma OAI.MemoryPrecision.blockCount_mono line 24
  4. lemma OAI.MemoryPrecision.blockCount_zero line 26
  5. lemma OAI.MemoryPrecision.blockCount_pos line 27
  6. def OAI.MemoryPrecision.StepConstant line 31
  7. lemma OAI.MemoryPrecision.stepConstant_one line 32
  8. lemma OAI.MemoryPrecision.stepConstant_pos line 33
  9. def OAI.MemoryPrecision.RealStep line 35
  10. lemma OAI.MemoryPrecision.realStep_one line 36
  11. lemma OAI.MemoryPrecision.realStep_pos line 40
  12. lemma OAI.MemoryPrecision.sphere_deterministic_step line 43
  13. lemma OAI.MemoryPrecision.SphereBallBound.mono line 68
  14. lemma OAI.MemoryPrecision.real_continuation_mass line 73