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

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ForcedComputation.BoundedSpatialJets.Operator line 18

   Source documentation

   The operator type with its normed-space structure fixed before taking another operator space.

   def Operator (k : ℕ) := Space E G k →L[ℝ] Space E H k

   Mentions: OAI.ForcedComputation.BoundedSpatialJets.Space

2. instance OAI.ForcedComputation.BoundedSpatialJets.(instance at line 20) line 20
3. instance OAI.ForcedComputation.BoundedSpatialJets.(instance at line 23) line 23
4. def OAI.ForcedComputation.BoundedSpatialJets.operatorEquiv line 26
5. instance OAI.ForcedComputation.BoundedSpatialJets.(instance at line 30) line 30
6. def OAI.ForcedComputation.BoundedSpatialJets.bilinearCLM line 34

   Source documentation

   Dependence of the multiplication operator on its coefficient jet is linear and bounded.

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

   Mentions: OAI.ForcedComputation.BoundedSpatialJets.Space, OAI.ForcedComputation.BoundedSpatialJets.Operator

7. theorem OAI.ForcedComputation.BoundedSpatialJets.bilinearCLM_apply line 64
8. theorem OAI.ForcedComputation.BoundedSpatialJets.norm_bilinearCLM_le line 68
9. theorem OAI.ForcedComputation.BoundedSpatialJets.continuous_bilinear line 76

   Source documentation

   Joint time continuity of coefficient and unknown is enough for continuity of the source.

   theorem continuous_bilinear {X : Type*} [TopologicalSpace X] (k : ℕ)
       (B : F →L[ℝ] G →L[ℝ] H) (J : X → Space E F k) (K : X → Space E G k)
       (hJ : Continuous J) (hK : Continuous K) :
       Continuous (fun t => bilinear E F G H k B (J t) (K t)) := by
   …

   Mentions: OAI.ForcedComputation.BoundedSpatialJets.Space, OAI.ForcedComputation.BoundedSpatialJets.bilinear

10. theorem OAI.ForcedComputation.BoundedSpatialJets.continuousOn_bilinear line 84

    Source documentation

    The same continuity statement restricted to a time interval.

    theorem continuousOn_bilinear {X : Type*} [TopologicalSpace X] (S : Set X) (k : ℕ)
        (B : F →L[ℝ] G →L[ℝ] H) (J : X → Space E F k) (K : X → Space E G k)
        (hJ : ContinuousOn J S) (hK : ContinuousOn K S) :
        ContinuousOn (fun t => bilinear E F G H k B (J t) (K t)) S := by
    …

    Mentions: OAI.ForcedComputation.BoundedSpatialJets.Space, OAI.ForcedComputation.BoundedSpatialJets.bilinear