OAI/MathematicalPhysics/RapidForcing/RationalProfiles.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.RapidForcing.EffectiveProfile.Ball line 11
  2. def OAI.RapidForcing.EffectiveProfile.Ball.exact line 16
  3. def OAI.RapidForcing.EffectiveProfile.Ball.add line 17
  4. def OAI.RapidForcing.EffectiveProfile.Ball.mul line 18
  5. def OAI.RapidForcing.EffectiveProfile.Ball.pow line 22
  6. def OAI.RapidForcing.EffectiveProfile.Ball.denInv line 26
  7. def OAI.RapidForcing.EffectiveProfile.Ball.Covers line 29
  8. lemma OAI.RapidForcing.EffectiveProfile.Ball.Covers.radius_nonneg line 31
  9. lemma OAI.RapidForcing.EffectiveProfile.Ball.covers_exact line 34
  10. lemma OAI.RapidForcing.EffectiveProfile.Ball.Covers.add line 37
  11. lemma OAI.RapidForcing.EffectiveProfile.Ball.Covers.mul line 46
  12. lemma OAI.RapidForcing.EffectiveProfile.Ball.Covers.pow line 67
  13. lemma OAI.RapidForcing.EffectiveProfile.clamp_dist line 73
  14. lemma OAI.RapidForcing.EffectiveProfile.Ball.Covers.denInv line 81
  15. def OAI.RapidForcing.EffectiveProfile.Encloses line 100
  16. lemma OAI.RapidForcing.EffectiveProfile.Encloses.centers line 103
  17. lemma OAI.RapidForcing.EffectiveProfile.encloses_exact line 108
  18. lemma OAI.RapidForcing.EffectiveProfile.Encloses.add line 111
  19. lemma OAI.RapidForcing.EffectiveProfile.Encloses.mul line 115
  20. lemma OAI.RapidForcing.EffectiveProfile.Encloses.pow line 121
  21. lemma OAI.RapidForcing.EffectiveProfile.Encloses.denInv line 127
  22. def OAI.RapidForcing.EffectiveProfile.expTerms line 131
  23. def OAI.RapidForcing.EffectiveProfile.expBall line 133
  24. lemma OAI.RapidForcing.EffectiveProfile.expTerms_large line 138
  25. lemma OAI.RapidForcing.EffectiveProfile.expBall_covers line 148
  26. lemma OAI.RapidForcing.EffectiveProfile.expBall_encloses line 161
  27. def OAI.RapidForcing.EffectiveProfile.monoBall line 168
  28. def OAI.RapidForcing.EffectiveProfile.glueBall line 172
  29. lemma OAI.RapidForcing.EffectiveProfile.monoBall_encloses line 176
  30. lemma OAI.RapidForcing.EffectiveProfile.glueBall_encloses line 186
  31. def OAI.RapidForcing.EffectiveProfile.Expr.numeric line 193
  32. lemma OAI.RapidForcing.EffectiveProfile.Expr.numeric_encloses line 202
  33. def OAI.RapidForcing.EffectiveProfile.Expr.numericError line 216
  34. lemma OAI.RapidForcing.EffectiveProfile.Expr.numeric_error_le line 219