Volterra operator for bounded measurable linear coefficients

The interval path is represented by a ContinuousMap on Icc a b. A continuous clamping extension lets us state Bochner integrability on the ambient real line without adding arbitrary measurability assumptions outside the interval.

def AVenhance.Infra.ODE.clampPoint (a b : ℝ) (hab : a ≤ b) (t : ℝ) : ↑(Set.Icc a b)

A point of [a,b] obtained by clamping a real number to the interval.

Equations

• AVenhance.Infra.ODE.clampPoint a b hab t = ⟨max a (min b t), ⋯⟩

def AVenhance.Infra.ODE.extendCurve {E : Type u_1} [NormedAddCommGroup E] {a b : ℝ} (hab : a ≤ b) (u : C(↑(Set.Icc a b), E)) : ℝ → E

Extend a continuous path on [a,b] to the line by constant continuation at both endpoints.

Equations

• AVenhance.Infra.ODE.extendCurve hab u t = u (AVenhance.Infra.ODE.clampPoint a b hab t)

theorem AVenhance.Infra.ODE.continuous_extendCurve {E : Type u_1} [NormedAddCommGroup E] {a b : ℝ} (hab : a ≤ b) (u : C(↑(Set.Icc a b), E)) : Continuous (extendCurve hab u)

@[simp]

theorem AVenhance.Infra.ODE.extendCurve_eq_of_mem {E : Type u_1} [NormedAddCommGroup E] {a b : ℝ} (hab : a ≤ b) (u : C(↑(Set.Icc a b), E)) {t : ℝ} (ht : t ∈ Set.Icc a b) : extendCurve hab u t = u ⟨t, ht⟩

structure AVenhance.Infra.ODE.LinearODEData {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (a b : ℝ) (hab : a ≤ b) : Type u_1

Data for a bounded measurable linear equation with an L¹ forcing on [a,b].

• A : ℝ → E →L[ℝ] E

  Time-dependent bounded linear operator in the inhomogeneous ODE.

• f : ℝ → E

  Integrable forcing term in the inhomogeneous ODE.

• y₀ : E

  Initial state at time zero for the inhomogeneous ODE.

• operatorBound : ℝ

  Uniform operator-norm bound on the ODE coefficient.

• operatorBound_nonneg : 0 ≤ self.operatorBound
• operator_aestronglyMeasurable : MeasureTheory.AEStronglyMeasurable self.A MeasureTheory.volume
• operator_norm_le (t : ℝ) : ‖self.A t‖ ≤ self.operatorBound
• forcing_intervalIntegrable : IntervalIntegrable self.f MeasureTheory.volume a b

def AVenhance.Infra.ODE.LinearODEData.rhs {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} {hab : a ≤ b} (D : LinearODEData a b hab) (u : C(↑(Set.Icc a b), E)) (t : ℝ) : E

The right-hand side evaluated along a continuous path.

Equations

• D.rhs u t = (D.A t) (AVenhance.Infra.ODE.extendCurve hab u t) + D.f t

theorem AVenhance.Infra.ODE.LinearODEData.rhs_intervalIntegrable {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} {hab : a ≤ b} (D : LinearODEData a b hab) (u : C(↑(Set.Icc a b), E)) : IntervalIntegrable (D.rhs u) MeasureTheory.volume a b

noncomputable def AVenhance.Infra.ODE.LinearODEData.volterra {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} {hab : a ≤ b} (D : LinearODEData a b hab) : C(↑(Set.Icc a b), E) → C(↑(Set.Icc a b), E)

The Volterra operator on continuous paths on [a,b].

Equations

• D.volterra u = { toFun := fun (t : ↑(Set.Icc a b)) => D.y₀ + ∫ (s : ℝ) in a..↑t, D.rhs u s, continuous_toFun := ⋯ }

@[simp]

theorem AVenhance.Infra.ODE.LinearODEData.volterra_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} {hab : a ≤ b} (D : LinearODEData a b hab) (u : C(↑(Set.Icc a b), E)) (t : ↑(Set.Icc a b)) : (D.volterra u) t = D.y₀ + ∫ (s : ℝ) in a..↑t, D.rhs u s

