Relative perturbation estimates for the finite-dimensional scalar ODE in the Euler packet proposal. These results do not assert the PDE packet lemma.

theorem EulerPacketPerturbation.integral_absorb {g : ℝ → ℝ} {a b A K : ℝ} (hab : a ≤ b) (hg : ContinuousOn g (Set.Icc a b)) (hgn : ∀ t ∈ Set.Icc a b, 0 ≤ g t) (hK : 0 ≤ K) (hsmall : K * (b - a) ≤ 1 / 2) (hineq : ∀ t ∈ Set.Icc a b, g t ≤ A + K * ∫ (s : ℝ) in a..t, g s) (t : ℝ) : t ∈ Set.Icc a b → g t ≤ 2 * A

A compact-interval Volterra absorption estimate with an explicit factor of two and no exponential loss.

theorem EulerPacketPerturbation.relative_integral_absorb {f U : ℝ → ℝ} {a b A K : ℝ} (hab : a ≤ b) (hf : ContinuousOn f (Set.Icc a b)) (hU : ContinuousOn U (Set.Icc a b)) (hfn : ∀ t ∈ Set.Icc a b, 0 ≤ f t) (hUp : ∀ t ∈ Set.Icc a b, 0 < U t) (hK : 0 ≤ K) (hsmall : K * (b - a) ≤ 1 / 2) (hineq : ∀ t ∈ Set.Icc a b, f t ≤ U t * (A + K * ∫ (s : ℝ) in a..t, f s / U s)) (t : ℝ) : t ∈ Set.Icc a b → f t ≤ 2 * A * U t

Absorbing a Duhamel inequality after division by a positive reference solution. This preserves relative rather than absolute control.

theorem EulerPacketPerturbation.forced_wronskian_derivative {D c u u₁ Y Y₁ f g : ℝ → ℝ} {t : ℝ} (hu : HasDerivAt u (u₁ t) t) (hfu : HasDerivAt (fun (s : ℝ) => D s * u₁ s) (c t * u t) t) (hY : HasDerivAt Y (Y₁ t + f t) t) (hfY : HasDerivAt (fun (s : ℝ) => D s * Y₁ s) (c t * Y t + D t * g t) t) : HasDerivAt (fun (s : ℝ) => u s * (D s * Y₁ s) - D s * u₁ s * Y s) (D t * (u t * g t - u₁ t * f t)) t

The Wronskian of a homogeneous solution and a forced solution obeys an exact first-order forcing identity.

theorem EulerPacketPerturbation.forced_wronskian_integral {D c u u₁ Y Y₁ f g : ℝ → ℝ} {a b : ℝ} (hu : ∀ t ∈ Set.Icc a b, HasDerivAt u (u₁ t) t) (hfu : ∀ t ∈ Set.Icc a b, HasDerivAt (fun (s : ℝ) => D s * u₁ s) (c t * u t) t) (hY : ∀ t ∈ Set.Icc a b, HasDerivAt Y (Y₁ t + f t) t) (hfY : ∀ t ∈ Set.Icc a b, HasDerivAt (fun (s : ℝ) => D s * Y₁ s) (c t * Y t + D t * g t) t) (hDc : ContinuousOn D (Set.Icc a b)) (hu₁c : ContinuousOn u₁ (Set.Icc a b)) (hfc : ContinuousOn f (Set.Icc a b)) (hgc : ContinuousOn g (Set.Icc a b)) (t : ℝ) : t ∈ Set.Icc a b → u t * (D t * Y₁ t) - D t * u₁ t * Y t = u a * (D a * Y₁ a) - D a * u₁ a * Y a + ∫ (s : ℝ) in a..t, D s * (u s * g s - u₁ s * f s)

The integrated forced Wronskian identity.

