OAI/MeasureTheory/FalconerCompletion/Recursion/ClassConditional.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

Recursive policies and quantitative depth estimates.

  1. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.classConditional line 24
  2. instance OAI.GraphLiteralSupport.CurrentFalconer.TreeND.classConditional_finite line 28
  3. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.classConditional_probability line 33
  4. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.adjustedProfile line 43
  5. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.testWidth line 46
  6. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.fullParallelCount line 49
  7. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.fullParallelCount_actual_line line 55
  8. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.measurable_fullParallelCount line 63
  9. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.fullProjectionCollision line 84
  10. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.measurable_fullProjectionCollision line 89
  11. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.descriptorGood line 96
  12. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.measurable_descriptorGood line 108
  13. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.radialVector line 121
  14. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.norm_radialVector line 123
  15. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.measurable_radialVector line 128
  16. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.endpointGood line 133
  17. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.measurable_endpointGood line 139
  18. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.distanceGood line 150
  19. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.measurable_distanceGood line 157
  20. structure OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState line 168
  21. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.good line 178
  22. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.cellPair line 179
  23. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.pair line 180
  24. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.distance line 181
  25. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.levelMass line 182
  26. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.normalization line 183
  27. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.width line 184
  28. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.coincidence line 185
  29. instance OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.cellPair_finite line 188
  30. instance OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.pair_finite line 190
  31. instance OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.distance_finite line 192
  32. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.measurable_good line 195
  33. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.distance_apply line 198
  34. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.distance_collision line 204
  35. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.coincidence_four_point line 212
  36. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.coincidence_ne_top line 219
  37. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.RegularizedProfileData.normalized_cell_mass_le line 239
  38. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.normalized_cellPair_mass line 254
  39. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.normalized_cellPair_profile_mass line 266
  40. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.coincidence_trivial_profile_bound line 278
  41. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.actual_distance_terminal line 307
  42. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.actual_distance_terminal_rpow line 318