The Hilbert-space inverse used for the packet pressure equation. Invertibility is constructed from Lax--Milgram, not assumed. The coercivity hypothesis is an explicit quadratic inequality on the given bounded operator. This does not assert the Fourier or Sobolev realization of the pressure space.

noncomputable def EulerCoerciveProjection.operatorBilinear {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (T : E →L[ℝ] E) : E →L[ℝ] E →L[ℝ] ℝ

The bounded bilinear form associated with an operator and the real inner product.

Equations

• EulerCoerciveProjection.operatorBilinear T = innerSL ℝ ∘SL T

theorem EulerCoerciveProjection.operatorBilinear_coercive {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (T : E →L[ℝ] E) (c : ℝ) (hc : 0 < c) (hT : ∀ (x : E), c * ‖x‖ ^ 2 ≤ inner ℝ (T x) x) : IsCoercive (operatorBilinear T)

noncomputable def EulerCoerciveProjection.coerciveEquiv {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : E →L[ℝ] E) (c : ℝ) (hc : 0 < c) (hT : ∀ (x : E), c * ‖x‖ ^ 2 ≤ inner ℝ (T x) x) : E ≃L[ℝ] E

Lax--Milgram constructs an equivalence from the operator's coercivity.

Equations

• EulerCoerciveProjection.coerciveEquiv T c hc hT = ⋯.continuousLinearEquivOfBilin

@[simp]

theorem EulerCoerciveProjection.coerciveEquiv_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : E →L[ℝ] E) (c : ℝ) (hc : 0 < c) (hT : ∀ (x : E), c * ‖x‖ ^ 2 ≤ inner ℝ (T x) x) (x : E) : (coerciveEquiv T c hc hT) x = T x

noncomputable def EulerCoerciveProjection.coerciveInverse {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : E →L[ℝ] E) (c : ℝ) (hc : 0 < c) (hT : ∀ (x : E), c * ‖x‖ ^ 2 ≤ inner ℝ (T x) x) : E →L[ℝ] E

The inverse operator constructed from the coercive Lax–Milgram equivalence.

Equations

• EulerCoerciveProjection.coerciveInverse T c hc hT = ↑(EulerCoerciveProjection.coerciveEquiv T c hc hT).symm

@[simp]

theorem EulerCoerciveProjection.operator_inverse_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : E →L[ℝ] E) (c : ℝ) (hc : 0 < c) (hT : ∀ (x : E), c * ‖x‖ ^ 2 ≤ inner ℝ (T x) x) (y : E) : T ((coerciveInverse T c hc hT) y) = y

@[simp]

theorem EulerCoerciveProjection.inverse_operator_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : E →L[ℝ] E) (c : ℝ) (hc : 0 < c) (hT : ∀ (x : E), c * ‖x‖ ^ 2 ≤ inner ℝ (T x) x) (x : E) : (coerciveInverse T c hc hT) (T x) = x

theorem EulerCoerciveProjection.coerciveInverse_apply_norm_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : E →L[ℝ] E) (c : ℝ) (hc : 0 < c) (hT : ∀ (x : E), c * ‖x‖ ^ 2 ≤ inner ℝ (T x) x) (y : E) : ‖(coerciveInverse T c hc hT) y‖ ≤ c⁻¹ * ‖y‖

theorem EulerCoerciveProjection.coerciveInverse_norm_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : E →L[ℝ] E) (c : ℝ) (hc : 0 < c) (hT : ∀ (x : E), c * ‖x‖ ^ 2 ≤ inner ℝ (T x) x) : ‖coerciveInverse T c hc hT‖ ≤ c⁻¹

theorem EulerCoerciveProjection.coerciveInverse_resolvent {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T U : E →L[ℝ] E) (c d : ℝ) (hc : 0 < c) (hd : 0 < d) (hT : ∀ (x : E), c * ‖x‖ ^ 2 ≤ inner ℝ (T x) x) (hU : ∀ (x : E), d * ‖x‖ ^ 2 ≤ inner ℝ (U x) x) : coerciveInverse T c hc hT - coerciveInverse U d hd hU = coerciveInverse T c hc hT ∘SL (U - T) ∘SL coerciveInverse U d hd hU

The exact resolvent identity for the inverses constructed by Lax--Milgram.

theorem EulerCoerciveProjection.coerciveInverse_norm_sub_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T U : E →L[ℝ] E) (c d : ℝ) (hc : 0 < c) (hd : 0 < d) (hT : ∀ (x : E), c * ‖x‖ ^ 2 ≤ inner ℝ (T x) x) (hU : ∀ (x : E), d * ‖x‖ ^ 2 ≤ inner ℝ (U x) x) : ‖coerciveInverse T c hc hT - coerciveInverse U d hd hU‖ ≤ c⁻¹ * d⁻¹ * ‖U - T‖

