OAI/NumberTheory/GaussianMoat/MultiscaleSchedule.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.GaussianMoat.EnrichmentMargins line 10
  2. theorem OAI.GaussianMoat.TimeLaw.geometric_step_deficit line 25
  3. lemma OAI.GaussianMoat.SplitSieve.pointEntropy_nonneg line 44
  4. def OAI.GaussianMoat.TimeLaw.run line 50
  5. lemma OAI.GaussianMoat.TimeLaw.run_zero line 54
  6. lemma OAI.GaussianMoat.TimeLaw.run_succ line 56
  7. theorem OAI.GaussianMoat.TimeLaw.run_entropy line 59
  8. theorem OAI.GaussianMoat.TimeLaw.advance_entropy line 84
  9. theorem OAI.GaussianMoat.TimeLaw.run_future_entropy line 105
  10. def OAI.GaussianMoat.TimeLaw.observe line 120
  11. lemma OAI.GaussianMoat.TimeLaw.ext_observe line 123
  12. lemma OAI.GaussianMoat.TimeLaw.observe_advance line 139
  13. lemma OAI.GaussianMoat.ForwardKernel.then_observe line 146
  14. lemma OAI.GaussianMoat.TimeLaw.advance_then line 158
  15. lemma OAI.GaussianMoat.TimeLaw.advance_common_cons line 184
  16. lemma OAI.GaussianMoat.TimeLaw.advance_common_append line 189
  17. lemma OAI.GaussianMoat.TimeLaw.foldl_ofFn line 198
  18. lemma OAI.GaussianMoat.TimeLaw.run_common line 208
  19. lemma OAI.GaussianMoat.log_floor_exp line 215
  20. theorem OAI.GaussianMoat.EnrichmentMargins.from_scale line 233
  21. def OAI.GaussianMoat.bandScale line 323
  22. def OAI.GaussianMoat.bandLength line 324
  23. def OAI.GaussianMoat.bandSize line 325
  24. lemma OAI.GaussianMoat.bandScale_pos line 327
  25. lemma OAI.GaussianMoat.bandScale_antitone line 330
  26. lemma OAI.GaussianMoat.bandScale_succ line 336
  27. theorem OAI.GaussianMoat.geometric_band_margins line 342
  28. theorem OAI.GaussianMoat.TimeLaw.geometric_band_entropy line 367
  29. lemma OAI.GaussianMoat.commonSchedule_log_bound line 386
  30. lemma OAI.GaussianMoat.suffix_entropy_cost line 410