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

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Bounded operators needed for the finite-order Volterra equation: fixed-coefficient multiplication, lossless truncation, and one spatial derivative.

  1. theorem OAI.ForcedComputation.BoundedSpatialJets.function_add line 17
  2. theorem OAI.ForcedComputation.BoundedSpatialJets.function_smul line 22
  3. def OAI.ForcedComputation.BoundedSpatialJets.fixedBilinear line 33

    Source documentation

    Fixing the first factor of a pointwise bilinear product gives a bounded linear map.

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

    Mentions: OAI.ForcedComputation.BoundedSpatialJets.Space

  4. theorem OAI.ForcedComputation.BoundedSpatialJets.fixedBilinear_apply line 50
  5. theorem OAI.ForcedComputation.BoundedSpatialJets.norm_fixedBilinear_le line 54
  6. def OAI.ForcedComputation.BoundedSpatialJets.truncate line 62

    Source documentation

    Forget higher regularity without changing the represented function.

    def truncate (k n : ℕ) (hkn : k ≤ n) (J : Space E F n) : Space E F k :=
…

    Mentions: OAI.ForcedComputation.BoundedSpatialJets.Space

  7. theorem OAI.ForcedComputation.BoundedSpatialJets.function_truncate line 67
  8. theorem OAI.ForcedComputation.BoundedSpatialJets.norm_truncate_le line 71
  9. def OAI.ForcedComputation.BoundedSpatialJets.truncateCLM line 76

    Source documentation

    The lossless bounded linear map forgetting higher spatial jets.

    def truncateCLM (k n : ℕ) (hkn : k ≤ n) : Space E F n →L[ℝ] Space E F k :=
…

    Mentions: OAI.ForcedComputation.BoundedSpatialJets.Space

  10. theorem OAI.ForcedComputation.BoundedSpatialJets.norm_truncateCLM_le_one line 93
  11. def OAI.ForcedComputation.BoundedSpatialJets.derivative line 101

    Source documentation

    A spatial derivative loses exactly one order, with no increase of jet norm.

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

    Mentions: OAI.ForcedComputation.BoundedSpatialJets.Space

  12. theorem OAI.ForcedComputation.BoundedSpatialJets.function_derivative line 108
  13. theorem OAI.ForcedComputation.BoundedSpatialJets.norm_derivative_le line 113
  14. theorem OAI.ForcedComputation.BoundedSpatialJets.function_differentiable line 117
  15. def OAI.ForcedComputation.BoundedSpatialJets.derivativeCLM line 122

    Source documentation

    Bounded spatial differentiation between consecutive finite jet spaces.

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

    Mentions: OAI.ForcedComputation.BoundedSpatialJets.Space

  16. theorem OAI.ForcedComputation.BoundedSpatialJets.norm_derivativeCLM_le_one line 154