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.
The initialized finite pressure has its actual leading angular force and a uniformly small covector remainder.
theorem
EulerPacketTerminalDatum.initializedProfiles_one_highPressure
(M : EulerMeanPacketProvider.Data)
{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τ ⋯))
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(α : ℝ)
:
(initializedProfiles M D τ hτ hτT B δ hδ ξ hs α 1).highPressure = EulerTransversePacketPrimary.scalar τ hτ hτT B (initialData D δ hδ (α • ξ) hs)
theorem
EulerPacketTerminalDatum.initializedProfiles_one_meanPressure
(M : EulerMeanPacketProvider.Data)
{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τ ⋯))
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(α : ℝ)
:
noncomputable def
EulerPacketTerminalDatum.initializedAngularPressure
{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τ ⋯))
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(α : ℝ)
:
Initialized angular pressure, defined pointwise by (pressureJet (scalar τ hτ hτT B (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.initializedCovectorRemainder
(M : EulerMeanPacketProvider.Data)
{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τ ⋯))
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(α : ℝ)
(N : ℕ)
(κ : ℝ)
:
Initialized covector remainder, given by covectorRemainder (N := N) (a := initializedProfiles M D τ hτ hτT B δ hδ ξ hs α) D.m₀ κ.
Equations
- EulerPacketTerminalDatum.initializedCovectorRemainder M D τ hτ hτT B δ hδ ξ hs α N κ = EulerPacketPressure.covectorRemainder D.m₀ κ
Instances For
theorem
EulerPacketTerminalDatum.initializedPressure_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 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(δ : ℝ)
(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) =>
initializedPressure M D τ hτ hτT B δ hδ ξ hs α N k⁻¹ (↑t, Y y, k * inner ℝ D.m₀ (Y y)))
x = EulerPacketGraphHessian.fastForce
(fun (z : EulerLiftedGradientSpace.LiftTangent) => initializedAngularPressure D τ hτ hτT B δ 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)))
(initializedCovectorRemainder M D τ hτ hτT B δ hδ ξ hs α N k⁻¹ (↑t, Y x, k * inner ℝ D.m₀ (Y x)))
noncomputable def
EulerPacketTerminalDatum.initializedPressureBudget
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hTime : M.T = D.T)
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(α : ℝ)
(L : EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) 6)
(H : EulerTransversePacketPrimary.Budget L)
(NB : EulerTransversePacketJoin.NormalBudget D 6 L.R)
(W : L.GradeGuards NB)
(LM : EulerMeanPacketProvider.Budget M 6 L.R)
(WM : LM.GradeGuards)
(BC :
EulerPacketCylinderField.CoefficientBudget
(EulerPacketCylinderField.joinedSourceCoefficientData period M D τ hτ hτT B 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 : H.GradeGuards NB (wordCost (Fin 4) 6 δ * ‖ξ‖))
(S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 M.T))
(hgrowth : EulerPacketCylinderField.timeProfileChange S.growth hTime = α • L.fullProfile)
(p : ℕ)
:
EulerPacketCylinderField.PressureBudget period M.T ⋯ D.m₀ (initializedProfiles M D τ hτ hτT B δ hδ ξ hs α p) S L.R p
Initialized pressure budget, constructed using Classical.choice.
Equations
- EulerPacketTerminalDatum.initializedPressureBudget M D hTime τ hτ hτT B δ hδ ξ hs α L H NB W LM WM BC hRc hcost hδ1 hα hR WP S hgrowth p = Classical.choice ⋯
Instances For
noncomputable def
EulerPacketTerminalDatum.initializedAngularPressureField
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hTime : M.T = D.T)
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(α : ℝ)
(L : EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) 6)
(H : EulerTransversePacketPrimary.Budget L)
(NB : EulerTransversePacketJoin.NormalBudget D 6 L.R)
(W : L.GradeGuards NB)
(LM : EulerMeanPacketProvider.Budget M 6 L.R)
(WM : LM.GradeGuards)
(BC :
EulerPacketCylinderField.CoefficientBudget
(EulerPacketCylinderField.joinedSourceCoefficientData period M D τ hτ hτT B 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 : H.GradeGuards NB (wordCost (Fin 4) 6 δ * ‖ξ‖))
(S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 M.T))
(hgrowth : EulerPacketCylinderField.timeProfileChange S.growth hTime = α • L.fullProfile)
:
EulerPacketCylinderField.Field period D.T fun (z : EulerPacketPointJets.Domain) =>
initializedAngularPressure D τ hτ hτT B δ hδ ξ hs α z • D.m₀
Initialized angular pressure field as an element of Field period D.T (fun z => initializedAngularPressure D τ hτ hτT B δ hδ ξ hs α z • D.m₀).
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerPacketTerminalDatum.initializedAngularPressure_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 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(α : ℝ)
(L : EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) 6)
(H : EulerTransversePacketPrimary.Budget L)
(NB : EulerTransversePacketJoin.NormalBudget D 6 L.R)
(W : L.GradeGuards NB)
(LM : EulerMeanPacketProvider.Budget M 6 L.R)
(WM : LM.GradeGuards)
(BC :
EulerPacketCylinderField.CoefficientBudget
(EulerPacketCylinderField.joinedSourceCoefficientData period M D τ hτ hτT B 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 : H.GradeGuards NB (wordCost (Fin 4) 6 δ * ‖ξ‖))
(S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 M.T))
(hgrowth : EulerPacketCylinderField.timeProfileChange S.growth hTime = α • L.fullProfile)
:
(initializedAngularPressureField M D hTime τ hτ hτT B δ hδ ξ hs α L H 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.initializedCovectorRemainderField
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hTime : M.T = D.T)
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(α : ℝ)
(L : EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) 6)
(H : EulerTransversePacketPrimary.Budget L)
(NB : EulerTransversePacketJoin.NormalBudget D 6 L.R)
(W : L.GradeGuards NB)
(LM : EulerMeanPacketProvider.Budget M 6 L.R)
(WM : LM.GradeGuards)
(BC :
EulerPacketCylinderField.CoefficientBudget
(EulerPacketCylinderField.joinedSourceCoefficientData period M D τ hτ hτT B 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 : H.GradeGuards NB (wordCost (Fin 4) 6 δ * ‖ξ‖))
(S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 M.T))
(hgrowth : EulerPacketCylinderField.timeProfileChange S.growth hTime = α • L.fullProfile)
(N : ℕ)
(hN : 1 ≤ N)
(κ : ℝ)
:
EulerPacketCylinderField.Field period D.T (initializedCovectorRemainder M D τ hτ hτT B δ hδ ξ hs α N κ)
Initialized covector remainder field as an element of Field period D.T (initializedCovectorRemainder M D τ hτ hτT B δ hδ ξ hs α N κ).
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerPacketTerminalDatum.initializedCovectorRemainder_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 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(α : ℝ)
(L : EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) 6)
(H : EulerTransversePacketPrimary.Budget L)
(NB : EulerTransversePacketJoin.NormalBudget D 6 L.R)
(W : L.GradeGuards NB)
(LM : EulerMeanPacketProvider.Budget M 6 L.R)
(WM : LM.GradeGuards)
(BC :
EulerPacketCylinderField.CoefficientBudget
(EulerPacketCylinderField.joinedSourceCoefficientData period M D τ hτ hτT B 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 : H.GradeGuards NB (wordCost (Fin 4) 6 δ * ‖ξ‖))
(S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 M.T))
(hgrowth : EulerPacketCylinderField.timeProfileChange S.growth hTime = α • L.fullProfile)
(N : ℕ)
(hN : 1 ≤ N)
(k : ℝ)
(hk : 4 ≤ k)
(hbase : EulerPacketCoarseMajorant.tailBase L.R S.H0 BC.termCost N ≤ k ^ (1 / 100))
:
The leading pressure tensor of the actual joined primary. Both angular derivatives below are derivatives of its constructed scalar pressure.
noncomputable def
EulerPacketPrimaryPressure.coefficient
{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τ ⋯))
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(a : ℝ)
(t : ↑(Set.Icc 0 D.T))
(x : EulerSmoothLimit.Space)
:
Coefficient, given by -(2*a*⟪D.normal.field t x, D.M.field t x (canonicalVelocity τ hτ hτT B ξ hs t x)⟫_ℝ)/‖D.normal.field t x‖^2.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerPacketPrimaryPressure.scalar_hasDerivAt
{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τ ⋯))
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(a : ℝ)
(t : ↑(Set.Icc 0 D.T))
(x : EulerSmoothLimit.Space)
(θ : ℝ)
:
HasDerivAt
(fun (s : ℝ) =>
EulerTransversePacketPrimary.scalar τ hτ hτT B (EulerPacketTerminalDatum.initialData D δ hδ (a • ξ) hs) (↑t, x, s))
(coefficient τ hτ hτT B ξ hs a t x * EulerPeriodicProfile.profile δ θ) θ
theorem
EulerPacketPrimaryPressure.scalar_deriv
{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τ ⋯))
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(a : ℝ)
(t : ↑(Set.Icc 0 D.T))
(x : EulerSmoothLimit.Space)
(θ : ℝ)
:
deriv
(fun (s : ℝ) =>
EulerTransversePacketPrimary.scalar τ hτ hτT B (EulerPacketTerminalDatum.initialData D δ hδ (a • ξ) hs)
(↑t, x, s))
θ = coefficient τ hτ hτT B ξ hs a t x * EulerPeriodicProfile.profile δ θ
theorem
EulerPacketPrimaryPressure.scalar_deriv_hasDerivAt
{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τ ⋯))
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(a : ℝ)
(t : ↑(Set.Icc 0 D.T))
(x : EulerSmoothLimit.Space)
(θ : ℝ)
:
HasDerivAt
(deriv fun (s : ℝ) =>
EulerTransversePacketPrimary.scalar τ hτ hτT B (EulerPacketTerminalDatum.initialData D δ hδ (a • ξ) hs) (↑t, x, s))
(coefficient τ hτ hτT B ξ hs a t x * deriv (EulerPeriodicProfile.profile δ) θ) θ
theorem
EulerPacketPrimaryPressure.scalar_second_deriv
{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τ ⋯))
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(a : ℝ)
(t : ↑(Set.Icc 0 D.T))
(x : EulerSmoothLimit.Space)
(θ : ℝ)
:
deriv
(deriv fun (s : ℝ) =>
EulerTransversePacketPrimary.scalar τ hτ hτT B (EulerPacketTerminalDatum.initialData D δ hδ (a • ξ) hs)
(↑t, x, s))
θ = coefficient τ hτ hτT B ξ hs a t x * deriv (EulerPeriodicProfile.profile δ) θ
theorem
EulerPacketPrimaryPressure.scalar_second_deriv_zero
{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τ ⋯))
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(a : ℝ)
(t : ↑(Set.Icc 0 D.T))
(x : EulerSmoothLimit.Space)
:
deriv
(deriv fun (s : ℝ) =>
EulerTransversePacketPrimary.scalar τ hτ hτT B (EulerPacketTerminalDatum.initialData D δ hδ (a • ξ) hs)
(↑t, x, s))
0 = coefficient τ hτ hτT B ξ hs a t x / δ
noncomputable def
EulerPacketPrimaryPressure.physicalPressure
{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τ ⋯))
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(a k : ℝ)
(t : ↑(Set.Icc 0 D.T))
(Y : EulerSmoothLimit.Space → EulerSmoothLimit.Space)
(x : EulerSmoothLimit.Space)
:
Physical pressure, given by k⁻¹^2 * scalar τ hτ hτT B (initialData D δ hδ (a • ξ) hs) (t,(Y x,k*⟪D.m₀,Y x⟫_ℝ)).
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
EulerPacketPrimaryPressure.hessianRemainder
{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τ ⋯))
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(a k : ℝ)
(t : ↑(Set.Icc 0 D.T))
(Y : EulerSmoothLimit.Space → EulerSmoothLimit.Space)
(x : EulerSmoothLimit.Space)
:
Hessian remainder, given by lowerHessian (fun z => scalar τ hτ hτT B (initialData D δ hδ (a • ξ) hs) (t,z)) k D.m₀ Y (fun y => D.FInv.field t (Y y)) x.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerPacketPrimaryPressure.physicalPressure_hessian
{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τ ⋯))
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(a k : ℝ)
(hk : k ≠ 0)
(t : ↑(Set.Icc 0 D.T))
(Y : EulerSmoothLimit.Space → EulerSmoothLimit.Space)
(hY : ∀ (x : EulerSmoothLimit.Space), HasFDerivAt Y ((D.FInv.field t) (Y x)) x)
(x : EulerSmoothLimit.Space)
:
fderiv ℝ (gradient (physicalPressure τ hτ hτT B δ hδ ξ hs a k t Y)) x = (coefficient τ hτ hτT B ξ hs a t (Y x) * deriv (EulerPeriodicProfile.profile δ) (k * inner ℝ D.m₀ (Y x))) • ((InnerProductSpace.rankOne ℝ) ((D.normal.field t) (Y x))) ((D.normal.field t) (Y x)) + hessianRemainder τ hτ hτT B δ hδ ξ hs a k t Y x
The leading term is the literal normal tensor in source (20); the remainder contains only terms with at least one factor of k⁻¹.
theorem
EulerPacketPrimaryPressure.physicalPressure_hessian_of_inverse
{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τ ⋯))
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(a k : ℝ)
(hk : k ≠ 0)
(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))
(t : ↑(Set.Icc 0 D.T))
(x : EulerSmoothLimit.Space)
:
fderiv ℝ (gradient (physicalPressure τ hτ hτT B δ hδ ξ hs a k t (Y t))) x = (coefficient τ hτ hτT B ξ hs a 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)) + hessianRemainder τ hτ hτT B δ hδ ξ hs a k t (Y t) x
noncomputable def
EulerPacketTerminalDatum.initializedPressureHessianCost
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
{D : EulerTransversePacketProvider.Data U}
{q : ℕ}
{R₀ : ℝ}
(NB : EulerTransversePacketJoin.NormalBudget D q R₀)
(R H0 Rc C : ℝ)
:
Initialized pressure hessian cost, constructed using fastHessianCost.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerPacketTerminalDatum.initializedAngularPressure_smooth
{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τ ⋯))
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(α t : ℝ)
:
ContDiff ℝ ↑⊤ fun (z : EulerSmoothLimit.Space × ℝ) => initializedAngularPressure D τ hτ hτT B δ hδ ξ hs α (t, z)
theorem
EulerPacketTerminalDatum.initializedAngularPressure_second
{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τ ⋯))
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(α : ℝ)
(t : ↑(Set.Icc 0 D.T))
(z : EulerLiftedGradientSpace.LiftTangent)
:
EulerPacketGraphHessian.angularDerivative
(fun (w : EulerLiftedGradientSpace.LiftTangent) => initializedAngularPressure D τ hτ hτT B δ hδ ξ hs α (↑t, w)) z = EulerPacketPrimaryPressure.coefficient τ hτ hτT B ξ hs α t z.1 * deriv (EulerPeriodicProfile.profile δ) z.2
theorem
EulerPacketTerminalDatum.initializedPressure_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 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(α : ℝ)
(L : EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) 6)
(H : EulerTransversePacketPrimary.Budget L)
(NB : EulerTransversePacketJoin.NormalBudget D 6 L.R)
(W : L.GradeGuards NB)
(LM : EulerMeanPacketProvider.Budget M 6 L.R)
(WM : LM.GradeGuards)
(BC :
EulerPacketCylinderField.CoefficientBudget
(EulerPacketCylinderField.joinedSourceCoefficientData period M D τ hτ hτT B 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 : H.GradeGuards NB (wordCost (Fin 4) 6 δ * ‖ξ‖))
(S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 M.T))
(hgrowth : EulerPacketCylinderField.timeProfileChange S.growth hTime = α • L.fullProfile)
(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) =>
initializedPressure M D τ hτ hτT B δ hδ ξ hs α N k⁻¹ (↑t, Y t y, k * inner ℝ D.m₀ (Y t y)))
x - (EulerPacketPrimaryPressure.coefficient τ hτ hτT B ξ hs α 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))‖ ≤ initializedPressureHessianCost NB L.R S.H0 L.Rc L.C₀ / k