OAI/MathematicalPhysics/NavierStokes/ShearFlows/Extension.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ShearFlows.periodize line 13
  2. theorem OAI.ShearFlows.periodize_periodic line 16
  3. theorem OAI.ShearFlows.periodize_local_sum line 31
  4. theorem OAI.ShearFlows.periodize_smooth line 57
  5. theorem OAI.ShearFlows.periodize_eq_in_chart line 70
  6. theorem OAI.ShearFlows.periodic_deriv line 85
  7. theorem OAI.ShearFlows.periodic_deriv_integral_zero line 92
  8. theorem OAI.ShearFlows.closedCutoff_support line 102
  9. theorem OAI.ShearFlows.maskPotential_support line 108
  10. theorem OAI.ShearFlows.derivativeMask_support line 116
  11. def OAI.ShearFlows.circleMask line 120
  12. theorem OAI.ShearFlows.circleMask_smooth line 123
  13. theorem OAI.ShearFlows.circleMask_periodic line 129
  14. theorem OAI.ShearFlows.circleMask_integral_zero line 133
  15. theorem OAI.ShearFlows.circleMask_eq_in_chart line 141
  16. theorem OAI.ShearFlows.circleMask_plateau line 153
  17. theorem OAI.ShearFlows.circleMask_zero_in_chart line 161
  18. theorem OAI.ShearFlows.smoothPulse_support line 169
  19. def OAI.ShearFlows.periodPulse line 175
  20. theorem OAI.ShearFlows.periodPulse_periodic line 178
  21. theorem OAI.ShearFlows.periodPulse_smooth line 181
  22. theorem OAI.ShearFlows.periodPulse_eq_on_period line 187
  23. theorem OAI.ShearFlows.periodPulses_separated line 198
  24. theorem OAI.ShearFlows.periodPulse_nonneg line 211
  25. theorem OAI.ShearFlows.periodPulse_integral line 216
  26. theorem OAI.ShearFlows.periodPulses_vanish_near_integers line 233