OAI/Analysis/CircleDomains/Probability/RecursiveCodeLaw.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

The proved outputs retained at one stage of the endpoint-law recursion. The candidate includes actual densities and quantitative mark budgets.

  1. structure OAI.CircleDomainRigidity.RecursiveCodeGeometry line 20
  2. structure OAI.CircleDomainRigidity.RecursiveLawBudgets line 35
  3. def OAI.CircleDomainRigidity.RecursiveLawWitness line 44
  4. abbrev OAI.CircleDomainRigidity.RecursiveLawWitness.budgets line 57
  5. abbrev OAI.CircleDomainRigidity.RecursiveLawWitness.law line 58
  6. abbrev OAI.CircleDomainRigidity.RecursiveLawWitness.candidate line 59
  7. def OAI.CircleDomainRigidity.RecursiveLawWitness.hitConstant line 60
  8. theorem OAI.CircleDomainRigidity.RecursiveLawWitness.finite_hit_tests line 61
  9. theorem OAI.CircleDomainRigidity.RecursiveLawWitness.countable_dust_hits line 64
  10. def OAI.CircleDomainRigidity.RecursiveCodeLaw line 68
  11. abbrev OAI.CircleDomainRigidity.RecursiveCodeLaw.geometry line 79
  12. abbrev OAI.CircleDomainRigidity.RecursiveCodeLaw.witness line 80
  13. abbrev OAI.CircleDomainRigidity.RecursiveCodeLaw.data line 81
  14. abbrev OAI.CircleDomainRigidity.RecursiveCodeLaw.physical_eq line 82
  15. abbrev OAI.CircleDomainRigidity.RecursiveCodeLaw.quotient_eq line 83
  16. abbrev OAI.CircleDomainRigidity.RecursiveCodeLaw.dust_eq line 84
  17. abbrev OAI.CircleDomainRigidity.RecursiveCodeLaw.anchor_eq line 85
  18. abbrev OAI.CircleDomainRigidity.RecursiveCodeLaw.levels_eq line 86
  19. abbrev OAI.CircleDomainRigidity.RecursiveCodeLaw.weights_eq line 87
  20. abbrev OAI.CircleDomainRigidity.RecursiveCodeLaw.domain_agrees line 88
  21. abbrev OAI.CircleDomainRigidity.RecursiveCodeLaw.target_dust line 89
  22. abbrev OAI.CircleDomainRigidity.RecursiveCodeLaw.presentation line 90
  23. abbrev OAI.CircleDomainRigidity.RecursiveCodeLaw.prior_deletions_eq line 91
  24. abbrev OAI.CircleDomainRigidity.RecursiveCodeLaw.flag_deletions_eq line 92
  25. abbrev OAI.CircleDomainRigidity.RecursiveCodeLaw.law line 93
  26. abbrev OAI.CircleDomainRigidity.RecursiveCodeLaw.candidate line 94
  27. abbrev OAI.CircleDomainRigidity.RecursiveCodeLaw.hitConstant line 95
  28. abbrev OAI.CircleDomainRigidity.RecursiveCodeLaw.finite_hit_tests line 96
  29. abbrev OAI.CircleDomainRigidity.RecursiveCodeLaw.countable_dust_hits line 97
  30. abbrev OAI.CircleDomainRigidity.RecursiveCodeLaw.occupationMass line 98
  31. abbrev OAI.CircleDomainRigidity.RecursiveCodeLaw.tupleMass line 99
  32. abbrev OAI.CircleDomainRigidity.RecursiveCodeLaw.energy line 100
  33. abbrev OAI.CircleDomainRigidity.RecursiveCodeLaw.visitConstant line 101
  34. abbrev OAI.CircleDomainRigidity.RecursiveCodeLaw.occupationMass_finite line 102
  35. abbrev OAI.CircleDomainRigidity.RecursiveCodeLaw.energy_finite line 103
  36. abbrev OAI.CircleDomainRigidity.RecursiveCodeLaw.visitConstant_finite line 104
  37. def OAI.CircleDomainRigidity.RecursiveCodeLaw.density line 106
  38. theorem OAI.CircleDomainRigidity.RecursiveCodeLaw.density_measurable line 108
  39. theorem OAI.CircleDomainRigidity.RecursiveCodeLaw.occupation_eq line 110
  40. theorem OAI.CircleDomainRigidity.RecursiveCodeLaw.density_energy_finite line 113
  41. theorem OAI.CircleDomainRigidity.RecursiveCodeLaw.finite_occupation line 116
  42. theorem OAI.CircleDomainRigidity.RecursiveCodeLaw.hit_square_finite line 121
  43. theorem OAI.CircleDomainRigidity.RecursiveCodeLaw.tuple_absolutelyContinuous line 129
  44. theorem OAI.CircleDomainRigidity.RecursiveCodeLaw.prior_visit_norm_finite line 134
  45. theorem OAI.CircleDomainRigidity.RecursiveCodeLaw.flag_visit_norm_finite line 140
  46. theorem OAI.CircleDomainRigidity.RecursiveCodeLaw.full_hit_support_countable line 146