The joined pressure is the actual global normal-residual primitive #
The two local coercivity constants may differ. Both normal functionals are nevertheless the literal quotient by the same squared normal, so the joined pressure equals one global bounded cylinder operator applied to the actual forcing and velocity. This gives its estimates without any further solve.
theorem
EulerTransversePacketJoin.pressurePath_eq_source
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
{raw : EulerPacketProfileRecursion.VectorField}
(G : EulerTransversePacketProvider.Forcing P D raw)
:
pressurePath τ hτ hτT B G = EulerSourceNormalResidualBounds.sourcePressure P D.M D.normal D.normalLower ⋯ ⋯
(EulerTransversePacketProvider.HistoryData.forcingPath G) (velocityPath τ hτ hτT B G)
Actual equality of the whole pressure path, including the junction.
theorem
EulerTransversePacketJoin.pressurePath_normalized_eq_source
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
{raw : EulerPacketProfileRecursion.VectorField}
(G : EulerTransversePacketProvider.Forcing P D raw)
(g : C(↑(Set.Icc 0 D.T), ℝ))
(hg : ∀ (t : ↑(Set.Icc 0 D.T)), 0 < g t)
:
(EulerContinuousTimeWeight.normalize g hg) (pressurePath τ hτ hτT B G) = EulerSourceNormalResidualBounds.sourcePressure P D.M D.normal D.normalLower ⋯ ⋯
((EulerContinuousTimeWeight.normalize g hg) (EulerTransversePacketProvider.HistoryData.forcingPath G))
((EulerContinuousTimeWeight.normalize g hg) (velocityPath τ hτ hτT B G))
theorem
EulerTransversePacketJoin.source_pressure_bound
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
{raw : EulerPacketProfileRecursion.VectorField}
(G : EulerTransversePacketProvider.Forcing P D raw)
(g : C(↑(Set.Icc 0 D.T), ℝ))
(hg : ∀ (t : ↑(Set.Icc 0 D.T)), 0 < g t)
{ι : Type u_2}
[Fintype ι]
(directions : ι → EulerLiftedGradientSpace.LiftTangent)
(hdir : ∀ (i : ι), ‖directions i‖ ≤ 1)
(q : ℕ)
(Rc Cm CM Ri R Af Av : ℝ)
(hRc : 0 ≤ Rc)
(hCm : 0 ≤ Cm)
(hCM : 0 ≤ CM)
(hAf : 0 ≤ Af)
(hAv : 0 ≤ Av)
(hRi : 2 * EulerTimeLpGramGevrey.gramCost D.normalLower Cm 1 * (Rc + 1) ≤ Ri)
(hR : EulerParameterWordGevrey.sobolevCoefficientRadius ι (4 * Ri) ≤ R)
(hm :
∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space),
‖iteratedFDeriv ℝ n (⇑(D.normal.field t)) x‖ ≤ Cm * EulerGevrey.majorant Rc 0 n)
(hM :
∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space),
‖iteratedFDeriv ℝ n (⇑(D.M.field t)) x‖ ≤ CM * EulerGevrey.majorant Rc 0 n)
(d : ℕ)
(hf :
∀ (n : ℕ),
EulerParameterWordGevrey.block directions q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a)
((EulerContinuousTimeWeight.normalize g hg) (EulerTransversePacketProvider.HistoryData.forcingPath G)))
n 0 ≤ Af * EulerGevrey.majorant R d n)
(hv :
∀ (n : ℕ),
EulerParameterWordGevrey.block directions q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a)
((EulerContinuousTimeWeight.normalize g hg) (velocityPath τ hτ hτT B G)))
n 0 ≤ Av * EulerGevrey.majorant R d n)
(n : ℕ)
:
EulerParameterWordGevrey.block directions q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a)
((EulerContinuousTimeWeight.normalize g hg) (pressurePath τ hτ hτT B G)))
n 0 ≤ P * EulerSourceNormalResidualBounds.pressureCost ι q Ri Cm CM Af Av * EulerGevrey.majorant R d n
Literal pressure bound from the actual normalized forcing and velocity.
theorem
EulerTransversePacketJoin.scalarGradientField_normalized_bound
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
{raw : EulerPacketProfileRecursion.VectorField}
(G : EulerTransversePacketProvider.Forcing P D raw)
(g : C(↑(Set.Icc 0 D.T), ℝ))
(hg : ∀ (t : ↑(Set.Icc 0 D.T)), 0 < g t)
(q : ℕ)
(R A : ℝ)
(d : ℕ)
(hb :
∀ (n : ℕ),
EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a)
((EulerContinuousTimeWeight.normalize g hg) (pressurePath τ hτ hτT B G)))
n 0 ≤ A * EulerGevrey.majorant R d n)
(n : ℕ)
:
EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a)
((EulerContinuousTimeWeight.normalize g hg) (scalarGradientField τ hτ hτT B G).path))
n 0 ≤ 3 * A * EulerGevrey.majorant R (d + 1) n