The actual finite pressure Hessian is its primary normal tensor plus a uniform inverse-frequency error. No derivative or remainder estimate is assumed for a solved field.
Scalar pressure and angular pressure-gradient grade bounds for the actual zero-history solve. Forced grades have zero initial data; the primary keeps the literal compact initial-data amplitude. All bounds retain the same radius.
noncomputable def
EulerTransversePacketForward.scalarField
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
{raw : EulerPacketProfileRecursion.VectorField}
(G : EulerTransversePacketProvider.Forcing P D raw)
(I : EulerTransversePacketProvider.InitialData P D)
:
EulerPacketCylinderField.Field P D.T fun (z : EulerPacketPointJets.Domain) =>
EulerCylinderScalarPrimitive.scalarEmbed (G.scalar I z)
Scalar field, given by scalarEmbeddingField (G.scalar I) (G.pressurePath I) (G.pressurePath_orbit I) (G.scalar_eq_pointField I).
Equations
Instances For
noncomputable def
EulerTransversePacketForward.angularField
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
{raw : EulerPacketProfileRecursion.VectorField}
(G : EulerTransversePacketProvider.Forcing P D raw)
(I : EulerTransversePacketProvider.InitialData P D)
:
EulerPacketCylinderField.Field P D.T fun (z : EulerPacketPointJets.Domain) =>
(EulerPacketPointJets.pressureJet (G.scalar I) z).2 EulerPacketPointJets.angleDirection • D.m₀
Angular field, constructed using EulerPacketPressure.angularGradientField.
Equations
- EulerTransversePacketForward.angularField G I = EulerPacketPressure.angularGradientField P (G.scalar I) (G.pressurePath I) ⋯ ⋯ D.m₀
Instances For
theorem
EulerTransversePacketForward.Budget.scalar_grade_bound_pred
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
{raw : EulerPacketProfileRecursion.VectorField}
(L : Budget D (Fin 4) 6)
(N : EulerTransversePacketJoin.NormalBudget D 6 L.R)
(C : ℝ)
(W : L.GradeGuards N C)
(G : EulerTransversePacketProvider.Forcing P D raw)
(I : EulerTransversePacketProvider.InitialData P D)
(c : ℝ)
(hc : 0 < c)
(d e : ℕ)
(hroom : d + 3 ≤ e)
(hforce :
∀ (n : ℕ),
EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection 6
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a)
((EulerContinuousTimeWeight.normalize L.g ⋯) (EulerTransversePacketProvider.HistoryData.forcingPath G)))
n 0 ≤ c * C * EulerGevrey.majorant L.R d n)
(hinitial :
∀ (n : ℕ),
EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection 6
(fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) ↑I.value) n 0 ≤ c * C * EulerGevrey.majorant L.R d n)
:
((scalarField G I).normalized ⋯ (c • L.g) ⋯).WordBound 6 L.R 1 (e - 1)
theorem
EulerTransversePacketForward.Budget.angular_grade_bound
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
{raw : EulerPacketProfileRecursion.VectorField}
(L : Budget D (Fin 4) 6)
(N : EulerTransversePacketJoin.NormalBudget D 6 L.R)
(C : ℝ)
(W : L.GradeGuards N C)
(G : EulerTransversePacketProvider.Forcing P D raw)
(I : EulerTransversePacketProvider.InitialData P D)
(c : ℝ)
(hc : 0 < c)
(d e : ℕ)
(hroom : d + 3 ≤ e)
(hforce :
∀ (n : ℕ),
EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection 6
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a)
((EulerContinuousTimeWeight.normalize L.g ⋯) (EulerTransversePacketProvider.HistoryData.forcingPath G)))
n 0 ≤ c * C * EulerGevrey.majorant L.R d n)
(hinitial :
∀ (n : ℕ),
EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection 6
(fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) ↑I.value) n 0 ≤ c * C * EulerGevrey.majorant L.R d n)
:
((angularField G I).normalized ⋯ (c • L.g) ⋯).WordBound 6 L.R 1 e
theorem
EulerTransversePacketForward.Budget.scalar_grade_bound
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
{raw : EulerPacketProfileRecursion.VectorField}
(L : Budget D (Fin 4) 6)
(N : EulerTransversePacketJoin.NormalBudget D 6 L.R)
(C : ℝ)
(W : L.GradeGuards N C)
(G : EulerTransversePacketProvider.Forcing P D raw)
(I : EulerTransversePacketProvider.InitialData P D)
(c : ℝ)
(hc : 0 < c)
(d e : ℕ)
(hroom : d + 3 ≤ e)
(hforce :
∀ (n : ℕ),
EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection 6
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a)
((EulerContinuousTimeWeight.normalize L.g ⋯) (EulerTransversePacketProvider.HistoryData.forcingPath G)))
n 0 ≤ c * C * EulerGevrey.majorant L.R d n)
(hinitial :
∀ (n : ℕ),
EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection 6
(fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) ↑I.value) n 0 ≤ c * C * EulerGevrey.majorant L.R d n)
:
((scalarField G I).normalized ⋯ (c • L.g) ⋯).WordBound 6 L.R 1 e
theorem
EulerTransversePacketForward.Budget.forced_scalar_and_angular_grade_bound
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
{raw : EulerPacketProfileRecursion.VectorField}
(L : Budget D (Fin 4) 6)
(N : EulerTransversePacketJoin.NormalBudget D 6 L.R)
(W : L.GradeGuards N 1)
(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.g) ⋯).WordBound 6 L.R 1 (EulerPacketShiftArithmetic.highForceShift p))
:
((scalarField G (EulerTransversePacketProvider.InitialData.zero P D)).normalized ⋯ (c • L.g) ⋯).WordBound 6 L.R 1
(EulerPacketShiftArithmetic.highShift p) ∧ ((angularField G (EulerTransversePacketProvider.InitialData.zero P D)).normalized ⋯ (c • L.g) ⋯).WordBound 6 L.R 1
(EulerPacketShiftArithmetic.highShift p)
theorem
EulerTransversePacketForward.Budget.primary_scalar_and_angular_grade_bound
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
(L : Budget D (Fin 4) 6)
(N : EulerTransversePacketJoin.NormalBudget D 6 L.R)
(C : ℝ)
(W : L.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 (EulerPacketForwardPrimary.forcing D) Y).normalized ⋯ (α • L.g) ⋯).WordBound 6 L.R 1
(EulerPacketShiftArithmetic.highShift 1) ∧ ((angularField (EulerPacketForwardPrimary.forcing D) Y).normalized ⋯ (α • L.g) ⋯).WordBound 6 L.R 1
(EulerPacketShiftArithmetic.highShift 1)
The angular derivative of the actual recursive high pressure retains the unit grade budget. This is derived from the same source solve used by the velocity recursion.
theorem
EulerPacketCylinderField.ProfileBudget.forwardAngularPressure_step_exists
{P : ℝ}
[Fact (0 < P)]
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hTime : M.T = D.T)
(L : EulerTransversePacketForward.Budget D (Fin 4) 6)
(N : EulerTransversePacketJoin.NormalBudget D 6 L.R)
(W : L.GradeGuards N 1)
(LM : EulerMeanPacketProvider.Budget M 6 L.R)
(WM : LM.GradeGuards)
{O : EulerPacketProfileRecursion.Operators}
(C : CoefficientData P M.T O)
(BC : CoefficientBudget C)
(hmean : O.meanSolve = EulerMeanPacketProvider.meanSolve M)
(hhigh : O.highSolve = EulerTransversePacketProvider.highSolve P D (EulerTransversePacketProvider.InitialData.zero P D))
(hRc : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) BC.Rc ≤ L.R)
(hcost : BC.termCost ≤ L.R)
(S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 M.T))
{p : ℕ}
{a : ℕ → EulerPacketProfileRecursion.Profile}
(hp : 2 ≤ p)
(G : (i : ℕ) → i < p → ProfileRegularity P M.T ⋯ D.support (a i))
(hG : ∀ (i : ℕ) (hi : i < p), 1 ≤ i → ProfileBudget (G i hi) S L.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)
(c : ℝ)
(hc : 0 < c)
(hprofile : timeProfileChange (S.high p) hTime = c • L.g)
:
∃ (Q :
Field P M.T fun (z : EulerPacketPointJets.Domain) =>
(EulerPacketPointJets.pressureJet (EulerPacketProfileRecursion.step O p a).highPressure z).2
EulerPacketPointJets.angleDirection • D.m₀),
(Q.normalized ⋯ (S.high p) ⋯).WordBound 6 L.R 1 (EulerPacketShiftArithmetic.highShift p)
theorem
EulerPacketTerminalDatum.forwardInitializedPressureBudget_exists
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hTime : M.T = D.T)
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(α : ℝ)
(L : EulerTransversePacketForward.Budget D (Fin 4) 6)
(NB : EulerTransversePacketJoin.NormalBudget D 6 L.R)
(W : L.GradeGuards NB 1)
(LM : EulerMeanPacketProvider.Budget M 6 L.R)
(WM : LM.GradeGuards)
(BC :
EulerPacketCylinderField.CoefficientBudget
(EulerPacketCylinderField.sourceCoefficientData period M D (EulerTransversePacketProvider.InitialData.zero period D)
hTime))
(hRc : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) BC.Rc ≤ L.R)
(hcost : BC.termCost ≤ L.R)
(hδ1 : δ ≤ 1)
(hα : 0 < α)
(hR : wordRadius (Fin 4) δ ≤ L.R)
(WP : L.GradeGuards NB (wordCost (Fin 4) 6 δ * ‖ξ‖))
(S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 M.T))
(hgrowth : EulerPacketCylinderField.timeProfileChange S.growth hTime = α • L.g)
(p : ℕ)
:
Nonempty
(EulerPacketCylinderField.PressureBudget period M.T ⋯ D.m₀ (forwardInitializedProfiles M D δ hδ ξ hs α p) S L.R p)
The actual forward finite pressure has its actual leading angular force and a uniformly small covector remainder.
theorem
EulerPacketTerminalDatum.forwardInitializedProfiles_one_highPressure
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(α : ℝ)
:
(forwardInitializedProfiles M D δ hδ ξ hs α 1).highPressure = EulerPacketForwardPrimary.scalar D (initialData D δ hδ (α • ξ) hs)
theorem
EulerPacketTerminalDatum.forwardInitializedProfiles_one_meanPressure
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(α : ℝ)
:
noncomputable def
EulerPacketTerminalDatum.forwardInitializedAngularPressure
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(α : ℝ)
:
Forward initialized angular pressure, defined pointwise by (pressureJet (scalar D (initialData D δ hδ (α • ξ) hs)) z).2 angleDirection.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
EulerPacketTerminalDatum.forwardInitializedCovectorRemainder
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(α : ℝ)
(N : ℕ)
(κ : ℝ)
:
Forward initialized covector remainder, given by covectorRemainder (N := N) (a := forwardInitializedProfiles M D δ hδ ξ hs α) D.m₀ κ.
Equations
- EulerPacketTerminalDatum.forwardInitializedCovectorRemainder M D δ hδ ξ hs α N κ = EulerPacketPressure.covectorRemainder D.m₀ κ
Instances For
theorem
EulerPacketTerminalDatum.forwardInitializedPressure_gradient_decomposition
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hTime : M.T = D.T)
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(α : ℝ)
(N : ℕ)
(k : ℝ)
(hk : k ≠ 0)
(t : ↑(Set.Icc 0 D.T))
(Y : EulerSmoothLimit.Space → EulerSmoothLimit.Space)
(x : EulerSmoothLimit.Space)
(hY : HasFDerivAt Y ((D.FInv.field t) (Y x)) x)
:
gradient
(fun (y : EulerSmoothLimit.Space) =>
forwardInitializedPressure M D δ hδ ξ hs α N k⁻¹ (↑t, Y y, k * inner ℝ D.m₀ (Y y)))
x = EulerPacketGraphHessian.fastForce
(fun (z : EulerLiftedGradientSpace.LiftTangent) => forwardInitializedAngularPressure D δ hδ ξ hs α (↑t, z)) k D.m₀
Y (fun (y : EulerSmoothLimit.Space) => (D.FInv.field t) (Y y)) x + (ContinuousLinearMap.adjoint ((D.FInv.field t) (Y x)))
(forwardInitializedCovectorRemainder M D δ hδ ξ hs α N k⁻¹ (↑t, Y x, k * inner ℝ D.m₀ (Y x)))
noncomputable def
EulerPacketTerminalDatum.forwardInitializedPressureBudget
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hTime : M.T = D.T)
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(α : ℝ)
(L : EulerTransversePacketForward.Budget D (Fin 4) 6)
(NB : EulerTransversePacketJoin.NormalBudget D 6 L.R)
(W : L.GradeGuards NB 1)
(LM : EulerMeanPacketProvider.Budget M 6 L.R)
(WM : LM.GradeGuards)
(BC :
EulerPacketCylinderField.CoefficientBudget
(EulerPacketCylinderField.sourceCoefficientData period M D (EulerTransversePacketProvider.InitialData.zero period D)
hTime))
(hRc : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) BC.Rc ≤ L.R)
(hcost : BC.termCost ≤ L.R)
(hδ1 : δ ≤ 1)
(hα : 0 < α)
(hR : wordRadius (Fin 4) δ ≤ L.R)
(WP : L.GradeGuards NB (wordCost (Fin 4) 6 δ * ‖ξ‖))
(S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 M.T))
(hgrowth : EulerPacketCylinderField.timeProfileChange S.growth hTime = α • L.g)
(p : ℕ)
:
EulerPacketCylinderField.PressureBudget period M.T ⋯ D.m₀ (forwardInitializedProfiles M D δ hδ ξ hs α p) S L.R p
Forward initialized pressure budget, constructed using Classical.choice.
Equations
- EulerPacketTerminalDatum.forwardInitializedPressureBudget M D hTime δ hδ ξ hs α L NB W LM WM BC hRc hcost hδ1 hα hR WP S hgrowth p = Classical.choice ⋯
Instances For
noncomputable def
EulerPacketTerminalDatum.forwardInitializedAngularPressureField
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hTime : M.T = D.T)
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(α : ℝ)
(L : EulerTransversePacketForward.Budget D (Fin 4) 6)
(NB : EulerTransversePacketJoin.NormalBudget D 6 L.R)
(W : L.GradeGuards NB 1)
(LM : EulerMeanPacketProvider.Budget M 6 L.R)
(WM : LM.GradeGuards)
(BC :
EulerPacketCylinderField.CoefficientBudget
(EulerPacketCylinderField.sourceCoefficientData period M D (EulerTransversePacketProvider.InitialData.zero period D)
hTime))
(hRc : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) BC.Rc ≤ L.R)
(hcost : BC.termCost ≤ L.R)
(hδ1 : δ ≤ 1)
(hα : 0 < α)
(hR : wordRadius (Fin 4) δ ≤ L.R)
(WP : L.GradeGuards NB (wordCost (Fin 4) 6 δ * ‖ξ‖))
(S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 M.T))
(hgrowth : EulerPacketCylinderField.timeProfileChange S.growth hTime = α • L.g)
:
EulerPacketCylinderField.Field period D.T fun (z : EulerPacketPointJets.Domain) =>
forwardInitializedAngularPressure D δ hδ ξ hs α z • D.m₀
Forward initialized angular pressure field as an element of Field period D.T (fun z => forwardInitializedAngularPressure D δ hδ ξ hs α z • D.m₀).
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerPacketTerminalDatum.forwardInitializedAngularPressure_bound
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hTime : M.T = D.T)
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(α : ℝ)
(L : EulerTransversePacketForward.Budget D (Fin 4) 6)
(NB : EulerTransversePacketJoin.NormalBudget D 6 L.R)
(W : L.GradeGuards NB 1)
(LM : EulerMeanPacketProvider.Budget M 6 L.R)
(WM : LM.GradeGuards)
(BC :
EulerPacketCylinderField.CoefficientBudget
(EulerPacketCylinderField.sourceCoefficientData period M D (EulerTransversePacketProvider.InitialData.zero period D)
hTime))
(hRc : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) BC.Rc ≤ L.R)
(hcost : BC.termCost ≤ L.R)
(hδ1 : δ ≤ 1)
(hα : 0 < α)
(hR : wordRadius (Fin 4) δ ≤ L.R)
(WP : L.GradeGuards NB (wordCost (Fin 4) 6 δ * ‖ξ‖))
(S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 M.T))
(hgrowth : EulerPacketCylinderField.timeProfileChange S.growth hTime = α • L.g)
:
(forwardInitializedAngularPressureField M D hTime δ hδ ξ hs α L NB W LM WM BC hRc hcost hδ1 hα hR WP S
hgrowth).WordBound
6 (4 * L.R) (EulerPacketCylinderField.fixedVelocityGradeCost L.R S.H0 1) 0
noncomputable def
EulerPacketTerminalDatum.forwardInitializedCovectorRemainderField
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hTime : M.T = D.T)
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(α : ℝ)
(L : EulerTransversePacketForward.Budget D (Fin 4) 6)
(NB : EulerTransversePacketJoin.NormalBudget D 6 L.R)
(W : L.GradeGuards NB 1)
(LM : EulerMeanPacketProvider.Budget M 6 L.R)
(WM : LM.GradeGuards)
(BC :
EulerPacketCylinderField.CoefficientBudget
(EulerPacketCylinderField.sourceCoefficientData period M D (EulerTransversePacketProvider.InitialData.zero period D)
hTime))
(hRc : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) BC.Rc ≤ L.R)
(hcost : BC.termCost ≤ L.R)
(hδ1 : δ ≤ 1)
(hα : 0 < α)
(hR : wordRadius (Fin 4) δ ≤ L.R)
(WP : L.GradeGuards NB (wordCost (Fin 4) 6 δ * ‖ξ‖))
(S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 M.T))
(hgrowth : EulerPacketCylinderField.timeProfileChange S.growth hTime = α • L.g)
(N : ℕ)
(hN : 1 ≤ N)
(κ : ℝ)
:
EulerPacketCylinderField.Field period D.T (forwardInitializedCovectorRemainder M D δ hδ ξ hs α N κ)
Forward initialized covector remainder field as an element of Field period D.T (forwardInitializedCovectorRemainder M D δ hδ ξ hs α N κ).
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerPacketTerminalDatum.forwardInitializedCovectorRemainder_bound
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hTime : M.T = D.T)
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(α : ℝ)
(L : EulerTransversePacketForward.Budget D (Fin 4) 6)
(NB : EulerTransversePacketJoin.NormalBudget D 6 L.R)
(W : L.GradeGuards NB 1)
(LM : EulerMeanPacketProvider.Budget M 6 L.R)
(WM : LM.GradeGuards)
(BC :
EulerPacketCylinderField.CoefficientBudget
(EulerPacketCylinderField.sourceCoefficientData period M D (EulerTransversePacketProvider.InitialData.zero period D)
hTime))
(hRc : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) BC.Rc ≤ L.R)
(hcost : BC.termCost ≤ L.R)
(hδ1 : δ ≤ 1)
(hα : 0 < α)
(hR : wordRadius (Fin 4) δ ≤ L.R)
(WP : L.GradeGuards NB (wordCost (Fin 4) 6 δ * ‖ξ‖))
(S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 M.T))
(hgrowth : EulerPacketCylinderField.timeProfileChange S.growth hTime = α • L.g)
(N : ℕ)
(hN : 1 ≤ N)
(k : ℝ)
(hk : 4 ≤ k)
(hbase : EulerPacketCoarseMajorant.tailBase L.R S.H0 BC.termCost N ≤ k ^ (1 / 100))
:
noncomputable def
EulerPacketTerminalDatum.forwardInitializedPressureHessianCost
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
{D : EulerTransversePacketProvider.Data U}
{q : ℕ}
{R₀ : ℝ}
(NB : EulerTransversePacketJoin.NormalBudget D q R₀)
(R H0 Rc C : ℝ)
:
Forward initialized pressure hessian cost, constructed using fastHessianCost.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerPacketTerminalDatum.forwardInitializedAngularPressure_smooth
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(α t : ℝ)
:
ContDiff ℝ ↑⊤ fun (z : EulerSmoothLimit.Space × ℝ) => forwardInitializedAngularPressure D δ hδ ξ hs α (t, z)
theorem
EulerPacketTerminalDatum.forwardInitializedAngularPressure_second
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(α : ℝ)
(t : ↑(Set.Icc 0 D.T))
(z : EulerLiftedGradientSpace.LiftTangent)
:
EulerPacketGraphHessian.angularDerivative
(fun (w : EulerLiftedGradientSpace.LiftTangent) => forwardInitializedAngularPressure D δ hδ ξ hs α (↑t, w)) z = EulerPacketForwardShear.pressureCoefficient D ξ α t z.1 * deriv (EulerPeriodicProfile.profile δ) z.2
theorem
EulerPacketTerminalDatum.forwardInitializedPressure_hessian_bound
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(M : EulerMeanPacketProvider.Data)
(D : EulerTransversePacketProvider.Data U)
(hTime : M.T = D.T)
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(α : ℝ)
(L : EulerTransversePacketForward.Budget D (Fin 4) 6)
(NB : EulerTransversePacketJoin.NormalBudget D 6 L.R)
(W : L.GradeGuards NB 1)
(LM : EulerMeanPacketProvider.Budget M 6 L.R)
(WM : LM.GradeGuards)
(BC :
EulerPacketCylinderField.CoefficientBudget
(EulerPacketCylinderField.sourceCoefficientData period M D (EulerTransversePacketProvider.InitialData.zero period D)
hTime))
(hRc : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) BC.Rc ≤ L.R)
(hcost : BC.termCost ≤ L.R)
(hδ1 : δ ≤ 1)
(hα : 0 < α)
(hR : wordRadius (Fin 4) δ ≤ L.R)
(WP : L.GradeGuards NB (wordCost (Fin 4) 6 δ * ‖ξ‖))
(S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 M.T))
(hgrowth : EulerPacketCylinderField.timeProfileChange S.growth hTime = α • L.g)
(N : ℕ)
(hN : 1 ≤ N)
(k : ℝ)
(hk : 4 ≤ k)
(hbase : EulerPacketCoarseMajorant.tailBase L.R S.H0 BC.termCost N ≤ k ^ (1 / 100))
(X Y : ↑(Set.Icc 0 D.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space)
(hX : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), HasFDerivAt (X t) ((D.F.field t) x) x)
(hXY : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), X t (Y t x) = x)
(hY : Continuous (Function.uncurry Y))
(hdet :
∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space),
Matrix.det (EulerPacketPiola.operatorMatrix ((D.F.field t) x)) = 1)
(t : ↑(Set.Icc 0 D.T))
(x : EulerSmoothLimit.Space)
:
‖fderiv ℝ
(gradient fun (y : EulerSmoothLimit.Space) =>
forwardInitializedPressure M D δ hδ ξ hs α N k⁻¹ (↑t, Y t y, k * inner ℝ D.m₀ (Y t y)))
x - (EulerPacketForwardShear.pressureCoefficient D ξ α t (Y t x) * deriv (EulerPeriodicProfile.profile δ) (k * inner ℝ D.m₀ (Y t x))) • ((InnerProductSpace.rankOne ℝ) ((D.normal.field t) (Y t x))) ((D.normal.field t) (Y t x))‖ ≤ forwardInitializedPressureHessianCost NB L.R S.H0 L.Rc L.C₀ / k