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

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Directional derivatives commute with the actual Gaussian Volterra operators.

  1. def OAI.ForcedComputation.PlaneScalarMild.directionalPath line 15

    Source documentation

    Differentiate a continuous jet path pointwise.

    def directionalPath (k : ℕ) (v : Plane) (T : ℝ) :
    WeaklySingular.Path (Jet (k+1)) T →L[ℝ] WeaklySingular.Path (Jet k) T :=
…

    Mentions: OAI.ForcedComputation.WeaklySingular.Path, OAI.ForcedComputation.PlaneScalarMild.Jet

  2. theorem OAI.ForcedComputation.PlaneScalarMild.directionalPath_apply line 22
  3. theorem OAI.ForcedComputation.PlaneScalarMild.extendPath_directional line 26
  4. theorem OAI.ForcedComputation.PlaneScalarMild.rawHeatKernel_directional line 32
  5. theorem OAI.ForcedComputation.PlaneScalarMild.gradientKernel_directional line 43
  6. theorem OAI.ForcedComputation.PlaneScalarMild.rawKernels_directional line 55
  7. theorem OAI.ForcedComputation.PlaneScalarMild.rawKernelIntegral_directional line 63

    Source documentation

    Spatial differentiation passes through the actual singular time integral.

    theorem rawKernelIntegral_directional {T ν : ℝ} (hT : 0 ≤ T) (hν : 0 < ν)
    (k : ℕ) (v : Plane) (u : WeaklySingular.Path (Jet (k+1)) T)
    (i : Fin 3) (t : Icc (0 : ℝ) T) :
    BoundedSpatialJets.directionalDerivativeCLM Plane ℝ k v
      (∫ s in 0..t.val, rawKernels hν (k+1) i (t.val-s)
        (WeaklySingular.extendPath (Jet (k+1)) hT u s)) =
      ∫ s in 0..t.val, rawKernels hν k i (t.val-s)
        (WeaklySingular.extendPath (Jet k) hT (directionalPath k v T u) s) := by
…

    Mentions: OAI.ForcedComputation.WeaklySingular.Path, OAI.ForcedComputation.PlaneScalarMild.Jet, OAI.ForcedComputation.BoundedSpatialJets.directionalDerivativeCLM, OAI.ForcedComputation.PlaneScalarMild.rawKernels, OAI.ForcedComputation.WeaklySingular.extendPath, OAI.ForcedComputation.PlaneScalarMild.directionalPath

  8. theorem OAI.ForcedComputation.PlaneScalarMild.gradient_convolve_C1 line 77
  9. theorem OAI.ForcedComputation.PlaneScalarMild.gradientKernel_eq_heatDerivative line 96

    Source documentation

    On finite jets, a Gaussian gradient acting on the input equals heat acting on its derivative.

    theorem gradientKernel_eq_heatDerivative {ν : ℝ} (hν : 0 < ν) (k : ℕ)
    (j : Fin 2) (r : ℝ) (J : Jet (k+1)) :
    gradientKernel hν k j r (BoundedSpatialJets.truncateCLM Plane ℝ k (k+1) (by omega) J) =
      rawHeatKernel hν k r
        (BoundedSpatialJets.directionalDerivativeCLM Plane ℝ k (Pi.single j 1) J) := by
…

    Mentions: OAI.ForcedComputation.PlaneScalarMild.Jet, OAI.ForcedComputation.PlaneScalarMild.gradientKernel, OAI.ForcedComputation.BoundedSpatialJets.truncateCLM, OAI.ForcedComputation.PlaneScalarMild.rawHeatKernel, OAI.ForcedComputation.BoundedSpatialJets.directionalDerivativeCLM