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

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Joint smoothness of the actual scalar mild solution on the closed time slab.

  1. def OAI.ForcedComputation.PlaneScalarMild.CompatibleData.smoothCurves line 13
  2. theorem OAI.ForcedComputation.PlaneScalarMild.CompatibleData.solutionValue_smooth line 25

    Source documentation

    Norm-smooth time jets give joint smoothness, including the initial boundary.

    theorem solutionValue_smooth {T ν : ℝ} (hT : 0 < T) (hν : 0 < ν) (D : CompatibleData T)
    (hs : ∀ k, ContDiffOn ℝ ∞ (D.solutionJetValue hT.le hν k) (Icc (0 : ℝ) T)) :
    ContDiffOn ℝ ∞ (Function.uncurry (D.solutionValue hT.le hν))
      (Icc (0 : ℝ) T ×ˢ (univ : Set Plane)) := by
…

    Mentions: OAI.ForcedComputation.PlaneScalarMild.CompatibleData

  3. theorem OAI.ForcedComputation.PlaneScalarMild.CompatibleData.solutionValue_spatial_bounds line 36

    Source documentation

    Uniform bounds on any finite list of spatial derivative orders.

    theorem solutionValue_spatial_bounds {T ν : ℝ} (hT : 0 ≤ T) (hν : 0 < ν)
    (D : CompatibleData T) (n : ℕ) :
    ∃ B : ℝ, 0 ≤ B ∧ ∀ t ∈ Icc (0 : ℝ) T, ∀ k ≤ n, ∀ x,
      ‖iteratedFDeriv ℝ k (D.solutionValue hT hν t) x‖ ≤ B := by
…

    Mentions: OAI.ForcedComputation.PlaneScalarMild.CompatibleData