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

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Joint smoothness and periodicity of spatial derivatives with a time parameter.

  1. def OAI.ForcedComputation.spatialParameterDerivative line 16

    Source documentation

    Restrict the total derivative to spatial directions.

    def spatialParameterDerivative (n : ℕ) (f : ℝ × Plane → F) (p : ℝ × Plane) :
    ContinuousMultilinearMap ℝ (fun _ : Fin n => Plane) F :=
…
  2. theorem OAI.ForcedComputation.spatialParameterDerivative_eq line 21
  3. theorem OAI.ForcedComputation.spatialParameterDerivative_smooth line 32
  4. theorem OAI.ForcedComputation.planePeriodic_iteratedFDeriv line 38