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

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Fixed linear maps and directional derivatives on bounded spatial jets.

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

    Source documentation

    Postcomposition acts boundedly on every derivative in a finite jet.

    def postcompose (k : ℕ) (L : F →L[ℝ] G) (J : Space E F k) : Space E G k :=
…

    Mentions: OAI.ForcedComputation.BoundedSpatialJets.Space

  2. theorem OAI.ForcedComputation.BoundedSpatialJets.function_postcompose line 25
  3. theorem OAI.ForcedComputation.BoundedSpatialJets.norm_postcompose_le line 29
  4. def OAI.ForcedComputation.BoundedSpatialJets.postcomposeCLM line 34

    Source documentation

    Apply one fixed bounded linear map to a jet-valued function.

    def postcomposeCLM (k : ℕ) (L : F →L[ℝ] G) : Space E F k →L[ℝ] Space E G k :=
…

    Mentions: OAI.ForcedComputation.BoundedSpatialJets.Space

  5. theorem OAI.ForcedComputation.BoundedSpatialJets.postcomposeCLM_apply line 49
  6. theorem OAI.ForcedComputation.BoundedSpatialJets.norm_postcomposeCLM_le line 52
  7. theorem OAI.ForcedComputation.BoundedSpatialJets.postcomposeCLM_truncate line 56
  8. theorem OAI.ForcedComputation.BoundedSpatialJets.norm_evaluation_le line 67
  9. def OAI.ForcedComputation.BoundedSpatialJets.directionalDerivativeCLM line 74

    Source documentation

    One directional derivative loses one order and has norm at most the direction norm.

    def directionalDerivativeCLM (k : ℕ) (v : E) : Space E F (k+1) →L[ℝ] Space E F k :=
…

    Mentions: OAI.ForcedComputation.BoundedSpatialJets.Space

  10. theorem OAI.ForcedComputation.BoundedSpatialJets.function_directionalDerivativeCLM line 79
  11. theorem OAI.ForcedComputation.BoundedSpatialJets.norm_directionalDerivativeCLM_le line 89
  12. theorem OAI.ForcedComputation.BoundedSpatialJets.directionalDerivativeCLM_truncate line 101