theorem AVenhance.Infra.ODE.LinearODEData.dist_iterate_volterra_apply_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} {hab : a ≤ b} (D : LinearODEData a b hab) (u v : C(↑(Set.Icc a b), E)) (n : ℕ) (t : ↑(Set.Icc a b)) : dist ((D.volterra^[n] u) t) ((D.volterra^[n] v) t) ≤ (D.operatorBound * |↑t - a|) ^ n / ↑n.factorial * dist u v

The nth Volterra iterates have the standard factorial difference bound.

theorem AVenhance.Infra.ODE.LinearODEData.dist_iterate_volterra_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} {hab : a ≤ b} (D : LinearODEData a b hab) (u v : C(↑(Set.Icc a b), E)) (n : ℕ) : dist (D.volterra^[n] u) (D.volterra^[n] v) ≤ (D.operatorBound * (b - a)) ^ n / ↑n.factorial * dist u v

A global sup-norm estimate for the iterates follows from compactness of the time interval.

theorem AVenhance.Infra.ODE.LinearODEData.exists_contracting_volterra_iterate {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} {hab : a ≤ b} (D : LinearODEData a b hab) : ∃ (n : ℕ) (K : NNReal), ContractingWith K D.volterra^[n]

The Volterra map has a contracting iterate on every finite interval.

def AVenhance.Infra.ODE.LinearODEData.IsSolution {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} {hab : a ≤ b} (D : LinearODEData a b hab) (u : C(↑(Set.Icc a b), E)) : Prop

A continuous path is an integral solution exactly when it is a fixed point of the Volterra operator.

Equations

• D.IsSolution u = (D.volterra u = u)

theorem AVenhance.Infra.ODE.LinearODEData.existsUnique_solution {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} {hab : a ≤ b} [CompleteSpace E] (D : LinearODEData a b hab) : ∃! u : C(↑(Set.Icc a b), E), D.IsSolution u

There is exactly one continuous integral solution on the whole interval.

theorem AVenhance.Infra.ODE.LinearODEData.IsSolution.integralSolution {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} {hab : a ≤ b} (D : LinearODEData a b hab) (u : C(↑(Set.Icc a b), E)) (hu : D.IsSolution u) : IsLinearIntegralSolution D.A D.f D.y₀ a b (extendCurve hab u)

A Volterra fixed point gives the integral equation on the ambient interval.

theorem AVenhance.Infra.ODE.LinearODEData.isSolution_iff_integralSolution {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} {hab : a ≤ b} (D : LinearODEData a b hab) (u : C(↑(Set.Icc a b), E)) : D.IsSolution u ↔ IsLinearIntegralSolution D.A D.f D.y₀ a b (extendCurve hab u)

On continuous interval paths, the fixed-point equation is equivalent to the integral form.

theorem AVenhance.Infra.ODE.LinearODEData.IsSolution.absolutelyContinuousOnInterval {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} {hab : a ≤ b} (D : LinearODEData a b hab) (u : C(↑(Set.Icc a b), E)) (hu : D.IsSolution u) : AbsolutelyContinuousOnInterval (extendCurve hab u) a b

The continuous solution supplied by the fixed-point theorem is absolutely continuous.

theorem AVenhance.Infra.ODE.LinearODEData.existsUnique_absolutelyContinuous_integralSolution {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} {hab : a ≤ b} [CompleteSpace E] (D : LinearODEData a b hab) : ∃! u : C(↑(Set.Icc a b), E), IsLinearIntegralSolution D.A D.f D.y₀ a b (extendCurve hab u) ∧ AbsolutelyContinuousOnInterval (extendCurve hab u) a b

Existence and uniqueness in the requested absolutely-continuous integral-solution class.

theorem AVenhance.Infra.ODE.LinearODEData.IsSolution.ae_hasDerivAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} {hab : a ≤ b} [CompleteSpace E] (D : LinearODEData a b hab) (u : C(↑(Set.Icc a b), E)) (hu : D.IsSolution u) : ∀ᵐ (t : ℝ), t ∈ Set.Icc a b → HasDerivAt (extendCurve hab u) ((D.A t) (extendCurve hab u t) + D.f t) t

The solution is differentiable almost everywhere and satisfies the ODE there.