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

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

A positive-determinant affine change of planar coordinates which places halting state bands below nonhalting bands and swaps reciprocal factors.

  1. def OAI.ForcedComputation.PlanarConjugacy.map line 15

    Source documentation

    The determinant of the linear part is ε * c.

    def map (a b ε c : ℚ) (x : Plane) : Plane :=
…
  2. def OAI.ForcedComputation.PlanarConjugacy.box line 19
  3. theorem OAI.ForcedComputation.PlanarConjugacy.box_positive line 24
  4. theorem OAI.ForcedComputation.PlanarConjugacy.box_center line 31
  5. theorem OAI.ForcedComputation.PlanarConjugacy.box_halfWidth line 36
  6. theorem OAI.ForcedComputation.PlanarConjugacy.mem_box_of_mem line 42
  7. theorem OAI.ForcedComputation.PlanarConjugacy.map_injective line 52
  8. theorem OAI.ForcedComputation.PlanarConjugacy.box_image line 69
  9. theorem OAI.ForcedComputation.PlanarConjugacy.norm_lower_bound line 100
  10. theorem OAI.ForcedComputation.PlanarConjugacy.separated_image line 135
  11. def OAI.ForcedComputation.PlanarConjugacy.instruction line 144
  12. theorem OAI.ForcedComputation.PlanarConjugacy.instruction_factor_pos line 147
  13. theorem OAI.ForcedComputation.PlanarConjugacy.instruction_conjugacy line 151
  14. theorem OAI.ForcedComputation.PlanarConjugacy.instruction_image_eq line 166