Actual coefficient multiplication and the coercive projected pressure inverse as Sobolev CLMs.

theorem EulerSobolevCoefficientPressure.sumNorm_ofJet (period : ℝ) [Fact (0 < period)] {q : ℕ} {f : ↥(EulerLiftedGradientSpace.LiftL2 period)} (J : EulerSpatialSobolevInverse.SpatialJet period EulerCylinderSobolev.standardDirection q f) : EulerCylinderSobolevSpace.sumNorm period (EulerCylinderSobolevSpace.ofJet period J) = J.sobolevNorm

A genuine jet has exactly its source derivative-sum norm when regarded as a complete Sobolev element.

noncomputable def EulerSobolevCoefficientPressure.jetLift (period : ℝ) [Fact (0 < period)] {q : ℕ} (A : ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)) (Jmap : {f : ↥(EulerLiftedGradientSpace.LiftL2 period)} → EulerSpatialSobolevInverse.SpatialJet period EulerCylinderSobolev.standardDirection q f → EulerSpatialSobolevInverse.SpatialJet period EulerCylinderSobolev.standardDirection q (A f)) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)

An L² operator with a genuine derivative-jet construction acts on the complete Sobolev space.

Equations

• EulerSobolevCoefficientPressure.jetLift period A Jmap u = EulerCylinderSobolevSpace.ofJet period (Jmap (EulerCylinderSobolevSpace.toJet period u))

@[simp]

theorem EulerSobolevCoefficientPressure.jetLift_value (period : ℝ) [Fact (0 < period)] {q : ℕ} (A : ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)) (Jmap : {f : ↥(EulerLiftedGradientSpace.LiftL2 period)} → EulerSpatialSobolevInverse.SpatialJet period EulerCylinderSobolev.standardDirection q f → EulerSpatialSobolevInverse.SpatialJet period EulerCylinderSobolev.standardDirection q (A f)) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : EulerCylinderSobolevSpace.value period (jetLift period A (fun {f : ↥(EulerLiftedGradientSpace.LiftL2 period)} => Jmap) u) = A (EulerCylinderSobolevSpace.value period u)

The jet lift has exactly the original L² value.

theorem EulerSobolevCoefficientPressure.jetLift_bound (period : ℝ) [Fact (0 < period)] {q : ℕ} (A : ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)) (Jmap : {f : ↥(EulerLiftedGradientSpace.LiftL2 period)} → EulerSpatialSobolevInverse.SpatialJet period EulerCylinderSobolev.standardDirection q f → EulerSpatialSobolevInverse.SpatialJet period EulerCylinderSobolev.standardDirection q (A f)) (C : ℝ) (hC : 0 ≤ C) (hJ : ∀ {f : ↥(EulerLiftedGradientSpace.LiftL2 period)} (J : EulerSpatialSobolevInverse.SpatialJet period EulerCylinderSobolev.standardDirection q f), (Jmap J).sobolevNorm ≤ C * J.sobolevNorm) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : ‖jetLift period A (fun {f : ↥(EulerLiftedGradientSpace.LiftL2 period)} => Jmap) u‖ ≤ C * ↑(Fintype.card (EulerCylinderSobolevSpace.SobolevWord q)) * ‖u‖

The actual jet estimate controls the complete Sobolev operator norm.

noncomputable def EulerSobolevCoefficientPressure.jetLiftLinearMap (period : ℝ) [Fact (0 < period)] (q : ℕ) (A : ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)) (Jmap : {f : ↥(EulerLiftedGradientSpace.LiftL2 period)} → EulerSpatialSobolevInverse.SpatialJet period EulerCylinderSobolev.standardDirection q f → EulerSpatialSobolevInverse.SpatialJet period EulerCylinderSobolev.standardDirection q (A f)) : ↥(EulerCylinderSobolevSpace.SobolevSpace period q) →ₗ[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period q)

Uniqueness of derivative arrays makes a genuine L² jet lift linear.

Equations

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

noncomputable def EulerSobolevCoefficientPressure.jetLiftOperator (period : ℝ) [Fact (0 < period)] (q : ℕ) (A : ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)) (Jmap : {f : ↥(EulerLiftedGradientSpace.LiftL2 period)} → EulerSpatialSobolevInverse.SpatialJet period EulerCylinderSobolev.standardDirection q f → EulerSpatialSobolevInverse.SpatialJet period EulerCylinderSobolev.standardDirection q (A f)) (C : ℝ) (hC : 0 ≤ C) (hJ : ∀ {f : ↥(EulerLiftedGradientSpace.LiftL2 period)} (J : EulerSpatialSobolevInverse.SpatialJet period EulerCylinderSobolev.standardDirection q f), (Jmap J).sobolevNorm ≤ C * J.sobolevNorm) : ↥(EulerCylinderSobolevSpace.SobolevSpace period q) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period q)

The bounded continuous lift of an actual L² operator with proved derivative-jet estimates.

Equations

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

