Exact resolvent identities for the actual coercive pressure operators on complete Sobolev spaces.

@[simp]

theorem EulerSobolevCoefficientPressure.value_add (period : ℝ) [Fact (0 < period)] {q : ℕ} (u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : EulerCylinderSobolevSpace.value period (u + v) = EulerCylinderSobolevSpace.value period u + EulerCylinderSobolevSpace.value period v

Underlying L² evaluation respects addition of complete Sobolev elements.

@[simp]

theorem EulerSobolevCoefficientPressure.value_sub (period : ℝ) [Fact (0 < period)] {q : ℕ} (u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : EulerCylinderSobolevSpace.value period (u - v) = EulerCylinderSobolevSpace.value period u - EulerCylinderSobolevSpace.value period v

Underlying L² evaluation respects subtraction of complete Sobolev elements.

theorem EulerSobolevCoefficientPressure.pressureSobolev_mem_gradient (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) ∈ EulerLiftedGradientSpace.gradientSpace period κ m

Every actual Sobolev pressure takes values in the closed lifted gradient space.

theorem EulerSobolevCoefficientPressure.pressureSobolev_equation (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) (A.operator (EulerCylinderSobolevSpace.value period ((pressureSobolevOperator period K κ m c hc hpos) u))) = (EulerLiftedGradientSpace.gradientProjection period κ m) (EulerCylinderSobolevSpace.value period u)

The actual Sobolev pressure solves the original projected coefficient equation.

theorem EulerSobolevCoefficientPressure.pressureSobolev_unique (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 p : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) (hp : EulerCylinderSobolevSpace.value period p ∈ EulerLiftedGradientSpace.gradientSpace period κ m) (heq : (EulerLiftedGradientSpace.gradientProjection period κ m) (A.operator (EulerCylinderSobolevSpace.value period p)) = (EulerLiftedGradientSpace.gradientProjection period κ m) (EulerCylinderSobolevSpace.value period u)) : p = (pressureSobolevOperator period K κ m c hc hpos) u

Uniqueness of the Lax–Milgram solution gives uniqueness in the complete Sobolev space.

theorem EulerSobolevCoefficientPressure.projectedSource_divergenceFree (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) ∈ EulerLiftedGradientSpace.divergenceFreeSpace period κ m

The actual projected forcing lies in the lifted divergence-free space.

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

The difference of actual coefficient multipliers has the expected underlying L² action.

theorem EulerSobolevCoefficientPressure.pressureL2_resolvent_apply (period : ℝ) [Fact (0 < period)] (A B : EulerSpatialSobolevInverse.SmoothCoefficient period) (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (c d : ℝ) (hc : 0 < c) (hd : 0 < d) (hA : ∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3), c * ‖v‖ ^ 2 ≤ inner ℝ ((A.coefficient x) v) v) (hB : ∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3), d * ‖v‖ ^ 2 ≤ inner ℝ ((B.coefficient x) v) v) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : A.pressure κ m c hc hA f - B.pressure κ m d hd hB f = A.pressure κ m c hc hA ((B.operator - A.operator) (B.pressure κ m d hd hB f))

The coercive L² pressure satisfies the exact resolvent formula by uniqueness of its projected equation.

theorem EulerSobolevCoefficientPressure.pressure_resolvent_apply (period : ℝ) [Fact (0 < period)] {q : ℕ} {A B : EulerSpatialSobolevInverse.SmoothCoefficient period} (KA : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection q A) (KB : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection q B) (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (c d : ℝ) (hc : 0 < c) (hd : 0 < d) (hA : ∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3), c * ‖v‖ ^ 2 ≤ inner ℝ ((A.coefficient x) v) v) (hB : ∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3), d * ‖v‖ ^ 2 ≤ inner ℝ ((B.coefficient x) v) v) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : (pressureSobolevOperator period KA κ m c hc hA) u - (pressureSobolevOperator period KB κ m d hd hB) u = (pressureSobolevOperator period KA κ m c hc hA) ((coefficientSobolevOperator period KB - coefficientSobolevOperator period KA) ((pressureSobolevOperator period KB κ m d hd hB) u))

The genuine Sobolev pressure inverses obey the exact resolvent identity on every forcing.

theorem EulerSobolevCoefficientPressure.pressure_resolvent (period : ℝ) [Fact (0 < period)] {q : ℕ} {A B : EulerSpatialSobolevInverse.SmoothCoefficient period} (KA : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection q A) (KB : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection q B) (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (c d : ℝ) (hc : 0 < c) (hd : 0 < d) (hA : ∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3), c * ‖v‖ ^ 2 ≤ inner ℝ ((A.coefficient x) v) v) (hB : ∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3), d * ‖v‖ ^ 2 ≤ inner ℝ ((B.coefficient x) v) v) : pressureSobolevOperator period KA κ m c hc hA - pressureSobolevOperator period KB κ m d hd hB = pressureSobolevOperator period KA κ m c hc hA ∘SL (coefficientSobolevOperator period KB - coefficientSobolevOperator period KA) ∘SL pressureSobolevOperator period KB κ m d hd hB

The genuine pressure resolvent identity as an equality of Sobolev continuous linear maps.

theorem EulerSobolevCoefficientPressure.pressure_resolvent_bound (period : ℝ) [Fact (0 < period)] {q : ℕ} {A B : EulerSpatialSobolevInverse.SmoothCoefficient period} (KA : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection q A) (KB : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection q B) (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (c d : ℝ) (hc : 0 < c) (hd : 0 < d) (hA : ∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3), c * ‖v‖ ^ 2 ≤ inner ℝ ((A.coefficient x) v) v) (hB : ∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3), d * ‖v‖ ^ 2 ≤ inner ℝ ((B.coefficient x) v) v) : ‖pressureSobolevOperator period KA κ m c hc hA - pressureSobolevOperator period KB κ m d hd hB‖ ≤ ‖pressureSobolevOperator period KA κ m c hc hA‖ * ‖coefficientSobolevOperator period KB - coefficientSobolevOperator period KA‖ * ‖pressureSobolevOperator period KB κ m d hd hB‖

The norm of the genuine pressure difference is controlled by the coefficient multiplier difference.