OAI/Analysis/SolenoidalShears/Affine.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Four affine shears, intermediate excursion bounds and endpoint identities.

  1. abbrev OAI.Solenoidal.Shear.Plane line 9
  2. def OAI.Solenoidal.Shear.X line 11
  3. def OAI.Solenoidal.Shear.Y line 12
  4. def OAI.Solenoidal.Shear.endpoint line 15
  5. def OAI.Solenoidal.Shear.partialStage line 21
  6. def OAI.Solenoidal.Shear.interpolate line 29
  7. theorem OAI.Solenoidal.Shear.partialStage_interpolate line 33
  8. theorem OAI.Solenoidal.Shear.endpoint_one line 38
  9. theorem OAI.Solenoidal.Shear.endpoint_two line 42
  10. theorem OAI.Solenoidal.Shear.endpoint_three line 46
  11. theorem OAI.Solenoidal.Shear.four_shears line 51
  12. theorem OAI.Solenoidal.Shear.middle_term_bound line 56
  13. theorem OAI.Solenoidal.Shear.endpoint_bound line 71
  14. theorem OAI.Solenoidal.Shear.abs_interpolate_le line 105
  15. theorem OAI.Solenoidal.Shear.excursion line 117
  16. theorem OAI.Solenoidal.Shear.partialStage_zero line 132
  17. theorem OAI.Solenoidal.Shear.partialStage_one line 137