OAI/MathematicalPhysics/NavierStokes/ShearFlows/Construction.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ShearFlows.Input.planarLower line 16
  2. def OAI.ShearFlows.Input.planarUpper line 17
  3. def OAI.ShearFlows.Input.sources line 18
  4. def OAI.ShearFlows.Input.targets line 20
  5. def OAI.ShearFlows.Input.sourceRadius line 22
  6. def OAI.ShearFlows.Input.targetRadius line 23
  7. def OAI.ShearFlows.Input.heightSpacing line 25
  8. def OAI.ShearFlows.Input.privateHeight line 28
  9. def OAI.ShearFlows.Input.heightRadius line 31
  10. theorem OAI.ShearFlows.boxChartGap_pos_of_inChart line 35
  11. theorem OAI.ShearFlows.sourceRadius_pos line 49
  12. theorem OAI.ShearFlows.targetRadius_pos line 58
  13. theorem OAI.ShearFlows.heightSpacing_pos line 67
  14. theorem OAI.ShearFlows.privateHeight_collars_inside line 70
  15. theorem OAI.ShearFlows.privateHeight_order line 85
  16. theorem OAI.ShearFlows.privateHeight_collars_disjoint line 94
  17. def OAI.ShearFlows.circleCutoff line 113
  18. theorem OAI.ShearFlows.circleCutoff_smooth line 115
  19. theorem OAI.ShearFlows.circleCutoff_periodic line 120
  20. theorem OAI.ShearFlows.circleCutoff_eq_in_chart line 123
  21. theorem OAI.ShearFlows.circleCutoff_plateau line 132
  22. theorem OAI.ShearFlows.circleCutoff_zero_in_chart line 140
  23. def OAI.ShearFlows.planarMask line 148
  24. theorem OAI.ShearFlows.planarMask_smooth line 156
  25. theorem OAI.ShearFlows.planarMask_periodic line 163
  26. theorem OAI.ShearFlows.planarMask_plateau line 171
  27. theorem OAI.ShearFlows.planarMask_zero_in_chart line 184
  28. theorem OAI.ShearFlows.near_box_inside_plateau line 205
  29. theorem OAI.ShearFlows.familyMask_near line 214
  30. theorem OAI.ShearFlows.sourceMask_near_box line 241
  31. theorem OAI.ShearFlows.targetMask_near_box line 249