OAI/MeasureTheory/FalconerCompletion/Recursion/MaskScale2.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Recursive policies and quantitative depth estimates.

  1. def OAI.GraphLiteralSupport.Attempt4PrefixShell.sourceMaskScaleND line 18
  2. def OAI.GraphLiteralSupport.Attempt4PrefixShell.sourceMaskRadiusND line 21
  3. def OAI.GraphLiteralSupport.Attempt4PrefixShell.sourceTestWidthND line 24
  4. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.sourceMaskScaleND_one_le line 27
  5. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.sourceMaskScaleND_pos line 29
  6. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.sourceMaskRadiusND_pos line 32
  7. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.sourceMaskScaleND_mono line 35
  8. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.sourceMaskScaleND_inv_depth line 40
  9. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.sourceTestWidthND_gap line 50
  10. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.source_mask_width_gapND line 59
  11. theorem OAI.GraphLiteralSupport.Attempt4PrefixShell.source_mask_width_gap_eventuallyND line 83