OAI/NumberTheory/PiExponent/Approximation/WeightedGeometryScale.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PiExponent.WeightedGeometryScale.exists_power_scale line 10
  2. theorem OAI.PiExponent.WeightedGeometryScale.exists_common_scale line 25
  3. def OAI.PiExponent.WeightedGeometryScale.monomials line 42
  4. theorem OAI.PiExponent.WeightedGeometryScale.mem_monomials line 45
  5. theorem OAI.PiExponent.WeightedGeometryScale.zero_mem_monomials line 59
  6. theorem OAI.PiExponent.WeightedGeometryScale.pure_mem_monomials line 64
  7. theorem OAI.PiExponent.WeightedGeometryScale.coordinate_mem_monomials line 71
  8. theorem OAI.PiExponent.WeightedGeometryScale.exists_log_cutoff line 81
  9. structure OAI.PiExponent.WeightedGeometryScale.Scale line 88
  10. def OAI.PiExponent.WeightedGeometryScale.chooseScale line 98
  11. abbrev OAI.PiExponent.WeightedGeometryScale.Scale.Index line 107
  12. def OAI.PiExponent.WeightedGeometryScale.Scale.exponents line 109
  13. def OAI.PiExponent.WeightedGeometryScale.Scale.constantIndex line 111
  14. def OAI.PiExponent.WeightedGeometryScale.Scale.coordinateIndex line 114
  15. def OAI.PiExponent.WeightedGeometryScale.Scale.pureIndex line 118
  16. theorem OAI.PiExponent.WeightedGeometryScale.Scale.exponents_constant line 122
  17. theorem OAI.PiExponent.WeightedGeometryScale.Scale.exponents_coordinate line 125
  18. theorem OAI.PiExponent.WeightedGeometryScale.Scale.exponents_pure line 128
  19. theorem OAI.PiExponent.WeightedGeometryScale.Scale.budget line 131