theorem EulerPacketPerturbation.forced_variation_of_constants {D c u u₁ v v₁ Y Y₁ f g : ℝ → ℝ} {a b : ℝ} (hu : ∀ t ∈ Set.Icc a b, HasDerivAt u (u₁ t) t) (hv : ∀ t ∈ Set.Icc a b, HasDerivAt v (v₁ t) t) (hfu : ∀ t ∈ Set.Icc a b, HasDerivAt (fun (s : ℝ) => D s * u₁ s) (c t * u t) t) (hfv : ∀ t ∈ Set.Icc a b, HasDerivAt (fun (s : ℝ) => D s * v₁ s) (c t * v t) t) (hY : ∀ t ∈ Set.Icc a b, HasDerivAt Y (Y₁ t + f t) t) (hfY : ∀ t ∈ Set.Icc a b, HasDerivAt (fun (s : ℝ) => D s * Y₁ s) (c t * Y t + D t * g t) t) (hDc : ContinuousOn D (Set.Icc a b)) (hu₁c : ContinuousOn u₁ (Set.Icc a b)) (hv₁c : ContinuousOn v₁ (Set.Icc a b)) (hfc : ContinuousOn f (Set.Icc a b)) (hgc : ContinuousOn g (Set.Icc a b)) (hW0 : u a * (D a * v₁ a) - D a * u₁ a * v a = 1) (t : ℝ) : t ∈ Set.Icc a b → have A := u a * (D a * Y₁ a) - D a * u₁ a * Y a + ∫ (s : ℝ) in a..t, D s * (u s * g s - u₁ s * f s); have B := v a * (D a * Y₁ a) - D a * v₁ a * Y a + ∫ (s : ℝ) in a..t, D s * (v s * g s - v₁ s * f s); Y t = v t * A - u t * B ∧ Y₁ t = v₁ t * A - u₁ t * B

Variation of constants from two homogeneous solutions whose Wronskian flux is normalized to one. This handles forcing in both state components.

def EulerPacketPerturbation.kernel11 (D u u₁ v v₁ : ℝ → ℝ) (t s : ℝ) : ℝ

First displacement component of the scalar fundamental propagator.

Equations

• EulerPacketPerturbation.kernel11 D u u₁ v v₁ t s = D s * (u t * v₁ s - v t * u₁ s)

def EulerPacketPerturbation.kernel12 (D u v : ℝ → ℝ) (t s : ℝ) : ℝ

First velocity component of the scalar fundamental propagator.

Equations

• EulerPacketPerturbation.kernel12 D u v t s = D s * (v t * u s - u t * v s)

def EulerPacketPerturbation.kernel21 (D u₁ v₁ : ℝ → ℝ) (t s : ℝ) : ℝ

Second displacement component of the scalar fundamental propagator.

Equations

• EulerPacketPerturbation.kernel21 D u₁ v₁ t s = D s * (u₁ t * v₁ s - v₁ t * u₁ s)

def EulerPacketPerturbation.kernel22 (D u u₁ v v₁ : ℝ → ℝ) (t s : ℝ) : ℝ

Second velocity component of the scalar fundamental propagator.

Equations

• EulerPacketPerturbation.kernel22 D u u₁ v v₁ t s = D s * (v₁ t * u s - u₁ t * v s)

theorem EulerPacketPerturbation.forced_kernel_formula {D c u u₁ v v₁ Y Y₁ f g : ℝ → ℝ} {a b : ℝ} (hu : ∀ t ∈ Set.Icc a b, HasDerivAt u (u₁ t) t) (hv : ∀ t ∈ Set.Icc a b, HasDerivAt v (v₁ t) t) (hfu : ∀ t ∈ Set.Icc a b, HasDerivAt (fun (s : ℝ) => D s * u₁ s) (c t * u t) t) (hfv : ∀ t ∈ Set.Icc a b, HasDerivAt (fun (s : ℝ) => D s * v₁ s) (c t * v t) t) (hY : ∀ t ∈ Set.Icc a b, HasDerivAt Y (Y₁ t + f t) t) (hfY : ∀ t ∈ Set.Icc a b, HasDerivAt (fun (s : ℝ) => D s * Y₁ s) (c t * Y t + D t * g t) t) (hDc : ContinuousOn D (Set.Icc a b)) (hu₁c : ContinuousOn u₁ (Set.Icc a b)) (hv₁c : ContinuousOn v₁ (Set.Icc a b)) (hfc : ContinuousOn f (Set.Icc a b)) (hgc : ContinuousOn g (Set.Icc a b)) (hW0 : u a * (D a * v₁ a) - D a * u₁ a * v a = 1) (t : ℝ) : t ∈ Set.Icc a b → Y t = kernel11 D u u₁ v v₁ t a * Y a + kernel12 D u v t a * Y₁ a + ∫ (s : ℝ) in a..t, kernel11 D u u₁ v v₁ t s * f s + kernel12 D u v t s * g s ∧ Y₁ t = kernel21 D u₁ v₁ t a * Y a + kernel22 D u u₁ v v₁ t a * Y₁ a + ∫ (s : ℝ) in a..t, kernel21 D u₁ v₁ t s * f s + kernel22 D u u₁ v v₁ t s * g s

