OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Flow/PlanarNeighborhood.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The computed period map agrees with each branch's affine map on an explicit positive open neighborhood of its entire closed source rectangle.

  1. theorem OAI.ForcedComputation.Recorder.Planar.branchNeighborhood_open line 14
  2. theorem OAI.ForcedComputation.Recorder.Planar.normalized_branch_near_period line 23
  3. theorem OAI.ForcedComputation.Recorder.Planar.normalized_branch_neighborhood_period line 45