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

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

A weakly singular Volterra integral as a bounded linear operator on continuous paths.

  1. theorem OAI.ForcedComputation.WeaklySingular.volterra_integrable line 17
  2. def OAI.ForcedComputation.WeaklySingular.Path line 42

    Source documentation

    A fixed normed-space structure for continuous paths on the closed time interval.

    def Path (T : ℝ) := C(Icc (0 : ℝ) T, E)
  3. instance OAI.ForcedComputation.WeaklySingular.(instance at line 44) line 44
  4. instance OAI.ForcedComputation.WeaklySingular.(instance at line 46) line 46
  5. instance OAI.ForcedComputation.WeaklySingular.(instance at line 48) line 48
  6. def OAI.ForcedComputation.WeaklySingular.pathEquiv line 51
  7. instance OAI.ForcedComputation.WeaklySingular.(instance at line 54) line 54
  8. def OAI.ForcedComputation.WeaklySingular.extendPath line 58

    Source documentation

    Constant continuation beyond the endpoints gives a global bounded continuous source.

    def extendPath {T : ℝ} (hT : 0 ≤ T) (u : Path E T) (s : ℝ) : E :=
…

    Mentions: OAI.ForcedComputation.WeaklySingular.Path

  9. theorem OAI.ForcedComputation.WeaklySingular.continuous_extendPath line 61
  10. theorem OAI.ForcedComputation.WeaklySingular.norm_extendPath_le line 65
  11. theorem OAI.ForcedComputation.WeaklySingular.extendPath_coe line 69
  12. def OAI.ForcedComputation.WeaklySingular.integralPath line 73
  13. theorem OAI.ForcedComputation.WeaklySingular.norm_integralPath_le line 85
  14. def OAI.ForcedComputation.WeaklySingular.integralOperator line 103

    Source documentation

    The actual Volterra operator on continuous paths; its norm is bounded by 2 C sqrt T.

    def integralOperator {T : ℝ} (hT : 0 ≤ T) (K : ℝ → E →L[ℝ] E)
    (hK : ContinuousOn K (Ioi 0)) (C : ℝ) (hC : 0 ≤ C)
    (hbound : ∀ r, 0 ≤ r → ‖K r‖ ≤ C * inverseSqrt r) :
    Path E T →L[ℝ] Path E T :=
…

    Mentions: OAI.ForcedComputation.WeaklySingular.inverseSqrt, OAI.ForcedComputation.WeaklySingular.Path

  15. theorem OAI.ForcedComputation.WeaklySingular.integralOperator_apply line 139
  16. theorem OAI.ForcedComputation.WeaklySingular.norm_integralOperator_le line 146