OAI/MathematicalPhysics/RapidForcing/ScaledSyntax.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RapidForcing.EffectiveProfile.Formula.spIndex line 11
  2. def OAI.RapidForcing.EffectiveProfile.Formula.etaIndex line 12
  3. def OAI.RapidForcing.EffectiveProfile.Formula.xiIndex line 13
  4. def OAI.RapidForcing.EffectiveProfile.Formula.profileLinear line 15
  5. def OAI.RapidForcing.EffectiveProfile.Formula.profileParams line 20
  6. def OAI.RapidForcing.EffectiveProfile.Formula.profilePack line 22
  7. lemma OAI.RapidForcing.EffectiveProfile.Formula.profilePack_eq line 25
  8. lemma OAI.RapidForcing.EffectiveProfile.Formula.profileLinear_norm line 30
  9. lemma OAI.RapidForcing.EffectiveProfile.Formula.profilePack_line line 43
  10. def OAI.RapidForcing.EffectiveProfile.Formula.profileField line 48
  11. lemma OAI.RapidForcing.EffectiveProfile.Formula.profileField_smooth line 50
  12. lemma OAI.RapidForcing.EffectiveProfile.Formula.profile_partial line 56
  13. def OAI.RapidForcing.EffectiveProfile.Formula.profileCurl line 75
  14. lemma OAI.RapidForcing.EffectiveProfile.Formula.profileCurl_value line 79
  15. def OAI.RapidForcing.EffectiveProfile.Formula.scaledFormula line 91
  16. lemma OAI.RapidForcing.EffectiveProfile.Formula.scaledFormula_value line 97
  17. def OAI.RapidForcing.EffectiveProfile.Formula.curlJetBound line 125
  18. lemma OAI.RapidForcing.EffectiveProfile.Formula.curlJetBound_nonneg line 127
  19. lemma OAI.RapidForcing.EffectiveProfile.Formula.norm_jet_affine_le line 130
  20. lemma OAI.RapidForcing.EffectiveProfile.Formula.curlJetBound_spec line 146