OAI/MathematicalPhysics/NavierStokes/ShearFlows/Masks.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ShearFlows.cube_integral_prod line 14
  2. theorem OAI.ShearFlows.cube_integral_three line 21
  3. theorem OAI.ShearFlows.circleMask_setIntegral_zero line 27
  4. theorem OAI.ShearFlows.planarMask_cube_mean_zero line 33
  5. def OAI.ShearFlows.Input.horizontalBox line 49
  6. def OAI.ShearFlows.Input.horizontalRadius line 51
  7. def OAI.ShearFlows.Input.sourceMask line 54
  8. def OAI.ShearFlows.Input.targetMask line 57
  9. def OAI.ShearFlows.Input.heightMask line 60
  10. def OAI.ShearFlows.Input.horizontalProfile line 66
  11. theorem OAI.ShearFlows.horizontalRadius_pos line 76
  12. theorem OAI.ShearFlows.horizontal_collars_inside line 84
  13. theorem OAI.ShearFlows.sourceMask_smooth line 94
  14. theorem OAI.ShearFlows.targetMask_smooth line 98
  15. theorem OAI.ShearFlows.heightMask_smooth line 102
  16. theorem OAI.ShearFlows.heightMask_periodic line 108
  17. theorem OAI.ShearFlows.heightMask_integral_zero line 111
  18. theorem OAI.ShearFlows.horizontalProfile_periodic line 118
  19. theorem OAI.ShearFlows.horizontalProfile_smooth line 121
  20. theorem OAI.ShearFlows.horizontalProfile_eq line 128
  21. theorem OAI.ShearFlows.heightMask_near_privateHeight line 153