OAI/MathematicalPhysics/RapidForcing/VelocitySyntax.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RapidForcing.ScaleData.δQ line 11
2. def OAI.RapidForcing.ScaleData.bQ line 12
3. lemma OAI.RapidForcing.ScaleData.cast_deltaQ line 13
4. lemma OAI.RapidForcing.ScaleData.cast_bQ line 14
5. def OAI.RapidForcing.EffectiveProfile.Formula.listSum line 21
6. def OAI.RapidForcing.EffectiveProfile.Formula.listProd line 22
7. lemma OAI.RapidForcing.EffectiveProfile.Formula.value_listSum line 23
8. lemma OAI.RapidForcing.EffectiveProfile.Formula.value_listProd line 28
9. def OAI.RapidForcing.EffectiveProfile.Formula.switch line 34
10. def OAI.RapidForcing.EffectiveProfile.Formula.theta line 35
11. def OAI.RapidForcing.EffectiveProfile.Formula.thetaDot line 36
12. lemma OAI.RapidForcing.EffectiveProfile.Formula.value_switch line 38
13. lemma OAI.RapidForcing.EffectiveProfile.Formula.value_theta line 41
14. lemma OAI.RapidForcing.EffectiveProfile.Formula.value_thetaDot line 43
15. def OAI.RapidForcing.EffectiveProfile.Formula.zeta line 52
16. lemma OAI.RapidForcing.EffectiveProfile.Formula.value_zeta line 55
17. def OAI.RapidForcing.EffectiveProfile.Formula.crossF line 60
18. lemma OAI.RapidForcing.EffectiveProfile.Formula.value_crossF line 64
19. def OAI.RapidForcing.EffectiveProfile.Formula.curlF line 70
20. lemma OAI.RapidForcing.EffectiveProfile.Formula.vectorField_curlF line 74
21. def OAI.RapidForcing.EffectiveProfile.Formula.moving line 81
22. lemma OAI.RapidForcing.EffectiveProfile.Formula.deriv_affine_theta line 89
23. lemma OAI.RapidForcing.EffectiveProfile.Formula.vectorField_moving line 93