OAI/MeasureTheory/Falconer/Angular/GnomonicPairGram.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Pair transversality retains the original affine separation

  1. def OAI.Falconer.pairGram line 11
  2. theorem OAI.Falconer.pairGram_nonneg line 14
  3. theorem OAI.Falconer.pairGram_smul line 20
  4. theorem OAI.Falconer.northLift_pairGram line 26
  5. theorem OAI.Falconer.gnomonic_pairGram line 34
  6. theorem OAI.Falconer.gnomonic_pairGram_lower line 39
  7. theorem OAI.Falconer.gnomonic_pair_separation line 57