OAI/NumberTheory/PiExponent/LocalAlgebra/Dimension.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiExponent.dimensionK line 17
  2. def OAI.PiExponent.dimensionW line 19
  3. def OAI.PiExponent.dimensionV line 21
  4. theorem OAI.PiExponent.dimensionK_le line 24
  5. theorem OAI.PiExponent.dimensionK_one_le line 28
  6. theorem OAI.PiExponent.dimensionW_pos line 32
  7. theorem OAI.PiExponent.dimensionV_pos line 36
  8. theorem OAI.PiExponent.dimension_volume line 44
  9. theorem OAI.PiExponent.dimensionK_div_W_le line 56
  10. theorem OAI.PiExponent.dimensionV_geometric_lower line 61
  11. theorem OAI.PiExponent.dimension_volume_lt_one line 72
  12. theorem OAI.PiExponent.dimension_error_le line 81
  13. theorem OAI.PiExponent.dimension_collision_identity line 100
  14. theorem OAI.PiExponent.tendsto_dimension_error_majorant line 116
  15. theorem OAI.PiExponent.tendsto_dimension_collision line 133
  16. theorem OAI.PiExponent.exists_dimension_margin line 143