OAI/MathematicalPhysics/NavierStokes/ShearFlows/Affine.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ShearFlows.shearX line 10
  2. def OAI.ShearFlows.shearY line 11
  3. def OAI.ShearFlows.scalingEndpoints line 13
  4. def OAI.ShearFlows.partialShear line 20
  5. theorem OAI.ShearFlows.four_shears line 24
  6. theorem OAI.ShearFlows.partial_shear_is_segment line 30
  7. theorem OAI.ShearFlows.reciprocal_correction_bound line 40
  8. theorem OAI.ShearFlows.norm_segment_le line 53
  9. theorem OAI.ShearFlows.scaling_endpoints_bound line 67
  10. theorem OAI.ShearFlows.excursion line 83
  11. theorem OAI.ShearFlows.RationalBox.mem_iff_abs_sub_center_le line 99
  12. theorem OAI.ShearFlows.instruction_offset_bounds line 118
  13. def OAI.ShearFlows.scalingStage line 135
  14. theorem OAI.ShearFlows.scalingStage_bound line 139
  15. theorem OAI.ShearFlows.scaledOffset_bound line 150
  16. theorem OAI.ShearFlows.center_segment_mem line 163
  17. theorem OAI.ShearFlows.within_margin_in_planar_chart line 182
  18. theorem OAI.ShearFlows.scalingStage_in_chart line 195
  19. theorem OAI.ShearFlows.translation_in_chart line 203
  20. def OAI.ShearFlows.prefixBound line 214
  21. theorem OAI.ShearFlows.prefixBound_ge_one line 216
  22. theorem OAI.ShearFlows.scalingEndpoints_sub line 221
  23. theorem OAI.ShearFlows.scalingEndpoints_lipschitz line 227
  24. theorem OAI.ShearFlows.scalingStage_lipschitz line 258
  25. theorem OAI.ShearFlows.prefixBound_rational line 279
  26. theorem OAI.ShearFlows.scalingStage_start line 283
  27. theorem OAI.ShearFlows.scalingStage_finish line 290
  28. theorem OAI.ShearFlows.affine_eq_target_add_scaledOffset line 297
  29. theorem OAI.ShearFlows.scaling_final_endpoint line 302