Pointwise bounded coefficient fields act on genuine L² functions. Their pointwise positive quadratic bound supplies the Hilbert-space coercivity used by the lifted pressure solver. No multiplication operator is assumed.
theorem
EulerLiftedPressure.coefficientApply_memLp
{α : Type u_1}
{V : Type u_2}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
(A : α → V →L[ℝ] V)
(hA : MeasureTheory.AEStronglyMeasurable A μ)
(C : NNReal)
(hbound : ∀ (x : α), ‖A x‖ ≤ ↑C)
(f : ↥(MeasureTheory.Lp V 2 μ))
:
MeasureTheory.MemLp (fun (x : α) => (A x) (↑↑f x)) 2 μ
noncomputable def
EulerLiftedPressure.coefficientApply
{α : Type u_1}
{V : Type u_2}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
(A : α → V →L[ℝ] V)
(hA : MeasureTheory.AEStronglyMeasurable A μ)
(C : NNReal)
(hbound : ∀ (x : α), ‖A x‖ ≤ ↑C)
(f : ↥(MeasureTheory.Lp V 2 μ))
:
↥(MeasureTheory.Lp V 2 μ)
Pointwise bounded coefficient application represented as an L² element.
Equations
- EulerLiftedPressure.coefficientApply A hA C hbound f = MeasureTheory.MemLp.toLp (fun (x : α) => (A x) (↑↑f x)) ⋯
Instances For
theorem
EulerLiftedPressure.coefficientApply_ae
{α : Type u_1}
{V : Type u_2}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
(A : α → V →L[ℝ] V)
(hA : MeasureTheory.AEStronglyMeasurable A μ)
(C : NNReal)
(hbound : ∀ (x : α), ‖A x‖ ≤ ↑C)
(f : ↥(MeasureTheory.Lp V 2 μ))
:
↑↑(coefficientApply A hA C hbound f) =ᵐ[μ] fun (x : α) => (A x) (↑↑f x)
noncomputable def
EulerLiftedPressure.coefficientLinearMap
{α : Type u_1}
{V : Type u_2}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
(A : α → V →L[ℝ] V)
(hA : MeasureTheory.AEStronglyMeasurable A μ)
(C : NNReal)
(hbound : ∀ (x : α), ‖A x‖ ≤ ↑C)
:
The linear map induced by pointwise coefficient multiplication.
Equations
- EulerLiftedPressure.coefficientLinearMap A hA C hbound = { toFun := EulerLiftedPressure.coefficientApply A hA C hbound, map_add' := ⋯, map_smul' := ⋯ }
Instances For
theorem
EulerLiftedPressure.coefficientApply_norm_le
{α : Type u_1}
{V : Type u_2}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
(A : α → V →L[ℝ] V)
(hA : MeasureTheory.AEStronglyMeasurable A μ)
(C : NNReal)
(hbound : ∀ (x : α), ‖A x‖ ≤ ↑C)
(f : ↥(MeasureTheory.Lp V 2 μ))
:
noncomputable def
EulerLiftedPressure.coefficientOperator
{α : Type u_1}
{V : Type u_2}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
(A : α → V →L[ℝ] V)
(hA : MeasureTheory.AEStronglyMeasurable A μ)
(C : NNReal)
(hbound : ∀ (x : α), ‖A x‖ ≤ ↑C)
:
The bounded operator induced by the actual coefficient field.
Equations
- EulerLiftedPressure.coefficientOperator A hA C hbound = (EulerLiftedPressure.coefficientLinearMap A hA C hbound).mkContinuous ↑C ⋯
Instances For
theorem
EulerLiftedPressure.coefficientOperator_ae
{α : Type u_1}
{V : Type u_2}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
(A : α → V →L[ℝ] V)
(hA : MeasureTheory.AEStronglyMeasurable A μ)
(C : NNReal)
(hbound : ∀ (x : α), ‖A x‖ ≤ ↑C)
(f : ↥(MeasureTheory.Lp V 2 μ))
:
↑↑((coefficientOperator A hA C hbound) f) =ᵐ[μ] fun (x : α) => (A x) (↑↑f x)
theorem
EulerLiftedPressure.coefficientOperator_norm_le
{α : Type u_1}
{V : Type u_2}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
(A : α → V →L[ℝ] V)
(hA : MeasureTheory.AEStronglyMeasurable A μ)
(C : NNReal)
(hbound : ∀ (x : α), ‖A x‖ ≤ ↑C)
:
theorem
EulerLiftedPressure.coefficientOperator_coercive
{α : Type u_1}
{V : Type u_2}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
(A : α → V →L[ℝ] V)
(hA : MeasureTheory.AEStronglyMeasurable A μ)
(C : NNReal)
(hbound : ∀ (x : α), ‖A x‖ ≤ ↑C)
(c : ℝ)
(hpositive : ∀ (x : α) (v : V), c * ‖v‖ ^ 2 ≤ inner ℝ ((A x) v) v)
(f : ↥(MeasureTheory.Lp V 2 μ))
:
Pointwise coercivity yields the actual integral L² coercivity.
theorem
EulerLiftedPressure.coefficientOperator_comp_apply
{α : Type u_1}
{V : Type u_2}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
(A B : α → V →L[ℝ] V)
(hA : MeasureTheory.AEStronglyMeasurable A μ)
(hB : MeasureTheory.AEStronglyMeasurable B μ)
(C D : NNReal)
(hA_bound : ∀ (x : α), ‖A x‖ ≤ ↑C)
(hB_bound : ∀ (x : α), ‖B x‖ ≤ ↑D)
(hAB : ∀ (x : α) (v : V), (A x) ((B x) v) = v)
(f : ↥(MeasureTheory.Lp V 2 μ))
:
theorem
EulerLiftedPressure.coefficientOperator_inner_swap
{α : Type u_1}
{V : Type u_2}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
(A : α → V →L[ℝ] V)
(hA : MeasureTheory.AEStronglyMeasurable A μ)
(C : NNReal)
(hbound : ∀ (x : α), ‖A x‖ ≤ ↑C)
(hsym : ∀ (x : α) (v w : V), inner ℝ ((A x) v) w = inner ℝ v ((A x) w))
(f g : ↥(MeasureTheory.Lp V 2 μ))
:
inner ℝ ((coefficientOperator A hA C hbound) f) g = inner ℝ f ((coefficientOperator A hA C hbound) g)
Pointwise symmetry gives symmetry of the actual L² multiplication operator.
theorem
EulerLiftedPressure.existsUnique_lifted_pressure
(period : ℝ)
[Fact (0 < period)]
(κ : ℝ)
(m : EulerLiftedGradientSpace.Vector3)
(A :
EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerLiftedGradientSpace.Vector3)
(hA : MeasureTheory.AEStronglyMeasurable A (EulerLiftedGradientSpace.liftMeasure period))
(C : NNReal)
(hbound : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ‖A x‖ ≤ ↑C)
(c : ℝ)
(hc : 0 < c)
(hpositive :
∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3),
c * ‖v‖ ^ 2 ≤ inner ℝ ((A x) v) v)
(f : ↥(EulerLiftedGradientSpace.LiftL2 period))
:
∃! p : ↥(EulerLiftedGradientSpace.gradientSpace period κ m), (EulerLiftedGradientSpace.gradientSpace period κ m).orthogonalProjectionOnto
((coefficientOperator A hA C hbound) ↑p) = (EulerLiftedGradientSpace.gradientSpace period κ m).orthogonalProjectionOnto f
theorem
EulerLiftedPressure.exists_lifted_pressure_with_bound
(period : ℝ)
[Fact (0 < period)]
(κ : ℝ)
(m : EulerLiftedGradientSpace.Vector3)
(A :
EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerLiftedGradientSpace.Vector3)
(hA : MeasureTheory.AEStronglyMeasurable A (EulerLiftedGradientSpace.liftMeasure period))
(C : NNReal)
(hbound : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ‖A x‖ ≤ ↑C)
(c : ℝ)
(hc : 0 < c)
(hpositive :
∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3),
c * ‖v‖ ^ 2 ≤ inner ℝ ((A x) v) v)
(f : ↥(EulerLiftedGradientSpace.LiftL2 period))
:
∃ (p : ↥(EulerLiftedGradientSpace.gradientSpace period κ m)),
(EulerLiftedGradientSpace.gradientSpace period κ m).orthogonalProjectionOnto
((coefficientOperator A hA C hbound) ↑p) = (EulerLiftedGradientSpace.gradientSpace period κ m).orthogonalProjectionOnto f ∧ ‖p‖ ≤ c⁻¹ * ‖f‖
theorem
EulerLiftedPressure.metric_pressure_cancellation
(period : ℝ)
[Fact (0 < period)]
(κ : ℝ)
(m : EulerLiftedGradientSpace.Vector3)
(K G :
EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerLiftedGradientSpace.Vector3)
(hK : MeasureTheory.AEStronglyMeasurable K (EulerLiftedGradientSpace.liftMeasure period))
(hG : MeasureTheory.AEStronglyMeasurable G (EulerLiftedGradientSpace.liftMeasure period))
(C D : NNReal)
(hK_bound : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ‖K x‖ ≤ ↑C)
(hG_bound : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ‖G x‖ ≤ ↑D)
(hK_sym :
∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v w : EulerLiftedGradientSpace.Vector3),
inner ℝ ((K x) v) w = inner ℝ v ((K x) w))
(hKG : ∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3), (K x) ((G x) v) = v)
{e p : ↥(EulerLiftedGradientSpace.LiftL2 period)}
(he : e ∈ EulerLiftedGradientSpace.divergenceFreeSpace period κ m)
(hp : p ∈ EulerLiftedGradientSpace.gradientSpace period κ m)
:
Exact metric-pressure cancellation for pointwise inverse symmetric coefficient fields.