Documentation

LeanPool.AnomalousDiffusion.AVenhance.Infra.ODE.Linear.Basic

Integral-form linear ODEs #

This file records the integral formulation used for linear equations with measurable coefficients, together with the continuity and almost-everywhere derivative consequences of the Lebesgue differentiation theorem. The coefficient and forcing are deliberately abstract: the file is reusable for finite-dimensional spaces and for other complete real normed spaces.

source
def AVenhance.Infra.ODE.linearRhs {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (A : ℝ → E →L[ℝ] E) (f y : ℝ → E) (t : ℝ) :
E

The right-hand side of a time-dependent linear equation.

Equations
Instances For
    source
    def AVenhance.Infra.ODE.IsLinearIntegralSolution {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (A : ℝ → E →L[ℝ] E) (f : ℝ → E) (y₀ : E) (a b : ℝ) (y : ℝ → E) :
    Prop

    Integral form of y' = A(t)y + f(t) on the oriented interval a..b.

    Equations
    Instances For
      source
      theorem AVenhance.Infra.ODE.continuousOn_intervalPrimitive {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {g : ℝ → E} {a b : ℝ} (hg : IntervalIntegrable g MeasureTheory.volume a b) :
      ContinuousOn (fun (t : ℝ) => ∫ (s : ℝ) in a..t, g s) (Set.uIcc a b)

      A vector-valued integral primitive is continuous on the interval of integrability.

      source
      theorem AVenhance.Infra.ODE.ae_hasDerivAt_intervalPrimitive {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {g : ℝ → E} {a b : ℝ} [CompleteSpace E] (hg : IntervalIntegrable g MeasureTheory.volume a b) :
      ∀ᵐ (t : ℝ), t ∈ Set.uIcc a b → HasDerivAt (fun (x : ℝ) => ∫ (s : ℝ) in a..x, g s) (g t) t

      Lebesgue differentiation for the vector-valued interval primitive, with basepoint a.

      source
      theorem AVenhance.Infra.ODE.IntervalIntegrable.absolutelyContinuousOnInterval_intervalIntegral_vector {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {g : ℝ → E} {a b c : ℝ} (hg : IntervalIntegrable g MeasureTheory.volume a b) (hc : c ∈ Set.uIcc a b) :
      AbsolutelyContinuousOnInterval (fun (x : ℝ) => ∫ (t : ℝ) in c..x, g t) a b

      The interval primitive of a Banach-valued integrable function is absolutely continuous.

      source
      theorem AVenhance.Infra.ODE.IsLinearIntegralSolution.absolutelyContinuousOnInterval {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {A : ℝ → E →L[ℝ] E} {f y : ℝ → E} {y₀ : E} {a b : ℝ} (hab : a ≤ b) (hy : IsLinearIntegralSolution A f y₀ a b y) (h_rhs : IntervalIntegrable (linearRhs A f y) MeasureTheory.volume a b) :
      AbsolutelyContinuousOnInterval y a b

      Integral-form solutions are absolutely continuous whenever their right-hand side is L¹.

      source
      theorem AVenhance.Infra.ODE.IsLinearIntegralSolution.ae_hasDerivAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {A : ℝ → E →L[ℝ] E} {f y : ℝ → E} {y₀ : E} {a b : ℝ} [CompleteSpace E] (hab : a ≤ b) (hy : IsLinearIntegralSolution A f y₀ a b y) (h_rhs : IntervalIntegrable (linearRhs A f y) MeasureTheory.volume a b) :
      ∀ᵐ (t : ℝ), t ∈ Set.Icc a b → HasDerivAt y (linearRhs A f y t) t

      Integral-form solutions have the ordinary derivative almost everywhere in the interval.