OAI/MeasureTheory/FalconerCompletion/Recursion/FarCommonDepthUpper.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Recursive policies and quantitative depth estimates.

  1. lemma OAI.GraphLiteralSupport.Attempt4FullFar.far_common_depth_upperND line 16
  2. lemma OAI.GraphLiteralSupport.Attempt4FullFar.mem_ambientGridCell_floorND line 29
  3. lemma OAI.GraphLiteralSupport.Attempt4FullFar.ambientGridCell_subset_of_common_pointND line 35
  4. theorem OAI.GraphLiteralSupport.Attempt4FullFar.exists_far_grid_coverND line 46