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

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ForcedComputation.PlaneScalarMild.multiplication_contDiffOn line 14
2. theorem OAI.ForcedComputation.PlaneScalarMild.path_add_eval line 32
3. theorem OAI.ForcedComputation.PlaneScalarMild.path_sum_eval line 36
4. theorem OAI.ForcedComputation.PlaneScalarMild.path_three_eval line 43
5. def OAI.ForcedComputation.PlaneScalarMild.CompatibleData.sourceJetValue line 52
6. def OAI.ForcedComputation.PlaneScalarMild.CompatibleData.coefficientJetValue line 55
7. theorem OAI.ForcedComputation.PlaneScalarMild.CompatibleData.effectiveSourceJet_formula line 59
8. theorem OAI.ForcedComputation.PlaneScalarMild.CompatibleData.effectiveSourceJet_contDiffOn line 84
9. theorem OAI.ForcedComputation.PlaneScalarMild.CompatibleData.solutionJetValue_smooth_time line 105

   Source documentation

   Smooth source and coefficient curves make every finite spatial jet smooth in time.

   theorem solutionJetValue_smooth_time {T ν : ℝ} (hT : 0 < T) (hν : 0 < ν)
       (D : CompatibleData T)
       (hs : ∀ k, ContDiffOn ℝ ∞ (WeaklySingular.extendPath (Jet k) hT.le (D.source k))
         (Icc (0 : ℝ) T))
       (hb : ∀ k i, ContDiffOn ℝ ∞ (CoefficientTimeJets.extend hT.le (D.coefficient k i))
         (Icc (0 : ℝ) T)) (k : ℕ) :
       ContDiffOn ℝ ∞ (D.solutionJetValue hT.le hν k) (Icc (0 : ℝ) T) := by
   …

   Mentions: OAI.ForcedComputation.PlaneScalarMild.CompatibleData, OAI.ForcedComputation.WeaklySingular.extendPath, OAI.ForcedComputation.PlaneScalarMild.Jet, OAI.ForcedComputation.CoefficientTimeJets.extend

10. theorem OAI.ForcedComputation.PlaneScalarMild.CompatibleData.periodic_solutionJetValue_smooth_time line 132

    Source documentation

    The periodic data supplied by the compiler satisfy the time-smoothness hypotheses.

    theorem periodic_solutionJetValue_smooth_time {T ν : ℝ} (hT : 0 < T) (hν : 0 < ν)
        (D : CompatibleData T) {h : ℝ × Plane → ℝ} (hh : ContDiff ℝ ∞ h)
        (hph : ∀ t, PlanePeriodic (fun x => h (t,x)))
        {b : Fin 3 → ℝ × Plane → ℝ} (hbs : ∀ i, ContDiff ℝ ∞ (b i))
        (hpb : ∀ i t, PlanePeriodic (fun x => b i (t,x)))
        (hsource : ∀ k t x, BoundedSpatialJets.function Plane ℝ k (D.source k t) x = h (t.val,x))
        (hcoeff : ∀ k i t x, BoundedSpatialJets.function Plane ℝ k (D.coefficient k i t) x = b i (t.val,x))
        (k : ℕ) : ContDiffOn ℝ ∞ (D.solutionJetValue hT.le hν k) (Icc (0 : ℝ) T) := by
    …

    Mentions: OAI.ForcedComputation.PlaneScalarMild.CompatibleData, OAI.ForcedComputation.PlanePeriodic, OAI.ForcedComputation.BoundedSpatialJets.function

11. theorem OAI.ForcedComputation.PlaneScalarMild.CompatibleData.supported_solutionJetValue_smooth_time line 149

    Source documentation

    A common compact support gives the same smoothness for the whole-plane data.

    theorem supported_solutionJetValue_smooth_time {T ν : ℝ} (hT : 0 < T) (hν : 0 < ν)
        (D : CompatibleData T) {K : Set Plane} (hK : IsCompact K)
        {h : ℝ × Plane → ℝ} (hh : ContDiff ℝ ∞ h)
        (hsh : ∀ t ∈ Icc (0 : ℝ) T, ∀ x ∉ K, h (t,x) = 0)
        {b : Fin 3 → ℝ × Plane → ℝ} (hbs : ∀ i, ContDiff ℝ ∞ (b i))
        (hsb : ∀ i t, t ∈ Icc (0 : ℝ) T → ∀ x ∉ K, b i (t,x) = 0)
        (hsource : ∀ k t x, BoundedSpatialJets.function Plane ℝ k (D.source k t) x = h (t.val,x))
        (hcoeff : ∀ k i t x, BoundedSpatialJets.function Plane ℝ k (D.coefficient k i t) x = b i (t.val,x))
        (k : ℕ) : ContDiffOn ℝ ∞ (D.solutionJetValue hT.le hν k) (Icc (0 : ℝ) T) := by
    …

    Mentions: OAI.ForcedComputation.PlaneScalarMild.CompatibleData, OAI.ForcedComputation.BoundedSpatialJets.function