Actual continuous fundamental paths from the existence theorem

This module chooses the paths whose existence was proved by Picard iteration and records their initial values, two-sided inverse identities, and actual within-interval derivatives. The final specialization constructs an Evolution for every continuous bounded operator coefficient.

Construction of a homogeneous fundamental solution

Continuous bounded coefficients in a real Banach algebra have actual forward and inverse fundamental paths. Existence is the previously proved global Lipschitz Picard theorem; both inverse identities follow by differentiation and ODE uniqueness. This result is qualitative. No exponential estimate from this construction is used in the later profile estimates.

theorem EulerLinearFundamentalExistence.exists_fundamental {A : Type u_1} [NormedRing A] [NormedAlgebra ℝ A] [CompleteSpace A] (T : ℝ) (hT : 0 ≤ T) (B : C(↑(Set.Icc 0 T), A)) : ∃ (Φ : ℝ → A) (Ψ : ℝ → A), Φ 0 = 1 ∧ Ψ 0 = 1 ∧ (∀ t ∈ Set.Icc 0 T, HasDerivAt Φ (EulerVolterraConvolution.extendPath T hT B t * Φ t) t) ∧ (∀ t ∈ Set.Icc 0 T, HasDerivAt Ψ (-(Ψ t * EulerVolterraConvolution.extendPath T hT B t)) t) ∧ ∀ t ∈ Set.Icc 0 T, Φ t * Ψ t = 1 ∧ Ψ t * Φ t = 1

A continuous coefficient field has two-sided inverse fundamental paths.

structure EulerLinearFundamentalExistence.FundamentalPath {A : Type u_1} [NormedRing A] [NormedAlgebra ℝ A] (T : ℝ) (hT : 0 ≤ T) (B : C(↑(Set.Icc 0 T), A)) : Type u_1

The continuous paths constructed from the actual Banach-space ODE.

• forward : C(↑(Set.Icc 0 T), A)

  Forward of FundamentalPath, of type C(Icc (0 : ℝ) T,A).

• backward : C(↑(Set.Icc 0 T), A)

  Backward of FundamentalPath, of type C(Icc (0 : ℝ) T,A).

• forward_initial : self.forward ⟨0, ⋯⟩ = 1
• backward_initial : self.backward ⟨0, ⋯⟩ = 1
• forward_backward (t : ↑(Set.Icc 0 T)) : self.forward t * self.backward t = 1
• backward_forward (t : ↑(Set.Icc 0 T)) : self.backward t * self.forward t = 1
• derivative (t : ↑(Set.Icc 0 T)) : HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT self.forward) (B t * self.forward t) (Set.Icc 0 T) ↑t

theorem EulerLinearFundamentalExistence.nonempty_fundamentalPath {A : Type u_1} [NormedRing A] [NormedAlgebra ℝ A] [CompleteSpace A] (T : ℝ) (hT : 0 ≤ T) (B : C(↑(Set.Icc 0 T), A)) : Nonempty (FundamentalPath T hT B)

Every continuous coefficient has such actual paths, with no smallness hypothesis.

noncomputable def EulerLinearFundamentalExistence.fundamentalPath {A : Type u_1} [NormedRing A] [NormedAlgebra ℝ A] [CompleteSpace A] (T : ℝ) (hT : 0 ≤ T) (B : C(↑(Set.Icc 0 T), A)) : FundamentalPath T hT B

A fixed choice of the genuinely constructed fundamental paths.

Equations

• EulerLinearFundamentalExistence.fundamentalPath T hT B = Classical.choice ⋯

noncomputable def EulerLinearDuhamel.constructedEvolution {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (B : C(↑(Set.Icc 0 T), E →L[ℝ] E)) : Evolution T hT B

A homogeneous evolution constructed for an arbitrary continuous operator coefficient.

Equations

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

theorem EulerLinearDuhamel.constructedEvolution_initial {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (B : C(↑(Set.Icc 0 T), E →L[ℝ] E)) : (constructedEvolution T hT B).forward ⟨0, ⋯⟩ = ContinuousLinearMap.id ℝ E

Its forward path starts at the identity.