OAI/MathematicalPhysics/RapidForcing/QuantitativeDecay.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RapidForcing.addressCurl_jetBound line 10
  2. lemma OAI.RapidForcing.stepVelocity_jetBound line 49
  3. lemma OAI.RapidForcing.ScaleData.s_quadratic_lower line 91
  4. lemma OAI.RapidForcing.ScaleData.coefficient_tail_bound line 100
  5. def OAI.RapidForcing.ScaleData.coefficientBound line 119
  6. lemma OAI.RapidForcing.ScaleData.coefficientBound_nonneg line 122
  7. lemma OAI.RapidForcing.ScaleData.coefficient_sum_le line 131
  8. lemma OAI.RapidForcing.loadingVelocity_jetBound line 157
  9. lemma OAI.RapidForcing.loadingVelocity_weighted_jetBound line 179
  10. lemma OAI.RapidForcing.stepVelocity_weighted_jetBound line 197
  11. def OAI.RapidForcing.velocityJetBound line 217
  12. lemma OAI.RapidForcing.velocityJetBound_nonneg line 220
  13. lemma OAI.RapidForcing.addressedVelocity_weighted_jetBound line 224