OAI/MeasureTheory/Falconer/Geometry/SeededSeparation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Endpoint separation after a new inverse acts on existing jets

Both endpoint families keep all their original labels. Extracted scalar weights charge only the newly added derivative orders, including the complex angular multiplier when it is included as an extra label.

  1. abbrev OAI.Falconer.seededPairJets line 19
  2. def OAI.Falconer.seededJetSeparation line 23
  3. theorem OAI.Falconer.seededJetSeparation_left line 39
  4. theorem OAI.Falconer.seededJetSeparation_right line 49
  5. theorem OAI.Falconer.seededJetSeparation_exact line 58
  6. theorem OAI.Falconer.seededJetSeparation_card line 93
  7. theorem OAI.Falconer.seededJetSeparation_added_order line 103