OAI/MeasureTheory/FalconerCompletion/Recursion/EuclideanFarKernelOccupiedIntegrable.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Recursive policies and quantitative depth estimates.

  1. lemma OAI.GraphLiteralSupport.Attempt4FullFar.euclideanFarKernelND_occupied_integrable line 18
  2. theorem OAI.GraphLiteralSupport.Attempt4FullFar.euclidean_source_comparable_far_branchND line 41
  3. lemma OAI.GraphLiteralSupport.Attempt4FullFar.far_depth_card_leND line 145
  4. theorem OAI.GraphLiteralSupport.Attempt4FullFar.far_depth_error_eventuallyND line 157