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

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The smooth planar processor theorem, assuming smooth dependence and the first two variational equations for the actual transition, expressed by PlanarVariations.

  1. def OAI.ForcedComputation.ProcessorFlowBounds line 18

    Source documentation

    Euclidean, rather than coordinate-maximum, norms are used in this clause.

    def ProcessorFlowBounds (V : ℝ → Plane → Plane) (Ψ : ℝ → ℝ → Plane → Plane)
    (L : ℕ) : Prop :=
…
  2. theorem OAI.ForcedComputation.periodic_zero_near_integers line 33
  3. def OAI.ForcedComputation.Recorder.Planar.processorHamiltonian line 48
  4. theorem OAI.ForcedComputation.Recorder.Planar.processorHamiltonian_joint_smooth line 52
  5. theorem OAI.ForcedComputation.Recorder.Planar.processorVelocity_joint_smooth line 67
  6. theorem OAI.ForcedComputation.Recorder.Planar.compact_normalizedInstruction_period line 87
  7. theorem OAI.ForcedComputation.Recorder.Planar.normalizedNeighborhood_ball line 103
  8. theorem OAI.ForcedComputation.Recorder.Planar.clockRectangle_in_unit line 123
  9. structure OAI.ForcedComputation.Recorder.Planar.ProcessorProperties line 130

    Source documentation

    All clauses of Theorem 3.1, with the two equivalent chart interpretations and the finite compiler data kept explicit.

    structure ProcessorProperties (I : Alternating.MachineInput) (hI : Alternating.ValidInput I)
    (Ω Ψ : ℝ → ℝ → Plane → Plane) : Prop where
…

    Mentions: OAI.Alternating.MachineInput, OAI.Alternating.ValidInput

  10. theorem OAI.ForcedComputation.Recorder.Planar.smooth_planar_processor line 204