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

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The scalar PDE holds as an ODE between successive finite spatial-jet spaces.

  1. def OAI.ForcedComputation.PlaneScalarMild.laplacianJetCLM line 13
  2. theorem OAI.ForcedComputation.PlaneScalarMild.function_laplacianJetCLM line 17
  3. def OAI.ForcedComputation.PlaneScalarMild.CompatibleData.solutionJetValue line 41
  4. def OAI.ForcedComputation.PlaneScalarMild.CompatibleData.timeRHSJet line 44
  5. theorem OAI.ForcedComputation.PlaneScalarMild.CompatibleData.solutionJetValue_continuous line 49
  6. theorem OAI.ForcedComputation.PlaneScalarMild.CompatibleData.timeRHSJet_continuous line 53
  7. theorem OAI.ForcedComputation.PlaneScalarMild.CompatibleData.solutionJetValue_function line 58
  8. theorem OAI.ForcedComputation.PlaneScalarMild.CompatibleData.timeRHSJet_function line 65
  9. theorem OAI.ForcedComputation.PlaneScalarMild.CompatibleData.solutionJetValue_hasDerivWithinAt line 78

    Source documentation

    The time derivative exists in the full jet norm, including the two endpoints.

    theorem solutionJetValue_hasDerivWithinAt {T ν : ℝ} (hT : 0 ≤ T) (hν : 0 < ν)
    (D : CompatibleData T) (k : ℕ) {t : ℝ} (ht : t ∈ Icc (0 : ℝ) T) :
    HasDerivWithinAt (D.solutionJetValue hT hν k) (D.timeRHSJet hT hν k t)
      (Icc (0 : ℝ) T) t := by
…

    Mentions: OAI.ForcedComputation.PlaneScalarMild.CompatibleData