OAI/NumberTheory/GaussianMoat/WalkPackage.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.GaussianMoat.WalkPackage line 10
  2. def OAI.GaussianMoat.ForwardKernel.packageSymbol line 12
  3. def OAI.GaussianMoat.ForwardKernel.packageLaw line 18
  4. def OAI.GaussianMoat.WalkPackage.prefix line 24
  5. lemma OAI.GaussianMoat.ForwardKernel.packageSymbol_prefix line 28
  6. def OAI.GaussianMoat.WalkPackage.Hits line 36
  7. lemma OAI.GaussianMoat.ForwardKernel.package_true_survives line 40
  8. lemma OAI.GaussianMoat.FinLaw.mass_map_eq_prob line 53
  9. theorem OAI.GaussianMoat.ForwardKernel.smoothed_package_floor line 56
  10. def OAI.GaussianMoat.ForwardKernel.passingException line 80
  11. lemma OAI.GaussianMoat.ForwardKernel.passingException_card line 84
  12. lemma OAI.GaussianMoat.ForwardKernel.not_mem_passingException line 90
  13. lemma OAI.GaussianMoat.SplitSieve.avoids_signed line 100
  14. theorem OAI.GaussianMoat.smoothed_batch_package_information line 107
  15. lemma OAI.GaussianMoat.FinLaw.cIf_congr_fibers line 154
  16. lemma OAI.GaussianMoat.FinLaw.joint_map_cIf line 168
  17. theorem OAI.GaussianMoat.ForwardKernel.package_information_transport line 176
  18. lemma OAI.GaussianMoat.perm_expect_uniform line 226
  19. def OAI.GaussianMoat.SplitSieve.selectedIndex line 238
  20. lemma OAI.GaussianMoat.SplitSieve.selected_sum_average line 242
  21. lemma OAI.GaussianMoat.selected_prefix_fibers line 255
  22. lemma OAI.GaussianMoat.SplitSieve.selected_residue_fibers line 272
  23. lemma OAI.GaussianMoat.SplitSieve.selected_entropy_average line 286
  24. lemma OAI.GaussianMoat.SplitSieve.selected_log_average line 296
  25. theorem OAI.GaussianMoat.averaged_batch_package_information line 305