OAI/NumberTheory/GaussianMoat/PointEnrichment.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.GaussianMoat.latticeBall_card_le line 12
  2. theorem OAI.GaussianMoat.displacement_entropy_le line 25
  3. theorem OAI.GaussianMoat.differences_rectangle line 36
  4. lemma OAI.GaussianMoat.difference_exists_pair line 58
  5. def OAI.GaussianMoat.differenceRepresentative line 66
  6. lemma OAI.GaussianMoat.differenceRepresentative_spec line 70
  7. lemma OAI.GaussianMoat.differenceRepresentative_injective line 75
  8. lemma OAI.GaussianMoat.differences_walkSegment_nonempty line 81
  9. def OAI.GaussianMoat.FinLaw.joint line 92
  10. theorem OAI.GaussianMoat.FinLaw.joint_mass line 98
  11. theorem OAI.GaussianMoat.FinLaw.joint_map_fst line 101
  12. theorem OAI.GaussianMoat.FinLaw.joint_map_snd line 109
  13. theorem OAI.GaussianMoat.FinLaw.joint_map_second line 114
  14. theorem OAI.GaussianMoat.FinLaw.entropy_joint line 125
  15. theorem OAI.GaussianMoat.FinLaw.Hf_map line 130
  16. theorem OAI.GaussianMoat.FinLaw.cHf_map line 138
  17. theorem OAI.GaussianMoat.FinLaw.Hf_joint_pair line 142
  18. theorem OAI.GaussianMoat.FinLaw.cHf_mix_ge line 155
  19. theorem OAI.GaussianMoat.FinLaw.joint_map_fiber line 176
  20. theorem OAI.GaussianMoat.FinLaw.Hf_joint_pair_vary line 187
  21. theorem OAI.GaussianMoat.FinLaw.cHf_joint_ge line 203
  22. theorem OAI.GaussianMoat.FinLaw.Hf_pair_const_right line 223
  23. theorem OAI.GaussianMoat.FinLaw.Hf_joint_ge line 229
  24. def OAI.GaussianMoat.SplitSieve.pointEntropy line 238
  25. def OAI.GaussianMoat.SplitSieve.freshCoordinate line 242
  26. lemma OAI.GaussianMoat.SplitSieve.freshCoordinate_map line 250
  27. def OAI.GaussianMoat.differenceLaw line 258
  28. theorem OAI.GaussianMoat.differenceLaw_fresh line 263
  29. theorem OAI.GaussianMoat.SplitSieve.freshCoordinate_joint_ge line 290
  30. lemma OAI.GaussianMoat.pointEntropy_fair_endpoint line 302
  31. theorem OAI.GaussianMoat.SplitSieve.point_enrichment_accounting line 318
  32. theorem OAI.GaussianMoat.SplitSieve.actual_enrichment line 342
  33. lemma OAI.GaussianMoat.fresh_error_bounds line 365
  34. lemma OAI.GaussianMoat.fresh_gap_bound line 398
  35. theorem OAI.GaussianMoat.SplitSieve.differenceLaw_fresh_lower line 410
  36. lemma OAI.GaussianMoat.SplitSieve.meanLog_bounds line 460
  37. theorem OAI.GaussianMoat.SplitSieve.walk_fresh_lower line 473