Related estimates used together by the same construction modules.
Retain the actual scalar angular pressure in the quantitative grade bounds. Its norm-one embedding supplies genuine vector-valued Sobolev evaluation, without changing the radius or the time profile.
theorem
EulerPacketCylinderField.scalarEmbeddingField_normalized_bound
{P T : ℝ}
[Fact (0 < P)]
(raw : EulerPacketProfileRecursion.ScalarField)
(p : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P ℝ)))
(hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p)
(he :
∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ),
raw (↑t, x, θ) = EulerCylinderScalarPrimitive.scalarPointField P p hp t (x, ↑θ))
(hT : 0 ≤ T)
(g : C(↑(Set.Icc 0 T), ℝ))
(hg : ∀ (t : ↑(Set.Icc 0 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) p))
n 0 ≤ A * EulerGevrey.majorant R d n)
:
((scalarEmbeddingField raw p hp he).normalized hT g hg).WordBound q R A d
theorem
EulerPacketCylinderField.angularGradientField_normalized_bound
{P T : ℝ}
[Fact (0 < P)]
(raw : EulerPacketProfileRecursion.ScalarField)
(p : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P ℝ)))
(hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p)
(he :
∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ),
raw (↑t, x, θ) = EulerCylinderScalarPrimitive.scalarPointField P p hp t (x, ↑θ))
(hT : 0 ≤ T)
(g : C(↑(Set.Icc 0 T), ℝ))
(hg : ∀ (t : ↑(Set.Icc 0 T)), 0 < g t)
(m : EulerSmoothLimit.Space)
(hm : ‖m‖ ≤ 1)
{q d : ℕ}
{R A : ℝ}
(hR : 0 ≤ R)
(hA : 0 ≤ A)
(hb : ((scalarEmbeddingField raw p hp he).normalized hT g hg).WordBound q R A d)
:
((EulerPacketPressure.angularGradientField P raw p hp he m).normalized hT g hg).WordBound q R A (d + 1)
noncomputable def
EulerTransversePacketJoin.scalarField
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
{raw : EulerPacketProfileRecursion.VectorField}
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(G : EulerTransversePacketProvider.Forcing P D raw)
:
EulerPacketCylinderField.Field P D.T fun (z : EulerPacketPointJets.Domain) =>
EulerCylinderScalarPrimitive.scalarEmbed (scalar τ hτ hτT B G z)
Scalar field, constructed using scalarEmbeddingField.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerTransversePacketJoin.Budget.scalar_grade_bound_pred
{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}
(L : Budget D τ hτ hτT B (Fin 4) 6)
(N : NormalBudget D 6 L.R)
(W : L.GradeGuards N)
(G : EulerTransversePacketProvider.Forcing P D raw)
(F : EulerPacketCylinderField.Field P D.T raw)
(c : ℝ)
(hc : 0 < c)
(p : ℕ)
(hp : 2 ≤ p)
(hforce : (F.normalized ⋯ (c • L.fullProfile) ⋯).WordBound 6 L.R 1 (EulerPacketShiftArithmetic.highForceShift p))
:
((scalarField τ hτ hτT B G).normalized ⋯ (c • L.fullProfile) ⋯).WordBound 6 L.R 1
(EulerPacketShiftArithmetic.highShift p - 1)
noncomputable def
EulerTransversePacketJoin.angularField
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
{raw : EulerPacketProfileRecursion.VectorField}
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(G : EulerTransversePacketProvider.Forcing P D raw)
:
EulerPacketCylinderField.Field P D.T fun (z : EulerPacketPointJets.Domain) =>
(EulerPacketPointJets.pressureJet (scalar τ hτ hτT B G) z).2 EulerPacketPointJets.angleDirection • D.m₀
Angular field, constructed using EulerPacketPressure.angularGradientField.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerTransversePacketJoin.Budget.angular_grade_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}
(L : Budget D τ hτ hτT B (Fin 4) 6)
(N : NormalBudget D 6 L.R)
(W : L.GradeGuards N)
(G : EulerTransversePacketProvider.Forcing P D raw)
(F : EulerPacketCylinderField.Field P D.T raw)
(c : ℝ)
(hc : 0 < c)
(p : ℕ)
(hp : 2 ≤ p)
(hforce : (F.normalized ⋯ (c • L.fullProfile) ⋯).WordBound 6 L.R 1 (EulerPacketShiftArithmetic.highForceShift p))
:
((angularField τ hτ hτT B G).normalized ⋯ (c • L.fullProfile) ⋯).WordBound 6 L.R 1
(EulerPacketShiftArithmetic.highShift p)
theorem
EulerTransversePacketJoin.Budget.scalar_grade_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}
(L : Budget D τ hτ hτT B (Fin 4) 6)
(N : NormalBudget D 6 L.R)
(W : L.GradeGuards N)
(G : EulerTransversePacketProvider.Forcing P D raw)
(F : EulerPacketCylinderField.Field P D.T raw)
(c : ℝ)
(hc : 0 < c)
(p : ℕ)
(hp : 2 ≤ p)
(hforce : (F.normalized ⋯ (c • L.fullProfile) ⋯).WordBound 6 L.R 1 (EulerPacketShiftArithmetic.highForceShift p))
:
((scalarField τ hτ hτT B G).normalized ⋯ (c • L.fullProfile) ⋯).WordBound 6 L.R 1
(EulerPacketShiftArithmetic.highShift p)
noncomputable def
EulerTransversePacketPrimary.scalarField
{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τ ⋯))
(Y : EulerTransversePacketProvider.InitialData P D)
:
EulerPacketCylinderField.Field P D.T fun (z : EulerPacketPointJets.Domain) =>
EulerCylinderScalarPrimitive.scalarEmbed (scalar τ hτ hτT B Y z)
Scalar field, constructed using scalarEmbeddingField.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerTransversePacketPrimary.Budget.scalar_grade_bound_pred
{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τ ⋯)}
{L : EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) 6}
(H : Budget L)
(N : EulerTransversePacketJoin.NormalBudget D 6 L.R)
(C : ℝ)
(W : H.GradeGuards N C)
(Y : EulerTransversePacketProvider.InitialData P D)
(α : ℝ)
(hα : 0 < α)
(hYb :
∀ (n : ℕ),
EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection 6
(fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) ↑Y.value) n 0 ≤ α * C * EulerGevrey.majorant L.R 0 n)
:
((scalarField τ hτ hτT B Y).normalized ⋯ (α • L.fullProfile) ⋯).WordBound 6 L.R 1
(EulerPacketShiftArithmetic.highShift 1 - 1)
noncomputable def
EulerTransversePacketPrimary.angularField
{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τ ⋯))
(Y : EulerTransversePacketProvider.InitialData P D)
:
EulerPacketCylinderField.Field P D.T fun (z : EulerPacketPointJets.Domain) =>
(EulerPacketPointJets.pressureJet (scalar τ hτ hτT B Y) z).2 EulerPacketPointJets.angleDirection • D.m₀
Angular field, constructed using EulerPacketPressure.angularGradientField.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerTransversePacketPrimary.Budget.angular_grade_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τ ⋯)}
{L : EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) 6}
(H : Budget L)
(N : EulerTransversePacketJoin.NormalBudget D 6 L.R)
(C : ℝ)
(W : H.GradeGuards N C)
(Y : EulerTransversePacketProvider.InitialData P D)
(α : ℝ)
(hα : 0 < α)
(hYb :
∀ (n : ℕ),
EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection 6
(fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) ↑Y.value) n 0 ≤ α * C * EulerGevrey.majorant L.R 0 n)
:
((angularField τ hτ hτT B Y).normalized ⋯ (α • L.fullProfile) ⋯).WordBound 6 L.R 1
(EulerPacketShiftArithmetic.highShift 1)
theorem
EulerTransversePacketPrimary.Budget.scalar_grade_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τ ⋯)}
{L : EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) 6}
(H : Budget L)
(N : EulerTransversePacketJoin.NormalBudget D 6 L.R)
(C : ℝ)
(W : H.GradeGuards N C)
(Y : EulerTransversePacketProvider.InitialData P D)
(α : ℝ)
(hα : 0 < α)
(hYb :
∀ (n : ℕ),
EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection 6
(fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) ↑Y.value) n 0 ≤ α * C * EulerGevrey.majorant L.R 0 n)
:
((scalarField τ hτ hτT B Y).normalized ⋯ (α • L.fullProfile) ⋯).WordBound 6 L.R 1
(EulerPacketShiftArithmetic.highShift 1)
The actual recursive mean pressure retains the same grade estimate as the mean velocity. This estimate was already proved by the source solver but is not a field of the velocity-oriented ProfileBudget.
theorem
EulerPacketCylinderField.ProfileBudget.meanPressure_step_exists
{P : ℝ}
[Fact (0 < P)]
(M : EulerMeanPacketProvider.Data)
{R : ℝ}
(LM : EulerMeanPacketProvider.Budget M 6 R)
(WM : LM.GradeGuards)
{O : EulerPacketProfileRecursion.Operators}
(C : CoefficientData P M.T O)
(BC : CoefficientBudget C)
(hmean : O.meanSolve = EulerMeanPacketProvider.meanSolve M)
(hRc : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) BC.Rc ≤ R)
(hcost : BC.termCost ≤ R)
(S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 M.T))
{support : Set EulerSmoothLimit.Space}
{p : ℕ}
{a : ℕ → EulerPacketProfileRecursion.Profile}
(hp : 2 ≤ p)
(G : (i : ℕ) → i < p → ProfileRegularity P M.T ⋯ support (a i))
(hG : ∀ (i : ℕ) (hi : i < p), 1 ≤ i → ProfileBudget (G i hi) S R i)
(hc₀ : (a 0).corrector = 0)
(hB₁ : (a 1).mean = 0)
(hA :
∀ i < p,
∀ (t : ↑(Set.Icc 0 M.T)) (x : EulerSmoothLimit.Space) (θ : ℝ),
inner ℝ (O.normal (↑t, x, θ)) ((a i).high (↑t, x, θ)) = 0)
:
∃ (Q : Field P M.T (pressureGradient (EulerPacketProfileRecursion.step O p a).meanPressure)),
(Q.normalized ⋯ (S.mean p) ⋯).WordBound 6 R 1 (EulerPacketShiftArithmetic.meanShift p)
theorem
EulerPacketCylinderField.ProfileBudget.meanPressure_step_bound
{P : ℝ}
[Fact (0 < P)]
(M : EulerMeanPacketProvider.Data)
{R : ℝ}
(LM : EulerMeanPacketProvider.Budget M 6 R)
(WM : LM.GradeGuards)
{O : EulerPacketProfileRecursion.Operators}
(C : CoefficientData P M.T O)
(BC : CoefficientBudget C)
(hmean : O.meanSolve = EulerMeanPacketProvider.meanSolve M)
(hRc : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) BC.Rc ≤ R)
(hcost : BC.termCost ≤ R)
(S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 M.T))
{support : Set EulerSmoothLimit.Space}
{p : ℕ}
{a : ℕ → EulerPacketProfileRecursion.Profile}
(hp : 2 ≤ p)
(G : (i : ℕ) → i < p → ProfileRegularity P M.T ⋯ support (a i))
(hG : ∀ (i : ℕ) (hi : i < p), 1 ≤ i → ProfileBudget (G i hi) S R i)
(hc₀ : (a 0).corrector = 0)
(hB₁ : (a 1).mean = 0)
(hA :
∀ i < p,
∀ (t : ↑(Set.Icc 0 M.T)) (x : EulerSmoothLimit.Space) (θ : ℝ),
inner ℝ (O.normal (↑t, x, θ)) ((a i).high (↑t, x, θ)) = 0)
(Q : Field P M.T (pressureGradient (EulerPacketProfileRecursion.step O p a).meanPressure))
:
(Q.normalized ⋯ (S.mean p) ⋯).WordBound 6 R 1 (EulerPacketShiftArithmetic.meanShift p)