Continuous coefficient data for the correction source, with proved uniform ball bounds.

Quantitative bounds for the actual projected linear-plus-quadratic source of the correction equation.

def EulerQuadraticSource.source {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] (P : Y →L[ℝ] Y) (r : Y) (A : X →L[ℝ] Y) (B : X →L[ℝ] X →L[ℝ] Y) (u : X) : Y

A pressure-projected source with actual forcing, linear terms, and quadratic terms.

Equations

• EulerQuadraticSource.source P r A B u = -P (r + A u + (B u) u)

theorem EulerQuadraticSource.source_continuous {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] {T : Type u_3} [TopologicalSpace T] (P : T → Y →L[ℝ] Y) (r : T → Y) (A : T → X →L[ℝ] Y) (B : T → X →L[ℝ] X →L[ℝ] Y) (hP : Continuous P) (hr : Continuous r) (hA : Continuous A) (hB : Continuous B) : Continuous fun (p : T × X) => source (P p.1) (r p.1) (A p.1) (B p.1) p.2

The actual quadratic source is jointly continuous in every coefficient and its unknown.

theorem EulerQuadraticSource.quadratic_sub {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] (B : X →L[ℝ] X →L[ℝ] Y) (u v : X) : (B u) u - (B v) v = (B (u - v)) u + (B v) (u - v)

The exact product difference identity needs no symmetry of the bilinear source.

theorem EulerQuadraticSource.source_bound {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] (P : Y →L[ℝ] Y) (r : Y) (A : X →L[ℝ] Y) (B : X →L[ℝ] X →L[ℝ] Y) (R : ℝ) (hR : 0 ≤ R) (u : X) (hu : ‖u‖ ≤ R) : ‖source P r A B u‖ ≤ ‖P‖ * (‖r‖ + ‖A‖ * R + ‖B‖ * R ^ 2)

The quadratic source has the genuine pointwise bound used for Picard existence.

theorem EulerQuadraticSource.source_sub_bound {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] (P : Y →L[ℝ] Y) (r : Y) (A : X →L[ℝ] Y) (B : X →L[ℝ] X →L[ℝ] Y) (R : ℝ) (_hR : 0 ≤ R) (u v : X) (hu : ‖u‖ ≤ R) (hv : ‖v‖ ≤ R) : ‖source P r A B u - source P r A B v‖ ≤ ‖P‖ * (‖A‖ + 2 * ‖B‖ * R) * ‖u - v‖

The quadratic source is Lipschitz on each norm ball, with an explicit finite constant.

theorem EulerQuadraticSource.source_uniform_bound {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] (P : Y →L[ℝ] Y) (r : Y) (A : X →L[ℝ] Y) (B : X →L[ℝ] X →L[ℝ] Y) (p₀ r₀ a₀ b₀ R : ℝ) (hp : ‖P‖ ≤ p₀) (hr : ‖r‖ ≤ r₀) (ha : ‖A‖ ≤ a₀) (hb : ‖B‖ ≤ b₀) (hR : 0 ≤ R) (u : X) (hu : ‖u‖ ≤ R) : ‖source P r A B u‖ ≤ p₀ * (r₀ + a₀ * R + b₀ * R ^ 2)

Uniform pointwise coefficient bounds imply the actual source bound on every ball.

theorem EulerQuadraticSource.source_uniform_sub_bound {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] (P : Y →L[ℝ] Y) (r : Y) (A : X →L[ℝ] Y) (B : X →L[ℝ] X →L[ℝ] Y) (p₀ a₀ b₀ R : ℝ) (hp : ‖P‖ ≤ p₀) (ha : ‖A‖ ≤ a₀) (hb : ‖B‖ ≤ b₀) (hR : 0 ≤ R) (u v : X) (hu : ‖u‖ ≤ R) (hv : ‖v‖ ≤ R) : ‖source P r A B u - source P r A B v‖ ≤ p₀ * (a₀ + 2 * b₀ * R) * ‖u - v‖

Uniform coefficient bounds imply the required local Lipschitz constant.

structure EulerQuadraticSource.Coefficients (T : Type u_4) [TopologicalSpace T] (X : Type u_5) (Y : Type u_6) [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] : Type (max (max u_4 u_5) u_6)

Actual continuous data for the pressure-projected quadratic source.

• projection : C(T, Y →L[ℝ] Y)

  Projection of Coefficients, of type C(T, Y →L[ℝ] Y).

• forcing : C(T, Y)

  Forcing of Coefficients, of type C(T, Y).

• linear : C(T, X →L[ℝ] Y)

  Linear of Coefficients, of type C(T, X →L[ℝ] Y).

• quadratic : C(T, X →L[ℝ] X →L[ℝ] Y)

  Quadratic of Coefficients, of type C(T, X →L[ℝ] X →L[ℝ] Y).

