OAI/MeasureTheory/FalconerCompletion/Recursion/NominalRadius.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Recursive policies and quantitative depth estimates.

  1. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.nominalRadius line 23
  2. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.testWidth_gap line 26
  3. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.uniform_testWidth_gap line 35
  4. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.fullParallelCount_transfer line 62
  5. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.classConditional_ae_mem line 85
  6. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.fullProjectionCollision_transfer line 89
  7. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.ValidDescriptor line 110
  8. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.policyDescriptor_valid line 114
  9. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.policyDescriptor_anchor_le_end line 119
  10. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.uniform_descriptorGood_transfer line 125
  11. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.dyadic_ratio_nominal line 149
  12. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.same_tree_ancestor line 162
  13. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.fine_radial_dist line 172
  14. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.uniform_suffix_good_transport line 206
  15. def OAI.GraphLiteralSupport.CurrentFalconer.sourceMaskScaleND line 264
  16. def OAI.GraphLiteralSupport.CurrentFalconer.sourceMaskRadiusND line 267
  17. def OAI.GraphLiteralSupport.CurrentFalconer.sourceTestWidthND line 270
  18. lemma OAI.GraphLiteralSupport.CurrentFalconer.sourceMaskScaleND_one_le line 273
  19. lemma OAI.GraphLiteralSupport.CurrentFalconer.sourceMaskScaleND_pos line 275
  20. lemma OAI.GraphLiteralSupport.CurrentFalconer.sourceMaskRadiusND_pos line 278
  21. lemma OAI.GraphLiteralSupport.CurrentFalconer.sourceMaskScaleND_mono line 281
  22. lemma OAI.GraphLiteralSupport.CurrentFalconer.sourceMaskScaleND_inv_depth line 286