OAI/MathematicalPhysics/RapidForcing/EffectiveProfiles.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.RapidForcing.EffectiveProfile.GluePoly line 13
  2. def OAI.RapidForcing.EffectiveProfile.glueDiff line 15
  3. def OAI.RapidForcing.EffectiveProfile.glueBound line 19
  4. def OAI.RapidForcing.EffectiveProfile.monoGlue line 23
  5. def OAI.RapidForcing.EffectiveProfile.glue line 25
  6. lemma OAI.RapidForcing.EffectiveProfile.glueBound_nonneg line 29
  7. lemma OAI.RapidForcing.EffectiveProfile.hasDerivAt_monoGlue line 34
  8. lemma OAI.RapidForcing.EffectiveProfile.hasDerivAt_glue line 44
  9. lemma OAI.RapidForcing.EffectiveProfile.contDiff_glue line 54
  10. lemma OAI.RapidForcing.EffectiveProfile.pow_mul_exp_neg_le line 65
  11. lemma OAI.RapidForcing.EffectiveProfile.abs_monoGlue_le line 75
  12. lemma OAI.RapidForcing.EffectiveProfile.abs_glue_le line 84
  13. lemma OAI.RapidForcing.EffectiveProfile.glue_one line 94
  14. lemma OAI.RapidForcing.EffectiveProfile.denominator_lower line 98
  15. inductive OAI.RapidForcing.EffectiveProfile.Expr line 114
  16. def OAI.RapidForcing.EffectiveProfile.Expr.value line 122
  17. def OAI.RapidForcing.EffectiveProfile.Expr.bound line 130
  18. def OAI.RapidForcing.EffectiveProfile.Expr.diff line 138
  19. lemma OAI.RapidForcing.EffectiveProfile.Expr.bound_nonneg line 148
  20. lemma OAI.RapidForcing.EffectiveProfile.Expr.abs_value_le line 157
  21. lemma OAI.RapidForcing.EffectiveProfile.Expr.hasDerivAt line 176
  22. lemma OAI.RapidForcing.EffectiveProfile.Expr.contDiff line 210
  23. lemma OAI.RapidForcing.EffectiveProfile.Expr.lipschitz line 222
  24. def OAI.RapidForcing.EffectiveProfile.switchExpr line 230
  25. lemma OAI.RapidForcing.EffectiveProfile.switchExpr_value line 233