OAI/MeasureTheory/FalconerCompletion/Recursion/PolicyDescriptorAnchorGtStart.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Recursive policies and quantitative depth estimates.

  1. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.policyDescriptor_anchor_gt_start line 24
  2. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.policyDescriptorList_subset_unreached line 34
  3. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.actualResidualAmbientGood_subset_farChild line 42
  4. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.actualResidualPairAmbientGood_subset_farChild line 54
  5. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.positiveDistanceCountND_mono line 65
  6. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.farChildMaximumND_mono line 72
  7. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.actualResidual_farChildMaximum_le line 92