Duhamel's formula in component form, with an explicitly defined fundamental kernel.

theorem EulerPacketPerturbation.linear_combination_solution {D c u u₁ v v₁ : ℝ → ℝ} {t A B : ℝ} (hu : HasDerivAt u (u₁ t) t) (hv : HasDerivAt v (v₁ t) t) (hfu : HasDerivAt (fun (s : ℝ) => D s * u₁ s) (c t * u t) t) (hfv : HasDerivAt (fun (s : ℝ) => D s * v₁ s) (c t * v t) t) : HasDerivAt (fun (s : ℝ) => A * u s + B * v s) (A * u₁ t + B * v₁ t) t ∧ HasDerivAt (fun (s : ℝ) => D s * (A * u₁ s + B * v₁ s)) (c t * (A * u t + B * v t)) t

Linear combinations of homogeneous scalar solutions are homogeneous.

theorem EulerPacketPerturbation.equation30_kernel_bound {ε Θ : ℝ} {U U₁ V V₁ : ℝ → ℝ} (hε : 0 < ε) (hεsmall : ε ≤ 1 / 4) (hΘ : 1 ≤ Θ) (hU : ∀ (t : ℝ), 0 ≤ t → HasDerivAt U (U₁ t) t) (hV : ∀ (t : ℝ), 0 ≤ t → HasDerivAt V (V₁ t) t) (hfluxU : ∀ (t : ℝ), 0 ≤ t → HasDerivAt (fun (s : ℝ) => (1 + (ε ^ 2 * s ^ 2) ^ 2) * U₁ s) (2 * (1 - ε ^ 2 * (ε ^ 2 * t ^ 2)) * U t) t) (hfluxV : ∀ (t : ℝ), 0 ≤ t → HasDerivAt (fun (s : ℝ) => (1 + (ε ^ 2 * s ^ 2) ^ 2) * V₁ s) (2 * (1 - ε ^ 2 * (ε ^ 2 * t ^ 2)) * V t) t) (hU0 : U 0 = 1) (hU₁0 : U₁ 0 = 0) (hV₁0 : V₁ 0 = 1) (s t : ℝ) : 0 ≤ s → s ≤ t → t ≤ Θ → have D := fun (r : ℝ) => 1 + (ε ^ 2 * r ^ 2) ^ 2; |kernel11 D U U₁ V V₁ t s| + |kernel21 D U₁ V₁ t s| ≤ 20 * Θ ^ 8 * (U t / U s) ∧ |kernel12 D U V t s| + |kernel22 D U U₁ V V₁ t s| ≤ 20 * Θ ^ 8 * (U t / U s)

The ideal fundamental kernel inherits the relative propagator bound in each column.

theorem EulerPacketPerturbation.two_column_bound {a b c d x y C : ℝ} (h1 : |a| + |c| ≤ C) (h2 : |b| + |d| ≤ C) : |a * x + b * y| + |c * x + d * y| ≤ C * (|x| + |y|)

The induced sum-of-absolute-values bound from two column bounds.

