OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Scalar/PlaneScalarGlobal.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.PlaneScalarSolution.restrict line 13
  2. theorem OAI.ForcedComputation.VelocityDetector.PlaneScalarSolution.congr line 23
  3. def OAI.ForcedComputation.VelocityDetector.GlobalPlaneScalarSolution line 39

    Source documentation

    Bounded smooth solutions on every finite closed time cylinder.

    def GlobalPlaneScalarSolution (ν : ℝ) (a : ℝ → Plane → Plane)
    (h w : ℝ → Plane → ℝ) : Prop := ∀ T, 0 ≤ T → PlaneScalarSolution T ν a h w

    Mentions: OAI.ForcedComputation.VelocityDetector.PlaneScalarSolution

  4. theorem OAI.ForcedComputation.VelocityDetector.PlaneScalarExistence.global line 42
  5. theorem OAI.ForcedComputation.VelocityDetector.GlobalPlaneScalarSolution.nonnegative line 67
  6. theorem OAI.ForcedComputation.VelocityDetector.GlobalPlaneScalarSolution.unique line 75