OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Programs/IntermediateObservation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The finite shear program cannot produce an observation between safe endpoints.

  1. theorem OAI.ShearFlows.RationalBox.coordinate_le_center_add_halfWidth line 12
  2. theorem OAI.ShearFlows.RationalBox.center_sub_halfWidth_le_coordinate line 18
  3. theorem OAI.ShearFlows.branchNodes_first_le line 24
  4. theorem OAI.ShearFlows.branchNodes_first_ge line 57
  5. theorem OAI.ShearFlows.exists_block_of_mem line 90
  6. theorem OAI.ShearFlows.materialFlow_first_le line 106
  7. theorem OAI.ShearFlows.materialFlow_first_ge line 131