theorem EulerPacketPerturbation.kernel_integral_bound {K11 K12 K21 K22 f g U : ℝ → ℝ} {a b y0 y₁0 y y₁ C : ℝ} (hab : a ≤ b) (h11 : ContinuousOn K11 (Set.Icc a b)) (h12 : ContinuousOn K12 (Set.Icc a b)) (h21 : ContinuousOn K21 (Set.Icc a b)) (h22 : ContinuousOn K22 (Set.Icc a b)) (hfc : ContinuousOn f (Set.Icc a b)) (hgc : ContinuousOn g (Set.Icc a b)) (hUc : ContinuousOn U (Set.Icc a b)) (hUp : ∀ s ∈ Set.Icc a b, 0 < U s) (hcol1 : ∀ s ∈ Set.Icc a b, |K11 s| + |K21 s| ≤ C * (U b / U s)) (hcol2 : ∀ s ∈ Set.Icc a b, |K12 s| + |K22 s| ≤ C * (U b / U s)) (hy : y = K11 a * y0 + K12 a * y₁0 + ∫ (s : ℝ) in a..b, K11 s * f s + K12 s * g s) (hy₁ : y₁ = K21 a * y0 + K22 a * y₁0 + ∫ (s : ℝ) in a..b, K21 s * f s + K22 s * g s) : |y| + |y₁| ≤ C * (U b / U a) * (|y0| + |y₁0|) + C * U b * ∫ (s : ℝ) in a..b, (|f s| + |g s|) / U s

Passing from Duhamel's formula and relative kernel bounds to a scalar relative integral inequality, with the forcing in both components.

theorem EulerPacketPerturbation.equation30_forced_bound {ε Θ a b : ℝ} {U U₁ V V₁ Y Y₁ f g : ℝ → ℝ} (hε : 0 < ε) (hεsmall : ε ≤ 1 / 4) (hΘ : 1 ≤ Θ) (ha : 0 ≤ a) (hb : b ≤ Θ) (hU : ∀ (t : ℝ), 0 ≤ t → HasDerivAt U (U₁ t) t) (hV : ∀ (t : ℝ), 0 ≤ t → HasDerivAt V (V₁ t) t) (hfluxU : ∀ (t : ℝ), 0 ≤ t → HasDerivAt (fun (s : ℝ) => (1 + (ε ^ 2 * s ^ 2) ^ 2) * U₁ s) (2 * (1 - ε ^ 2 * (ε ^ 2 * t ^ 2)) * U t) t) (hfluxV : ∀ (t : ℝ), 0 ≤ t → HasDerivAt (fun (s : ℝ) => (1 + (ε ^ 2 * s ^ 2) ^ 2) * V₁ s) (2 * (1 - ε ^ 2 * (ε ^ 2 * t ^ 2)) * V t) t) (hU0 : U 0 = 1) (hU₁0 : U₁ 0 = 0) (hV₁0 : V₁ 0 = 1) (hY : ∀ t ∈ Set.Icc a b, HasDerivAt Y (Y₁ t + f t) t) (hfluxY : ∀ t ∈ Set.Icc a b, HasDerivAt (fun (s : ℝ) => (1 + (ε ^ 2 * s ^ 2) ^ 2) * Y₁ s) (2 * (1 - ε ^ 2 * (ε ^ 2 * t ^ 2)) * Y t + (1 + (ε ^ 2 * t ^ 2) ^ 2) * g t) t) (hfc : ContinuousOn f (Set.Icc a b)) (hgc : ContinuousOn g (Set.Icc a b)) (t : ℝ) : t ∈ Set.Icc a b → |Y t| + |Y₁ t| ≤ 20 * Θ ^ 8 * (U t / U a) * (|Y a| + |Y₁ a|) + 20 * Θ ^ 8 * U t * ∫ (s : ℝ) in a..t, (|f s| + |g s|) / U s

Duhamel's inequality for the exact scalar ODE, measured relative to the zero-slope reference solution. The forcing may occur in both components.

theorem EulerPacketPerturbation.continuousOn_of_flux {D f : ℝ → ℝ} {S : Set ℝ} (hD : ContinuousOn D S) (hf : ContinuousOn (fun (t : ℝ) => D t * f t) S) (hDn : ∀ t ∈ S, D t ≠ 0) : ContinuousOn f S

Continuity of the second state component follows from continuity of its nonvanishing flux coefficient and of the flux.

