The exact Sobolev equation is the literal pointwise normalized equation for the canonical smooth representatives. No pointwise PDE is assumed.
noncomputable def
EulerAllOrderDriftCorrection.pointNonlinearity
(P : ℝ)
[Fact (0 < P)]
{T : ℝ}
(A : EulerAllOrderCorrectionData.Data P T)
(Z : EulerAllOrderCorrectionData.FieldTower P T)
(t : ↑(Set.Icc 0 T))
(x : EulerLiftedGradientSpace.LiftDomain P)
:
Point nonlinearity as an element of Vector3.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerAllOrderDriftCorrection.pointNonlinearity_continuous
(P : ℝ)
[Fact (0 < P)]
{T : ℝ}
(A : EulerAllOrderCorrectionData.Data P T)
(Z : EulerAllOrderCorrectionData.FieldTower P T)
(t : ↑(Set.Icc 0 T))
:
Continuous (pointNonlinearity P A Z t)
theorem
EulerAllOrderDriftCorrection.nonlinearity_value_ae
(P : ℝ)
[Fact (0 < P)]
{T : ℝ}
(A : EulerAllOrderCorrectionData.Data P T)
(Z : EulerAllOrderCorrectionData.FieldTower P T)
(q : ℕ)
(hq : 6 ≤ q)
(t : ↑(Set.Icc 0 T))
:
↑↑(EulerCylinderSobolevSpace.value P
(EulerCorrectionResidualCancellation.nonlinearity P (EulerAllOrderCorrectionData.Data.atOrder P A q) hq t
((Z.realization (q + 1)) t))) =ᵐ[EulerLiftedGradientSpace.liftMeasure P] pointNonlinearity P A Z t
theorem
EulerAllOrderDriftCorrection.pointEvaluation_nonlinearity
(P : ℝ)
[Fact (0 < P)]
{T : ℝ}
(A : EulerAllOrderCorrectionData.Data P T)
(Z : EulerAllOrderCorrectionData.FieldTower P T)
(q : ℕ)
(hq : 6 ≤ q)
(t : ↑(Set.Icc 0 T))
(x : EulerLiftedGradientSpace.LiftDomain P)
:
(EulerSobolevPointEvaluation.pointEvaluation P x)
((EulerCylinderSobolevSpace.restrictOperator P ⋯)
(EulerCorrectionResidualCancellation.nonlinearity P (EulerAllOrderCorrectionData.Data.atOrder P A q) hq t
((Z.realization (q + 1)) t))) = pointNonlinearity P A Z t x
noncomputable def
EulerAllOrderDriftCorrection.ExactLiftedPacket.pointTimeDerivative
{P : ℝ}
[Fact (0 < P)]
{T : ℝ}
{hT : 0 < T}
{A : EulerAllOrderCorrectionData.Data P T}
{B : Budget P hT A}
(S : ExactLiftedPacket P hT A B)
(t : ↑(Set.Icc 0 T))
(x : EulerLiftedGradientSpace.LiftDomain P)
:
Point time derivative, given by -pointNonlinearity P A S.velocity t x - (A.metric.coefficient t).coefficient x (S.pressure.pointField t x).
Equations
- S.pointTimeDerivative t x = -EulerAllOrderDriftCorrection.pointNonlinearity P A S.velocity t x - ((A.metric.coefficient t).coefficient x) (S.pressure.pointField t x)
Instances For
theorem
EulerAllOrderDriftCorrection.ExactLiftedPacket.pointField_hasDerivAt
{P : ℝ}
[Fact (0 < P)]
{T : ℝ}
{hT : 0 < T}
{A : EulerAllOrderCorrectionData.Data P T}
{B : Budget P hT A}
(S : ExactLiftedPacket P hT A B)
(x : EulerLiftedGradientSpace.LiftDomain P)
(t : ℝ)
(ht : t ∈ Set.Ioo 0 T)
:
HasDerivAt (fun (r : ℝ) => S.velocity.pointField (Set.projIcc 0 T ⋯ r) x) (S.pointTimeDerivative ⟨t, ⋯⟩ x) t
Bounded Sobolev evaluation differentiates the actual solved path.
theorem
EulerAllOrderDriftCorrection.ExactLiftedPacket.pointwise_equation
{P : ℝ}
[Fact (0 < P)]
{T : ℝ}
{hT : 0 < T}
{A : EulerAllOrderCorrectionData.Data P T}
{B : Budget P hT A}
(S : ExactLiftedPacket P hT A B)
(t : ↑(Set.Icc 0 T))
(x : EulerLiftedGradientSpace.LiftDomain P)
:
S.pointTimeDerivative t x + ((A.linear.coefficient t).coefficient x) (S.velocity.pointField t x) + (EulerLiftedWeakDerivative.fieldFDeriv P (S.velocity.pointField t) x)
(EulerMetricTransport.transportDirection A.κ A.direction (S.velocity.pointField t x)) + ∑ i : Fin 3,
(S.velocity.pointField t x).ofLp i • (((A.quadratic i).coefficient t).coefficient x) (S.velocity.pointField t x) + ((A.metric.coefficient t).coefficient x) (S.pressure.pointField t x) = 0
The canonical fields satisfy the literal normalized pointwise equation.