noncomputable def EulerSobolevCoefficientPressure.coefficientSobolevOperator (period : ℝ) [Fact (0 < period)] {q : ℕ} {A : EulerSpatialSobolevInverse.SmoothCoefficient period} (K : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection q A) : ↥(EulerCylinderSobolevSpace.SobolevSpace period q) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period q)

Actual multiplication by a smooth bounded coefficient, as a Sobolev continuous linear map.

Equations

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

@[simp]

theorem EulerSobolevCoefficientPressure.coefficientSobolevOperator_value (period : ℝ) [Fact (0 < period)] {q : ℕ} {A : EulerSpatialSobolevInverse.SmoothCoefficient period} (K : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection q A) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : EulerCylinderSobolevSpace.value period ((coefficientSobolevOperator period K) u) = A.operator (EulerCylinderSobolevSpace.value period u)

The coefficient Sobolev operator is represented by literal pointwise coefficient multiplication.

noncomputable def EulerSobolevCoefficientPressure.pressureL2Operator (period : ℝ) [Fact (0 < period)] (A : EulerSpatialSobolevInverse.SmoothCoefficient period) (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (c : ℝ) (hc : 0 < c) (hpos : ∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3), c * ‖v‖ ^ 2 ≤ inner ℝ ((A.coefficient x) v) v) : ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)

The existing Lax–Milgram pressure inverse as an ambient L² continuous linear map.

Equations

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

@[simp]

theorem EulerSobolevCoefficientPressure.pressureL2Operator_apply (period : ℝ) [Fact (0 < period)] (A : EulerSpatialSobolevInverse.SmoothCoefficient period) (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (c : ℝ) (hc : 0 < c) (hpos : ∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3), c * ‖v‖ ^ 2 ≤ inner ℝ ((A.coefficient x) v) v) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : (pressureL2Operator period A κ m c hc hpos) f = A.pressure κ m c hc hpos f

The bounded L² pressure operator agrees with the already constructed actual coercive pressure.

noncomputable def EulerSobolevCoefficientPressure.pressureSobolevOperator (period : ℝ) [Fact (0 < period)] {q : ℕ} {A : EulerSpatialSobolevInverse.SmoothCoefficient period} (K : 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) : ↥(EulerCylinderSobolevSpace.SobolevSpace period q) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period q)

The genuine coercive projected pressure inverse is a bounded map on every finite Sobolev space.

Equations

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

@[simp]

theorem EulerSobolevCoefficientPressure.pressureSobolevOperator_value (period : ℝ) [Fact (0 < period)] {q : ℕ} {A : EulerSpatialSobolevInverse.SmoothCoefficient period} (K : 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 q)) : EulerCylinderSobolevSpace.value period ((pressureSobolevOperator period K κ m c hc hpos) u) = A.pressure κ m c hc hpos (EulerCylinderSobolevSpace.value period u)

The Sobolev pressure is exactly the actual coercive L² pressure on underlying fields.

theorem EulerSobolevCoefficientPressure.pressureSobolevOperator_bound (period : ℝ) [Fact (0 < period)] {q : ℕ} {A : EulerSpatialSobolevInverse.SmoothCoefficient period} (K : 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 q)) : ‖(pressureSobolevOperator period K κ m c hc hpos) u‖ ≤ K.pressureConstant c * ↑(Fintype.card (EulerCylinderSobolevSpace.SobolevWord q)) * ‖u‖

The explicit finite-order pressure bound on the complete Sobolev norm.

noncomputable def EulerSobolevCoefficientPressure.projectedSourceOperator (period : ℝ) [Fact (0 < period)] {q : ℕ} {A : EulerSpatialSobolevInverse.SmoothCoefficient period} (K : 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) : ↥(EulerCylinderSobolevSpace.SobolevSpace period q) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period q)

Subtracting the actual coefficient-weighted pressure defines the projected Euler forcing.

Equations

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

@[simp]

theorem EulerSobolevCoefficientPressure.projectedSourceOperator_value (period : ℝ) [Fact (0 < period)] {q : ℕ} {A : EulerSpatialSobolevInverse.SmoothCoefficient period} (K : 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 q)) : EulerCylinderSobolevSpace.value period ((projectedSourceOperator period K κ m c hc hpos) u) = EulerCylinderSobolevSpace.value period u - A.operator (A.pressure κ m c hc hpos (EulerCylinderSobolevSpace.value period u))

The projected forcing has the literal pressure-corrected L² value.

theorem EulerSobolevCoefficientPressure.projectedSource_gradient_zero (period : ℝ) [Fact (0 < period)] {q : ℕ} {A : EulerSpatialSobolevInverse.SmoothCoefficient period} (K : 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 q)) : (EulerLiftedGradientSpace.gradientProjection period κ m) (EulerCylinderSobolevSpace.value period ((projectedSourceOperator period K κ m c hc hpos) u)) = 0

The actual pressure correction cancels the lifted gradient projection of the source.