theorem EulerPacketPerturbation.equation30_perturbed_bound {ε Θ a b δ : ℝ} {U U₁ V V₁ Y Y₁ f g : ℝ → ℝ} (hε : 0 < ε) (hεsmall : ε ≤ 1 / 4) (hΘ : 1 ≤ Θ) (ha : 0 ≤ a) (hab : a ≤ b) (hb : b ≤ Θ) (hδ : 0 ≤ δ) (hsmall : 20 * Θ ^ 8 * δ * (b - a) ≤ 1 / 2) (hU : ∀ (t : ℝ), 0 ≤ t → HasDerivAt U (U₁ t) t) (hV : ∀ (t : ℝ), 0 ≤ t → HasDerivAt V (V₁ t) t) (hfluxU : ∀ (t : ℝ), 0 ≤ t → HasDerivAt (fun (s : ℝ) => (1 + (ε ^ 2 * s ^ 2) ^ 2) * U₁ s) (2 * (1 - ε ^ 2 * (ε ^ 2 * t ^ 2)) * U t) t) (hfluxV : ∀ (t : ℝ), 0 ≤ t → HasDerivAt (fun (s : ℝ) => (1 + (ε ^ 2 * s ^ 2) ^ 2) * V₁ s) (2 * (1 - ε ^ 2 * (ε ^ 2 * t ^ 2)) * V t) t) (hU0 : U 0 = 1) (hU₁0 : U₁ 0 = 0) (hV₁0 : V₁ 0 = 1) (hY : ∀ t ∈ Set.Icc a b, HasDerivAt Y (Y₁ t + f t) t) (hfluxY : ∀ t ∈ Set.Icc a b, HasDerivAt (fun (s : ℝ) => (1 + (ε ^ 2 * s ^ 2) ^ 2) * Y₁ s) (2 * (1 - ε ^ 2 * (ε ^ 2 * t ^ 2)) * Y t + (1 + (ε ^ 2 * t ^ 2) ^ 2) * g t) t) (hfc : ContinuousOn f (Set.Icc a b)) (hgc : ContinuousOn g (Set.Icc a b)) (hforcing : ∀ t ∈ Set.Icc a b, |f t| + |g t| ≤ δ * (|Y t| + |Y₁ t|)) (t : ℝ) : t ∈ Set.Icc a b → |Y t| + |Y₁ t| ≤ 40 * Θ ^ 8 * (U t / U a) * (|Y a| + |Y₁ a|)

A sufficiently small perturbation grows by at most twice the ideal relative propagator bound. Smallness is an explicit interval inequality.

theorem EulerPacketPerturbation.equation30_perturbed_difference_bound {ε Θ a b δ : ℝ} {U U₁ V V₁ Y Y₁ Z Z₁ f g : ℝ → ℝ} (hε : 0 < ε) (hεsmall : ε ≤ 1 / 4) (hΘ : 1 ≤ Θ) (ha : 0 ≤ a) (hab : a ≤ b) (hb : b ≤ Θ) (hδ : 0 ≤ δ) (hsmall : 20 * Θ ^ 8 * δ * (b - a) ≤ 1 / 2) (hU : ∀ (t : ℝ), 0 ≤ t → HasDerivAt U (U₁ t) t) (hV : ∀ (t : ℝ), 0 ≤ t → HasDerivAt V (V₁ t) t) (hfluxU : ∀ (t : ℝ), 0 ≤ t → HasDerivAt (fun (s : ℝ) => (1 + (ε ^ 2 * s ^ 2) ^ 2) * U₁ s) (2 * (1 - ε ^ 2 * (ε ^ 2 * t ^ 2)) * U t) t) (hfluxV : ∀ (t : ℝ), 0 ≤ t → HasDerivAt (fun (s : ℝ) => (1 + (ε ^ 2 * s ^ 2) ^ 2) * V₁ s) (2 * (1 - ε ^ 2 * (ε ^ 2 * t ^ 2)) * V t) t) (hU0 : U 0 = 1) (hU₁0 : U₁ 0 = 0) (hV₁0 : V₁ 0 = 1) (hY : ∀ t ∈ Set.Icc a b, HasDerivAt Y (Y₁ t + f t) t) (hfluxY : ∀ t ∈ Set.Icc a b, HasDerivAt (fun (s : ℝ) => (1 + (ε ^ 2 * s ^ 2) ^ 2) * Y₁ s) (2 * (1 - ε ^ 2 * (ε ^ 2 * t ^ 2)) * Y t + (1 + (ε ^ 2 * t ^ 2) ^ 2) * g t) t) (hZ : ∀ t ∈ Set.Icc a b, HasDerivAt Z (Z₁ t) t) (hfluxZ : ∀ t ∈ Set.Icc a b, HasDerivAt (fun (s : ℝ) => (1 + (ε ^ 2 * s ^ 2) ^ 2) * Z₁ s) (2 * (1 - ε ^ 2 * (ε ^ 2 * t ^ 2)) * Z t) t) (hfc : ContinuousOn f (Set.Icc a b)) (hgc : ContinuousOn g (Set.Icc a b)) (hforcing : ∀ t ∈ Set.Icc a b, |f t| + |g t| ≤ δ * (|Y t| + |Y₁ t|)) (t : ℝ) : t ∈ Set.Icc a b → |Y t - Z t| + |Y₁ t - Z₁ t| ≤ 20 * Θ ^ 8 * (U t / U a) * (|Y a - Z a| + |Y₁ a - Z₁ a|) + 800 * δ * Θ ^ 17 * (U t / U a) * (|Y a| + |Y₁ a|)

