OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Scalar/ScalarGlobalExistence.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Consistent finite-cylinder solutions give one scalar evolution for all nonnegative time, with compatibility supplied by uniqueness.

  1. theorem OAI.ForcedComputation.VelocityDetector.TorusScalarSolution.restrict line 13
  2. theorem OAI.ForcedComputation.VelocityDetector.TorusScalarSolution.congr line 23
  3. def OAI.ForcedComputation.VelocityDetector.GlobalTorusScalarSolution line 38

    Source documentation

    Smoothness and the equation on every finite closed time cylinder.

    def GlobalTorusScalarSolution (ν : ℝ) (a : ℝ → Plane → Plane)
    (h w : ℝ → Plane → ℝ) (w₀ : Plane → ℝ) : Prop :=
…
  4. theorem OAI.ForcedComputation.VelocityDetector.TorusScalarExistence.global line 42
  5. theorem OAI.ForcedComputation.VelocityDetector.GlobalTorusScalarSolution.nonnegative line 69
  6. theorem OAI.ForcedComputation.VelocityDetector.GlobalTorusScalarSolution.unique line 77