Literal packet operators and coefficient witnesses from the given analytic source data.
def
EulerPacketCylinderField.MatrixCoefficient.changeTime
{T T' : ℝ}
{raw : EulerPacketPointJets.Domain → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space}
(G : MatrixCoefficient T raw)
(h : T = T')
:
MatrixCoefficient T' raw
Change time, given by h ▸ G.
Equations
- G.changeTime h = h ▸ G
Instances For
def
EulerPacketCylinderField.VectorCoefficient.changeTime
{T T' : ℝ}
{raw : EulerPacketProfileRecursion.VectorField}
(G : VectorCoefficient T raw)
(h : T = T')
:
VectorCoefficient T' raw
Change time, given by h ▸ G.
Equations
- G.changeTime h = h ▸ G
Instances For
noncomputable def
EulerPacketCylinderField.sourceOperators
(P : ℝ)
[Fact (0 < P)]
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(I : EulerTransversePacketProvider.InitialData P D)
:
Every linear solve and the curl corrector is the concrete source construction.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
EulerPacketCylinderField.sourceCoefficientData
(P : ℝ)
[Fact (0 < P)]
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(I : EulerTransversePacketProvider.InitialData P D)
(hT : M.T = D.T)
:
CoefficientData P M.T (sourceOperators P M D I)
No regularity of a solved field or abstract operator family is an input here.
Equations
- One or more equations did not get rendered due to their size.