The actual pressure-projected quadratic source passes to uniform Sobolev path limits.

noncomputable def EulerQuadraticSourceLimit.sourcePath {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] {T : ℝ} (C : EulerQuadraticSource.Coefficients (↑(Set.Icc 0 T)) X Y) (u : C(↑(Set.Icc 0 T), X)) : C(↑(Set.Icc 0 T), Y)

The literal quadratic source evaluated along an actual continuous state path.

Equations

• EulerQuadraticSourceLimit.sourcePath C u = EulerVolterraConvolution.pathNonlinearity T C.apply ⋯ u

theorem EulerQuadraticSourceLimit.sourcePath_sub_bound {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] {T : ℝ} (C : EulerQuadraticSource.Coefficients (↑(Set.Icc 0 T)) X Y) (R : ℝ) (hR : 0 ≤ R) (u v : C(↑(Set.Icc 0 T), X)) (hu : ‖u‖ ≤ R) (hv : ‖v‖ ≤ R) : ‖sourcePath C u - sourcePath C v‖ ≤ C.ballLipschitz R * ‖u - v‖

The actual nonlinear source map obeys the proved ball Lipschitz bound in uniform path norm.

theorem EulerQuadraticSourceLimit.sourcePath_tendsto {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] {T : ℝ} (C : EulerQuadraticSource.Coefficients (↑(Set.Icc 0 T)) X Y) (R : ℝ) (hR : 0 ≤ R) (u : ℕ → C(↑(Set.Icc 0 T), X)) (v : C(↑(Set.Icc 0 T), X)) (hu : ∀ (n : ℕ), ‖u n‖ ≤ R) (hv : ‖v‖ ≤ R) (h : Filter.Tendsto u Filter.atTop (nhds v)) : Filter.Tendsto (fun (n : ℕ) => sourcePath C (u n)) Filter.atTop (nhds (sourcePath C v))

Uniform convergence of actual bounded state paths gives uniform convergence of the literal quadratic source paths.