OAI/MeasureTheory/FalconerCompletion/Recursion/PrefixDescriptors.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Recursive policies and quantitative depth estimates.

  1. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.prefixDescriptors line 29
  2. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.prefixEndpointSmooth line 32
  3. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.prefix_pairMask_eq line 37
  4. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.prefix_pairMask_radial line 49
  5. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.prefix_shell_transform_exact line 56
  6. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.prefixEndpoint_norm_le line 91
  7. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.prefixDescriptors_card line 96
  8. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.prefixDescriptor_scale line 104
  9. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.prefixShell_le_sourceShell line 111
  10. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.uniform_prefixEndpoint_derivatives line 134
  11. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.uniform_actual_prefix_pair_symbol line 147