noncomputable def EulerCoerciveProjection.projectedOperator {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (S : Submodule ℝ E) [CompleteSpace ↥S] (G : E →L[ℝ] E) : ↥S →L[ℝ] ↥S

Orthogonal projection of the given ambient operator, restricted to the subspace.

Equations

• EulerCoerciveProjection.projectedOperator S G = S.orthogonalProjectionOnto ∘SL G ∘SL S.subtypeL

theorem EulerCoerciveProjection.projectedOperator_inner {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (S : Submodule ℝ E) [CompleteSpace ↥S] (G : E →L[ℝ] E) (x y : ↥S) : inner ℝ ((projectedOperator S G) x) y = inner ℝ (G ↑x) ↑y

theorem EulerCoerciveProjection.projectedOperator_coercive {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (S : Submodule ℝ E) [CompleteSpace ↥S] (G : E →L[ℝ] E) (c : ℝ) (hG : ∀ (x : E), c * ‖x‖ ^ 2 ≤ inner ℝ (G x) x) (x : ↥S) : c * ‖x‖ ^ 2 ≤ inner ℝ ((projectedOperator S G) x) x

noncomputable def EulerCoerciveProjection.projectedInverse {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (S : Submodule ℝ E) [CompleteSpace ↥S] (G : E →L[ℝ] E) (c : ℝ) (hc : 0 < c) (hG : ∀ (x : E), c * ‖x‖ ^ 2 ≤ inner ℝ (G x) x) : ↥S →L[ℝ] ↥S

The projected-pressure inverse, constructed by applying Lax--Milgram on S.

Equations

• EulerCoerciveProjection.projectedInverse S G c hc hG = EulerCoerciveProjection.coerciveInverse (EulerCoerciveProjection.projectedOperator S G) c hc ⋯

@[simp]

theorem EulerCoerciveProjection.projectedOperator_inverse_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (S : Submodule ℝ E) [CompleteSpace ↥S] (G : E →L[ℝ] E) (c : ℝ) (hc : 0 < c) (hG : ∀ (x : E), c * ‖x‖ ^ 2 ≤ inner ℝ (G x) x) (f : ↥S) : (projectedOperator S G) ((projectedInverse S G c hc hG) f) = f

theorem EulerCoerciveProjection.projectedInverse_norm_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (S : Submodule ℝ E) [CompleteSpace ↥S] (G : E →L[ℝ] E) (c : ℝ) (hc : 0 < c) (hG : ∀ (x : E), c * ‖x‖ ^ 2 ≤ inner ℝ (G x) x) : ‖projectedInverse S G c hc hG‖ ≤ c⁻¹

@[simp]

theorem EulerCoerciveProjection.projectedOperator_sub {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (S : Submodule ℝ E) [CompleteSpace ↥S] (G H : E →L[ℝ] E) : projectedOperator S (G - H) = projectedOperator S G - projectedOperator S H

theorem EulerCoerciveProjection.projectedOperator_norm_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (S : Submodule ℝ E) [CompleteSpace ↥S] (G : E →L[ℝ] E) : ‖projectedOperator S G‖ ≤ ‖G‖

theorem EulerCoerciveProjection.projectedInverse_norm_sub_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (S : Submodule ℝ E) [CompleteSpace ↥S] (G H : E →L[ℝ] E) (c d : ℝ) (hc : 0 < c) (hd : 0 < d) (hG : ∀ (x : E), c * ‖x‖ ^ 2 ≤ inner ℝ (G x) x) (hH : ∀ (x : E), d * ‖x‖ ^ 2 ≤ inner ℝ (H x) x) : ‖projectedInverse S G c hc hG - projectedInverse S H d hd hH‖ ≤ c⁻¹ * d⁻¹ * ‖H - G‖

noncomputable def EulerCoerciveProjection.pressureSolver {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (S : Submodule ℝ E) [CompleteSpace ↥S] (G : E →L[ℝ] E) (c : ℝ) (hc : 0 < c) (hG : ∀ (x : E), c * ‖x‖ ^ 2 ≤ inner ℝ (G x) x) : E →L[ℝ] ↥S

Solves the projected equation with an ambient forcing vector.

Equations

• EulerCoerciveProjection.pressureSolver S G c hc hG = EulerCoerciveProjection.projectedInverse S G c hc hG ∘SL S.orthogonalProjectionOnto

theorem EulerCoerciveProjection.pressureSolver_equation {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (S : Submodule ℝ E) [CompleteSpace ↥S] (G : E →L[ℝ] E) (c : ℝ) (hc : 0 < c) (hG : ∀ (x : E), c * ‖x‖ ^ 2 ≤ inner ℝ (G x) x) (f : E) : S.orthogonalProjectionOnto (G ↑((pressureSolver S G c hc hG) f)) = S.orthogonalProjectionOnto f

theorem EulerCoerciveProjection.pressureSolver_apply_norm_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (S : Submodule ℝ E) [CompleteSpace ↥S] (G : E →L[ℝ] E) (c : ℝ) (hc : 0 < c) (hG : ∀ (x : E), c * ‖x‖ ^ 2 ≤ inner ℝ (G x) x) (f : E) : ‖(pressureSolver S G c hc hG) f‖ ≤ c⁻¹ * ‖f‖

theorem EulerCoerciveProjection.existsUnique_projected_solution {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (S : Submodule ℝ E) [CompleteSpace ↥S] (G : E →L[ℝ] E) (c : ℝ) (hc : 0 < c) (hG : ∀ (x : E), c * ‖x‖ ^ 2 ≤ inner ℝ (G x) x) (f : E) : ∃! p : ↥S, S.orthogonalProjectionOnto (G ↑p) = S.orthogonalProjectionOnto f

Existence and uniqueness of the pressure variable in the closed subspace.

theorem EulerCoerciveProjection.closed_subspace_inverse {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (S : Submodule ℝ E) (hS : IsClosed ↑S) (G : E →L[ℝ] E) (c : ℝ) (hc : 0 < c) (hG : ∀ (x : E), c * ‖x‖ ^ 2 ≤ inner ℝ (G x) x) : ∃ (I : ↥S →L[ℝ] ↥S), (∀ (f y : ↥S), inner ℝ (G ↑(I f)) ↑y = inner ℝ ↑f ↑y) ∧ ‖I‖ ≤ c⁻¹

Closedness supplies completeness; no inverse or existence hypothesis is assumed.