OAI/Geometry/PolarProducts/LensBounds.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PlanarLens.exists_inner_bound line 39
  2. theorem OAI.PlanarLens.exists_uniform_error_bound line 84
  3. theorem OAI.PlanarLens.J_div_order line 126
  4. theorem OAI.PlanarLens.rho_neg line 132
  5. def OAI.PlanarLens.excess line 138
  6. def OAI.PlanarLens.epsilon line 140
  7. theorem OAI.PlanarLens.epsilon_nonneg line 142
  8. theorem OAI.PlanarLens.exists_excess_bound line 144
  9. theorem OAI.PlanarLens.bddAbove_excess line 166
  10. theorem OAI.PlanarLens.excess_le_epsilon line 172
  11. theorem OAI.PlanarLens.epsilon_le_of_excess_le line 175
  12. theorem OAI.PlanarLens.tendsto_inner_error line 182
  13. theorem OAI.PlanarLens.exists_small_tail line 198
  14. theorem OAI.PlanarLens.tendsto_epsilon line 217
  15. theorem OAI.PlanarLens.uniform_slice line 233