Quantitative difference from an ideal solution. A perturbation of size δ = O(e Θ^12) produces the source's O(e Θ^29) relative error.

theorem EulerPacketPerturbation.equation30_relative_error_order29 {ε Θ b e lam : ℝ} {U U₁ V V₁ Y Y₁ Z Z₁ f g : ℝ → ℝ} (hε : 0 < ε) (hεsmall : ε ≤ 1 / 4) (hΘ : 1 ≤ Θ) (hb0 : 0 ≤ b) (hb : b ≤ Θ) (he : 0 ≤ e) (hlam : 0 ≤ lam) (hsmall : 40 * e * Θ ^ 21 ≤ 1) (hU : ∀ (t : ℝ), 0 ≤ t → HasDerivAt U (U₁ t) t) (hV : ∀ (t : ℝ), 0 ≤ t → HasDerivAt V (V₁ t) t) (hfluxU : ∀ (t : ℝ), 0 ≤ t → HasDerivAt (fun (s : ℝ) => (1 + (ε ^ 2 * s ^ 2) ^ 2) * U₁ s) (2 * (1 - ε ^ 2 * (ε ^ 2 * t ^ 2)) * U t) t) (hfluxV : ∀ (t : ℝ), 0 ≤ t → HasDerivAt (fun (s : ℝ) => (1 + (ε ^ 2 * s ^ 2) ^ 2) * V₁ s) (2 * (1 - ε ^ 2 * (ε ^ 2 * t ^ 2)) * V t) t) (hU0 : U 0 = 1) (hU₁0 : U₁ 0 = 0) (hV₁0 : V₁ 0 = 1) (hY : ∀ t ∈ Set.Icc 0 b, HasDerivAt Y (Y₁ t + f t) t) (hfluxY : ∀ t ∈ Set.Icc 0 b, HasDerivAt (fun (s : ℝ) => (1 + (ε ^ 2 * s ^ 2) ^ 2) * Y₁ s) (2 * (1 - ε ^ 2 * (ε ^ 2 * t ^ 2)) * Y t + (1 + (ε ^ 2 * t ^ 2) ^ 2) * g t) t) (hZ : ∀ t ∈ Set.Icc 0 b, HasDerivAt Z (Z₁ t) t) (hfluxZ : ∀ t ∈ Set.Icc 0 b, HasDerivAt (fun (s : ℝ) => (1 + (ε ^ 2 * s ^ 2) ^ 2) * Z₁ s) (2 * (1 - ε ^ 2 * (ε ^ 2 * t ^ 2)) * Z t) t) (hY0 : Y 0 = 1) (hY₁0 : Y₁ 0 = lam) (hZ0 : Z 0 = 1) (hZ₁0 : Z₁ 0 = lam) (hfc : ContinuousOn f (Set.Icc 0 b)) (hgc : ContinuousOn g (Set.Icc 0 b)) (hforcing : ∀ t ∈ Set.Icc 0 b, |f t| + |g t| ≤ e * Θ ^ 12 * (|Y t| + |Y₁ t|)) (t : ℝ) : t ∈ Set.Icc 0 b → |Y t - Z t| + |Y₁ t - Z₁ t| ≤ 800 * e * Θ ^ 29 * (1 + lam) * U t

The explicit Θ^29 relative error bound in the source's normalization. Its Θ^21 smallness condition follows from the exact Duhamel argument above.