Exact consistency of actual products, transport, and pressure across the Sobolev scale.

@[instance_reducible]

noncomputable def EulerSobolevNonlinearCompatibility.nonlinearCompatGroup (period : ℝ) [Fact (0 < period)] (q : ℕ) : NormedAddCommGroup ↥(EulerCylinderSobolevSpace.SobolevSpace period q)

Cache the standard NormedAddCommGroup (SobolevSpace period q) instance to shorten typeclass synthesis.

Equations

• EulerSobolevNonlinearCompatibility.nonlinearCompatGroup period q = inferInstance

@[instance_reducible]

noncomputable def EulerSobolevNonlinearCompatibility.nonlinearCompatSpace (period : ℝ) [Fact (0 < period)] (q : ℕ) : NormedSpace ℝ ↥(EulerCylinderSobolevSpace.SobolevSpace period q)

Cache the standard NormedSpace ℝ (SobolevSpace period q) instance to shorten typeclass synthesis.

Equations

• EulerSobolevNonlinearCompatibility.nonlinearCompatSpace period q = inferInstance

@[instance_reducible]

noncomputable def EulerSobolevNonlinearCompatibility.nonlinearCompatBilinearGroup (period : ℝ) [Fact (0 < period)] (q : ℕ) : SeminormedAddCommGroup (↥(EulerCylinderSobolevSpace.SobolevSpace period q) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period q) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period q))

Cache the standard SeminormedAddCommGroup (SobolevSpace period q →L[ℝ] SobolevSpace period q →L[ℝ] SobolevSpace period q) instance to shorten typeclass synthesis.

Equations

• EulerSobolevNonlinearCompatibility.nonlinearCompatBilinearGroup period q = inferInstance

theorem EulerSobolevNonlinearCompatibility.restrict_productHq (period : ℝ) [Fact (0 < period)] {p q : ℕ} (hp : 6 ≤ p) (hq : 6 ≤ q) (hqp : q ≤ p) (L : EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ‖L‖ ≤ 1) (u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period p)) : (EulerCylinderSobolevSpace.restrictOperator period hqp) (EulerSobolevL2Product.productHq period hp L hL u v) = EulerSobolevL2Product.productHq period hq L hL ((EulerCylinderSobolevSpace.restrictOperator period hqp) u) ((EulerCylinderSobolevSpace.restrictOperator period hqp) v)

Actual Sobolev products restrict to the same pointwise product at every lower algebra level.

theorem EulerSobolevNonlinearCompatibility.restrict_asymmetricTransport (period : ℝ) [Fact (0 < period)] {p q : ℕ} (hp : 6 ≤ p) (hq : 6 ≤ q) (hqp : q ≤ p) (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ∀ (i : Fin 4), ‖L i‖ ≤ 1) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period p)) (v : ↥(EulerCylinderSobolevSpace.SobolevSpace period (p + 1))) : (EulerCylinderSobolevSpace.restrictOperator period hqp) (((EulerAsymmetricTransport.asymmetricTransport period hp L hL) u) v) = ((EulerAsymmetricTransport.asymmetricTransport period hq L hL) ((EulerCylinderSobolevSpace.restrictOperator period hqp) u)) ((EulerCylinderSobolevSpace.restrictOperator period ⋯) v)

Actual asymmetric transport restricts to the identical lower-order nonlinear field.

theorem EulerSobolevNonlinearCompatibility.restrict_coefficient (period : ℝ) [Fact (0 < period)] {p q : ℕ} (hqp : q ≤ p) {A : EulerSpatialSobolevInverse.SmoothCoefficient period} (KP : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection p A) (KQ : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection q A) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period p)) : (EulerCylinderSobolevSpace.restrictOperator period hqp) ((EulerSobolevCoefficientPressure.coefficientSobolevOperator period KP) u) = (EulerSobolevCoefficientPressure.coefficientSobolevOperator period KQ) ((EulerCylinderSobolevSpace.restrictOperator period hqp) u)

The genuine pointwise coefficient action is independent of the chosen Sobolev order.

theorem EulerSobolevNonlinearCompatibility.restrict_pressure (period : ℝ) [Fact (0 < period)] {p q : ℕ} (hqp : q ≤ p) {A : EulerSpatialSobolevInverse.SmoothCoefficient period} (KP : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection p A) (KQ : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection q A) (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (c : ℝ) (hc : 0 < c) (hpos : ∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3), c * ‖v‖ ^ 2 ≤ inner ℝ ((A.coefficient x) v) v) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period p)) : (EulerCylinderSobolevSpace.restrictOperator period hqp) ((EulerSobolevCoefficientPressure.pressureSobolevOperator period KP κ m c hc hpos) u) = (EulerSobolevCoefficientPressure.pressureSobolevOperator period KQ κ m c hc hpos) ((EulerCylinderSobolevSpace.restrictOperator period hqp) u)

The actual coercive pressure solve agrees at every Sobolev order by its unique L² value.

theorem EulerSobolevNonlinearCompatibility.restrict_projectedSource (period : ℝ) [Fact (0 < period)] {p q : ℕ} (hqp : q ≤ p) {A : EulerSpatialSobolevInverse.SmoothCoefficient period} (KP : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection p A) (KQ : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection q A) (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (c : ℝ) (hc : 0 < c) (hpos : ∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3), c * ‖v‖ ^ 2 ≤ inner ℝ ((A.coefficient x) v) v) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period p)) : (EulerCylinderSobolevSpace.restrictOperator period hqp) ((EulerSobolevCoefficientPressure.projectedSourceOperator period KP κ m c hc hpos) u) = (EulerSobolevCoefficientPressure.projectedSourceOperator period KQ κ m c hc hpos) ((EulerCylinderSobolevSpace.restrictOperator period hqp) u)

The projected Euler forcing is exactly consistent across the finite Sobolev scale.

noncomputable def EulerSobolevNonlinearCompatibility.algebraicAtBilinear (period : ℝ) [Fact (0 < period)] {s : ℕ} (hs : 6 ≤ s) (C : Fin 3 → ↥(EulerCylinderSobolevSpace.SobolevSpace period s) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) : ↥(EulerCylinderSobolevSpace.SobolevSpace period s) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period s) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period s)

The actual order-zero algebraic term as a bilinear map on one complete Sobolev level.

Equations

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

theorem EulerSobolevNonlinearCompatibility.algebraicAtBilinear_apply (period : ℝ) [Fact (0 < period)] {s : ℕ} (hs : 6 ≤ s) (C : Fin 3 → ↥(EulerCylinderSobolevSpace.SobolevSpace period s) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) (u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) : ((algebraicAtBilinear period hs C) u) v = EulerGevreyOrderZero.algebraicAt period hs C u v

This bilinear map is precisely the already bounded order-zero Euler term.