def EulerQuadraticSource.Coefficients.apply {X : Type u_1} {Y : Type u_2} {T : Type u_3} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] [TopologicalSpace T] (C : Coefficients T X Y) (t : T) (u : X) : Y

Evaluate the genuine projected source.

Equations

• C.apply t u = EulerQuadraticSource.source (C.projection t) (C.forcing t) (C.linear t) (C.quadratic t) u

theorem EulerQuadraticSource.Coefficients.continuous {X : Type u_1} {Y : Type u_2} {T : Type u_3} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] [TopologicalSpace T] (C : Coefficients T X Y) : Continuous fun (p : T × X) => C.apply p.1 p.2

The source is jointly continuous in time and the Sobolev unknown.

noncomputable def EulerQuadraticSource.Coefficients.comp {X : Type u_1} {Y : Type u_2} {T : Type u_3} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] [TopologicalSpace T] {U : Type u_4} [TopologicalSpace U] (C : Coefficients T X Y) (f : C(U, T)) : Coefficients U X Y

Restrict coefficient data along any continuous parameter map.

Equations

• C.comp f = { projection := C.projection.comp f, forcing := C.forcing.comp f, linear := C.linear.comp f, quadratic := C.quadratic.comp f }

@[simp]

theorem EulerQuadraticSource.Coefficients.comp_apply {X : Type u_1} {Y : Type u_2} {T : Type u_3} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] [TopologicalSpace T] {U : Type u_4} [TopologicalSpace U] (C : Coefficients T X Y) (f : C(U, T)) (t : U) (u : X) : (C.comp f).apply t u = C.apply (f t) u

@[instance_reducible]

noncomputable def EulerQuadraticSource.nestedGroup {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] : SeminormedAddCommGroup (X →L[ℝ] X →L[ℝ] Y)

Cache the standard SeminormedAddCommGroup (X →L[ℝ] X →L[ℝ] Y) instance to shorten typeclass synthesis.

Equations

• EulerQuadraticSource.nestedGroup = inferInstance

noncomputable def EulerQuadraticSource.Coefficients.ballBound {X : Type u_1} {Y : Type u_2} {T : Type u_3} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] [TopologicalSpace T] [CompactSpace T] (C : Coefficients T X Y) (R : ℝ) : ℝ

A uniform norm bound for the actual source on a ball.

Equations

• C.ballBound R = ‖C.projection‖ * (‖C.forcing‖ + ‖C.linear‖ * R + ‖C.quadratic‖ * R ^ 2)

noncomputable def EulerQuadraticSource.Coefficients.ballLipschitz {X : Type u_1} {Y : Type u_2} {T : Type u_3} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] [TopologicalSpace T] [CompactSpace T] (C : Coefficients T X Y) (R : ℝ) : ℝ

A uniform Lipschitz constant for the actual source on a ball.

Equations

• C.ballLipschitz R = ‖C.projection‖ * (‖C.linear‖ + 2 * ‖C.quadratic‖ * R)

theorem EulerQuadraticSource.Coefficients.ballBound_nonneg {X : Type u_1} {Y : Type u_2} {T : Type u_3} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] [TopologicalSpace T] [CompactSpace T] (C : Coefficients T X Y) (R : ℝ) (hR : 0 ≤ R) : 0 ≤ C.ballBound R

theorem EulerQuadraticSource.Coefficients.ballLipschitz_nonneg {X : Type u_1} {Y : Type u_2} {T : Type u_3} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] [TopologicalSpace T] [CompactSpace T] (C : Coefficients T X Y) (R : ℝ) (hR : 0 ≤ R) : 0 ≤ C.ballLipschitz R

theorem EulerQuadraticSource.Coefficients.apply_bound {X : Type u_1} {Y : Type u_2} {T : Type u_3} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] [TopologicalSpace T] [CompactSpace T] (C : Coefficients T X Y) (R : ℝ) (hR : 0 ≤ R) (t : T) (u : X) (hu : ‖u‖ ≤ R) : ‖C.apply t u‖ ≤ C.ballBound R

The uniform source bound follows from actual operator norms, with no assumed nonlinear estimate.

theorem EulerQuadraticSource.Coefficients.apply_sub_bound {X : Type u_1} {Y : Type u_2} {T : Type u_3} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] [TopologicalSpace T] [CompactSpace T] (C : Coefficients T X Y) (R : ℝ) (hR : 0 ≤ R) (t : T) (u v : X) (hu : ‖u‖ ≤ R) (hv : ‖v‖ ≤ R) : ‖C.apply t u - C.apply t v‖ ≤ C.ballLipschitz R * ‖u - v‖

The uniform local Lipschitz estimate follows from the proved quadratic difference identity.