OAI/MeasureTheory/FalconerCompletion/Estimates/NormLinearErrorIdentity.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Quantitative estimates for the distance-set construction.

  1. lemma OAI.GraphLiteralSupport.CurrentFalconer.norm_linear_error_identityND line 22
  2. lemma OAI.GraphLiteralSupport.CurrentFalconer.norm_linear_errorND line 28
  3. lemma OAI.GraphLiteralSupport.CurrentFalconer.distance_linearizationND line 41
  4. lemma OAI.GraphLiteralSupport.CurrentFalconer.normalized_direction_distND line 57
  5. lemma OAI.GraphLiteralSupport.CurrentFalconer.projection_direction_changeND line 95
  6. theorem OAI.GraphLiteralSupport.CurrentFalconer.suffix_witness_local_collisionND line 111