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

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Continuity of a Volterra integral with an inverse-square-root operator singularity.

  1. theorem OAI.ForcedComputation.WeaklySingular.scale_inverseSqrt line 16
  2. def OAI.ForcedComputation.WeaklySingular.scaled line 30
  3. theorem OAI.ForcedComputation.WeaklySingular.volterra_eq_scaled line 33
  4. theorem OAI.ForcedComputation.WeaklySingular.norm_scaled_le line 46
  5. theorem OAI.ForcedComputation.WeaklySingular.scaled_continuousAt_parameter line 63
  6. theorem OAI.ForcedComputation.WeaklySingular.scaled_measurable line 75
  7. theorem OAI.ForcedComputation.WeaklySingular.continuousAt_volterra line 92

    Source documentation

    Positive-time continuity follows by moving the integral to a fixed unit interval.

    theorem continuousAt_volterra (K : ℝ → E →L[ℝ] E) (u : ℝ → E)
    (hK : ContinuousOn K (Ioi 0)) (hu : Continuous u)
    (C B : ℝ) (hC : 0 ≤ C)
    (hbound : ∀ r, 0 ≤ r → ‖K r‖ ≤ C * inverseSqrt r)
    (hub : ∀ s, ‖u s‖ ≤ B) {t : ℝ} (ht : 0 < t) :
    ContinuousAt (volterra E K u) t := by
…

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

  8. theorem OAI.ForcedComputation.WeaklySingular.continuousWithinAt_volterra_zero line 123

    Source documentation

    The O(sqrt(t)) estimate supplies the missing continuity at the initial endpoint.

    theorem continuousWithinAt_volterra_zero (K : ℝ → E →L[ℝ] E) (u : ℝ → E)
    (C B : ℝ) (hC : 0 ≤ C)
    (hbound : ∀ r, 0 ≤ r → ‖K r‖ ≤ C * inverseSqrt r)
    (hub : ∀ s, ‖u s‖ ≤ B) :
    ContinuousWithinAt (volterra E K u) (Ici 0) 0 := by
…

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

  9. theorem OAI.ForcedComputation.WeaklySingular.continuousOn_volterra line 139

    Source documentation

    A bounded continuous source produces a continuous Volterra path on every finite time interval.

    theorem continuousOn_volterra (K : ℝ → E →L[ℝ] E) (u : ℝ → E)
    (hK : ContinuousOn K (Ioi 0)) (hu : Continuous u)
    (C B : ℝ) (hC : 0 ≤ C)
    (hbound : ∀ r, 0 ≤ r → ‖K r‖ ≤ C * inverseSqrt r)
    (hub : ∀ s, ‖u s‖ ≤ B) : ContinuousOn (volterra E K u) (Ici 0) := by
…

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