OAI/MathematicalPhysics/NavierStokes/ShearFlows/EffectiveProfiles.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ShearFlows.gluePower line 13
  2. theorem OAI.ShearFlows.gluePower_smooth line 15
  3. theorem OAI.ShearFlows.gluePower_deriv line 20
  4. theorem OAI.ShearFlows.gluePower_bound line 31
  5. def OAI.ShearFlows.transitionDen line 46
  6. theorem OAI.ShearFlows.transitionDen_ge line 48
  7. def OAI.ShearFlows.denomPower line 66
  8. theorem OAI.ShearFlows.transitionDen_pos line 68
  9. theorem OAI.ShearFlows.denomPower_smooth line 71
  10. theorem OAI.ShearFlows.transitionDen_deriv line 76
  11. theorem OAI.ShearFlows.denomPower_deriv line 85
  12. theorem OAI.ShearFlows.denomPower_bound line 96
  13. inductive OAI.ShearFlows.ProfileExpr line 103
  14. def OAI.ShearFlows.ProfileExpr.val line 114
  15. def OAI.ShearFlows.ProfileExpr.sub line 122
  16. def OAI.ShearFlows.ProfileExpr.diff line 124
  17. theorem OAI.ShearFlows.ProfileExpr.smooth line 134
  18. theorem OAI.ShearFlows.ProfileExpr.hasDerivAt line 143
  19. theorem OAI.ShearFlows.ProfileExpr.val_diff line 162
  20. def OAI.ShearFlows.ProfileExpr.diffN line 165
  21. theorem OAI.ShearFlows.ProfileExpr.val_diffN line 169
  22. def OAI.ShearFlows.ProfileExpr.bound line 174
  23. theorem OAI.ShearFlows.ProfileExpr.bound_nonneg line 182
  24. theorem OAI.ShearFlows.ProfileExpr.val_bound line 185
  25. def OAI.ShearFlows.ProfileExpr.transition line 198
  26. def OAI.ShearFlows.ProfileExpr.ramp line 199
  27. def OAI.ShearFlows.ProfileExpr.cutoff line 200
  28. def OAI.ShearFlows.ProfileExpr.potential line 202
  29. theorem OAI.ShearFlows.ProfileExpr.val_transition line 205
  30. theorem OAI.ShearFlows.ProfileExpr.val_ramp line 209
  31. theorem OAI.ShearFlows.ProfileExpr.val_cutoff line 217
  32. theorem OAI.ShearFlows.ProfileExpr.val_potential line 225