OAI/MeasureTheory/FalconerCompletion/Recursion/TensorCapCompact.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Recursive policies and quantitative depth estimates.

  1. lemma OAI.GraphLiteralSupport.CurrentFalconer.tensorCapND_compact line 22
  2. lemma OAI.GraphLiteralSupport.CurrentFalconer.bufferedMaskND_compact line 28
  3. lemma OAI.GraphLiteralSupport.CurrentFalconer.evenBufferedMaskND_compact line 38
  4. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.actualDescriptorSmooth_compact line 47
  5. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.actualEndpointAngular_global_bound line 53
  6. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.actualAngularProduct_global_bound line 95
  7. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.prefixInverse_global_bound line 111