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

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Fixed spatial translations on finite bounded jets, including convolution covariance.

  1. def OAI.ForcedComputation.BoundedSpatialJets.translation line 17

    Source documentation

    A fixed translation does not increase any derivative norm.

    def translation (k : ℕ) (a : E) (J : Space E F k) : Space E F k :=
…

    Mentions: OAI.ForcedComputation.BoundedSpatialJets.Space

  2. theorem OAI.ForcedComputation.BoundedSpatialJets.function_translation line 24
  3. theorem OAI.ForcedComputation.BoundedSpatialJets.norm_translation_le line 28
  4. def OAI.ForcedComputation.BoundedSpatialJets.translationCLM line 32
  5. theorem OAI.ForcedComputation.BoundedSpatialJets.translationCLM_apply line 49
  6. theorem OAI.ForcedComputation.BoundedSpatialJets.translation_eq_self line 52
  7. theorem OAI.ForcedComputation.BoundedSpatialJets.translation_convolution line 64