Passing genuine Banach-valued evolution equations through uniform time-path limits.

noncomputable def EulerIntegralPathLimit.pathIntegralOperator {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (T : ℝ) (hT : 0 ≤ T) (a b : ℝ) : C(↑(Set.Icc 0 T), E) →L[ℝ] E

Integration of the actual clamped time path is a bounded linear operator.

Equations

• One or more equations did not get rendered due to their size.

theorem EulerIntegralPathLimit.pathIntegralOperator_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (T : ℝ) (hT : 0 ≤ T) (a b : ℝ) (f : C(↑(Set.Icc 0 T), E)) : (pathIntegralOperator T hT a b) f = ∫ (t : ℝ) in a..b, EulerVolterraConvolution.extendPath T hT f t

The time-integral operator is the literal Bochner interval integral.

theorem EulerIntegralPathLimit.integral_equation_of_hasDerivAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (u f : C(↑(Set.Icc 0 T), E)) (hd : ∀ t ∈ Set.Ioo 0 T, HasDerivAt (EulerVolterraConvolution.extendPath T hT u) (EulerVolterraConvolution.extendPath T hT f t) t) (t : ↑(Set.Icc 0 T)) : u t = u ⟨0, ⋯⟩ + (pathIntegralOperator T hT 0 ↑t) f

Interior time derivatives with continuous endpoint traces give the exact integral evolution formula.

theorem EulerIntegralPathLimit.integral_equation_limit {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (T : ℝ) (hT : 0 ≤ T) (u f : ℕ → C(↑(Set.Icc 0 T), E)) (v g : C(↑(Set.Icc 0 T), E)) (hu : Filter.Tendsto u Filter.atTop (nhds v)) (hf : Filter.Tendsto f Filter.atTop (nhds g)) (heq : ∀ (n : ℕ) (t : ↑(Set.Icc 0 T)), (u n) t = (u n) ⟨0, ⋯⟩ + (pathIntegralOperator T hT 0 ↑t) (f n)) (t : ↑(Set.Icc 0 T)) : v t = v ⟨0, ⋯⟩ + (pathIntegralOperator T hT 0 ↑t) g

Actual integral evolution equations pass to uniform limits of the solution and derivative paths.

theorem EulerIntegralPathLimit.hasDerivAt_of_integral_equation {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (u f : C(↑(Set.Icc 0 T), E)) (heq : ∀ (t : ↑(Set.Icc 0 T)), u t = u ⟨0, ⋯⟩ + (pathIntegralOperator T hT 0 ↑t) f) (t : ℝ) (ht : t ∈ Set.Ioo 0 T) : HasDerivAt (EulerVolterraConvolution.extendPath T hT u) (EulerVolterraConvolution.extendPath T hT f t) t

A continuous path satisfying the actual integral equation has the prescribed interior derivative.