OAI/MeasureTheory/FalconerCompletion/Angular/InnerNormalizedOfClose.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Angular cutoffs and derivative estimates.

  1. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.inner_normalized_of_close line 21
  2. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.separatedAxis line 38
  3. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.separatedCutoff line 41
  4. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.separatedCutoff_contDiff line 44
  5. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.separatedCutoff_norm_le line 49
  6. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.separated_direction_inner line 54
  7. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.separatedCutoff_local line 77
  8. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.gridOffsetVector line 110
  9. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.grid_centers_sub line 113
  10. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.normalized_pos_smul line 122
  11. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.separatedAxis_offset line 127
  12. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.separatedCutoff_offset line 132
  13. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.separatedOffsets line 137
  14. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.separatedOffsets_finite line 140
  15. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.gridOffset_mem line 143
  16. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.eventually_all_separated_cutoffs line 162
  17. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.uniform_separatedCutoff_derivatives line 173