OAI/Geometry/TranslativeCovering/RadialShell.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RadialShell.η line 19
  2. def OAI.RadialShell.low line 20
  3. def OAI.RadialShell.high line 21
  4. lemma OAI.RadialShell.inv_limit line 23
  5. lemma OAI.RadialShell.eta_limit line 25
  6. lemma OAI.RadialShell.log_div_limit line 28
  7. lemma OAI.RadialShell.low_limit line 32
  8. lemma OAI.RadialShell.high_limit line 35
  9. lemma OAI.RadialShell.n_eta line 39
  10. lemma OAI.RadialShell.thresholds line 49
  11. lemma OAI.RadialShell.weight_upper line 79