OAI/MeasureTheory/Falconer/Recursion/PolicyDescriptors.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.PlanarFalconer.PolicyDescriptor line 9
  2. def OAI.PlanarFalconer.descriptorAnchor line 14
  3. def OAI.PlanarFalconer.descriptorLength line 18
  4. def OAI.PlanarFalconer.originDescriptors line 22
  5. def OAI.PlanarFalconer.policyOrigins line 28
  6. def OAI.PlanarFalconer.policyDescriptorList line 32
  7. theorem OAI.PlanarFalconer.policyOrigins_mono line 35
  8. theorem OAI.PlanarFalconer.policyDescriptorList_mono line 41
  9. theorem OAI.PlanarFalconer.originDescriptor_anchor line 48
  10. theorem OAI.PlanarFalconer.policyDescriptor_anchor_mem line 58
  11. theorem OAI.PlanarFalconer.originDescriptor_length line 67
  12. theorem OAI.PlanarFalconer.policyDescriptor_origin line 87
  13. theorem OAI.PlanarFalconer.originDescriptors_card line 98
  14. theorem OAI.PlanarFalconer.policyDescriptorList_card line 112