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

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Classical scalar advection-diffusion on the flat two-torus.

Mantegazza and Martinazzi, A note on quasilinear parabolic equations on manifolds, Ann. Sc. Norm. Super. Pisa (5) 11 (2012), 857--874, Proposition 2.3 and Remark 2.4 (p. 861), specialized to the flat two-torus, second order, constant positive diffusion and a prescribed smooth drift. Finite-time coefficients can be extended with a time cutoff before applying the globally bounded-coefficient result.

  1. def OAI.ForcedComputation.VelocityDetector.scalarLaplacian line 20
  2. def OAI.ForcedComputation.VelocityDetector.scalarGenerator line 23
  3. structure OAI.ForcedComputation.VelocityDetector.TorusScalarSolution line 28

    Source documentation

    Smoothness and the actual scalar equation on a finite closed cylinder. The time derivative is one-sided at its two endpoints.

    structure TorusScalarSolution (T ν : ℝ) (a : ℝ → Plane → Plane)
    (h w : ℝ → Plane → ℝ) (w₀ : Plane → ℝ) : Prop where
…
  4. theorem OAI.ForcedComputation.VelocityDetector.TorusScalarSolution.slice_smooth line 37
  5. def OAI.ForcedComputation.VelocityDetector.TorusScalarExistence line 50

    Source documentation

    Classical existence for smooth periodic scalar advection-diffusion on a finite time cylinder.

    def TorusScalarExistence : Prop :=
…
  6. theorem OAI.ForcedComputation.VelocityDetector.scalarLaplacian_zero line 58
  7. theorem OAI.ForcedComputation.VelocityDetector.scalarGenerator_zero line 64
  8. theorem OAI.ForcedComputation.VelocityDetector.zero_solution line 68