Exact nonlinear correction differences and their genuine L² lower-order bounds.
Actual L² bounds for the lower-order difference terms in nonlinear transport.
theorem
EulerSobolevL2Stability.scalarProduct_reverse_norm
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
(hq : 3 ≤ q)
(L : EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ)
(u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period q))
:
‖EulerSobolevL2Product.scalarProduct period hq L u (EulerCylinderSobolevSpace.value period v)‖ ≤ ‖L‖ * EulerCylinderSobolevSpace.sobolevEmbeddingConstant period q * ‖v‖ * ‖EulerCylinderSobolevSpace.value period u‖
The actual scalar-vector product is L² bounded in its first input when the second input has three Sobolev derivatives.
theorem
EulerSobolevL2Stability.transport_reverse_norm
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
(hq : 6 ≤ q)
(L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ)
(hL : ∀ (i : Fin 4), ‖L i‖ ≤ 1)
(u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))
:
‖EulerCylinderSobolevSpace.value period (((EulerSobolevTransport.transportBilinear period hq L hL) u) v)‖ ≤ 4 * EulerCylinderSobolevSpace.sobolevEmbeddingConstant period q * ‖v‖ * ‖EulerCylinderSobolevSpace.value period u‖
Actual nonlinear transport is L² bounded in its advecting input by one higher Sobolev norm of the advected input.
theorem
EulerSobolevL2Stability.coordinate_coefficient_norm
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
(hq : 6 ≤ q)
(C : EulerSpatialSobolevInverse.SmoothCoefficient period)
(K : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection q C)
(i : Fin 3)
(u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))
:
‖EulerCylinderSobolevSpace.value period
((EulerSobolevCoefficientPressure.coefficientSobolevOperator period K)
(((EulerCorrectionOperators.coordinateProduct period hq i) u) v))‖ ≤ ↑C.bound * EulerCylinderSobolevSpace.sobolevEmbeddingConstant period q * ‖u‖ * ‖EulerCylinderSobolevSpace.value period v‖
A genuine coefficient-weighted coordinate product is L² bounded in the vector factor.
theorem
EulerSobolevL2Stability.coordinate_coefficient_reverse_norm
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
(hq : 6 ≤ q)
(C : EulerSpatialSobolevInverse.SmoothCoefficient period)
(K : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection q C)
(i : Fin 3)
(u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))
:
‖EulerCylinderSobolevSpace.value period
((EulerSobolevCoefficientPressure.coefficientSobolevOperator period K)
(((EulerCorrectionOperators.coordinateProduct period hq i) u) v))‖ ≤ ↑C.bound * EulerCylinderSobolevSpace.sobolevEmbeddingConstant period q * ‖v‖ * ‖EulerCylinderSobolevSpace.value period u‖
A genuine coefficient-weighted coordinate product is also L² bounded in its scalar factor.
noncomputable def
EulerCorrectionDifference.differenceRemainder
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
{T : Type u_1}
[TopologicalSpace T]
(D : EulerCorrectionOperators.CorrectionData period q T)
(hq : 6 ≤ q)
(t : T)
(u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))
:
↥(EulerCylinderSobolevSpace.SobolevSpace period q)
The actual lower-order part of the difference of two correction equations.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerCorrectionDifference.sub_linearize_expansion
{X : Type u_1}
{Y : Type u_2}
{Z : Type u_3}
[NormedAddCommGroup X]
[NormedSpace ℝ X]
[NormedAddCommGroup Y]
[NormedSpace ℝ Y]
[NormedAddCommGroup Z]
[NormedSpace ℝ Z]
(B₁ B₂ : X →L[ℝ] X →L[ℝ] Y)
(C : Z →L[ℝ] Y)
(S : X →L[ℝ] Z)
(r : Y)
(z u v : X)
:
The difference of two quadratic sources linearized about z, for a bilinear map B₁ + B₂ and
a composite linear map C ∘ S, in abstract normed spaces.
theorem
EulerCorrectionDifference.rawSource_sub
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
{T : Type u_1}
[TopologicalSpace T]
(D : EulerCorrectionOperators.CorrectionData period q T)
(hq : 6 ≤ q)
(t : T)
(u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))
:
EulerCorrectionOperators.CorrectionData.rawSource period D hq t u - EulerCorrectionOperators.CorrectionData.rawSource period D hq t v = ((EulerSobolevTransport.transportBilinear period hq (EulerSobolevTransport.velocityComponents D.κ D.direction) ⋯)
(D.approximation t + u))
(u - v) + differenceRemainder period D hq t u v
Exact bilinear subtraction exposes one cancellable top transport and the actual lower-order difference.
theorem
EulerCorrectionDifference.algebraic_norm
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
(hq : 6 ≤ q)
(C : Fin 3 → EulerSpatialSobolevInverse.SmoothCoefficient period)
(K : (i : Fin 3) → EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection q (C i))
(u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))
:
‖EulerCylinderSobolevSpace.value period
(((EulerCorrectionOperators.algebraicBilinear period hq fun (i : Fin 3) =>
EulerSobolevCoefficientPressure.coefficientSobolevOperator period (K i))
u)
v)‖ ≤ (∑ i : Fin 3, ↑(C i).bound) * EulerCylinderSobolevSpace.sobolevEmbeddingConstant period q * ‖u‖ * ‖EulerCylinderSobolevSpace.value period v‖
The actual algebraic quadratic term has an L² bound in its second input.
theorem
EulerCorrectionDifference.algebraic_reverse_norm
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
(hq : 6 ≤ q)
(C : Fin 3 → EulerSpatialSobolevInverse.SmoothCoefficient period)
(K : (i : Fin 3) → EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection q (C i))
(u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))
:
‖EulerCylinderSobolevSpace.value period
(((EulerCorrectionOperators.algebraicBilinear period hq fun (i : Fin 3) =>
EulerSobolevCoefficientPressure.coefficientSobolevOperator period (K i))
u)
v)‖ ≤ (∑ i : Fin 3, ↑(C i).bound) * EulerCylinderSobolevSpace.sobolevEmbeddingConstant period q * ‖v‖ * ‖EulerCylinderSobolevSpace.value period u‖
The same actual algebraic quadratic term has an L² bound in its first input.
theorem
EulerCorrectionDifference.differenceRemainder_norm
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
{T : Type u_1}
[TopologicalSpace T]
(D : EulerCorrectionOperators.CorrectionData period q T)
(hq : 6 ≤ q)
(t : T)
(u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))
:
‖EulerCylinderSobolevSpace.value period (differenceRemainder period D hq t u v)‖ ≤ (↑(D.linear.coefficient t).bound + 4 * EulerCylinderSobolevSpace.sobolevEmbeddingConstant period q * ‖D.approximation t + v‖ + (∑ i : Fin 3, ↑((D.quadratic i).coefficient t).bound) * EulerCylinderSobolevSpace.sobolevEmbeddingConstant period q * (‖D.approximation t + u‖ + ‖D.approximation t + v‖)) * ‖EulerCylinderSobolevSpace.value period (u - v)‖
The actual lower-order nonlinear difference is Lipschitz in L² with only fixed higher Sobolev norms in the coefficient.