The actual exact lifted field is jointly differentiable in time and covering-space coordinates. Uniform bounded Sobolev evaluation supplies the time remainder estimate, so joint differentiability is a conclusion.

Joint differentiation through uniformly bounded evaluation operators. Strong continuity on the derivative vector suffices; operator-norm continuity or differentiability of the whole family of evaluation maps is unnecessary.

theorem EulerBoundedEvaluation.hasFDerivAt {X : Type u_1} {H : Type u_2} {V : Type u_3} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup H] [NormedSpace ℝ H] [NormedAddCommGroup V] [NormedSpace ℝ V] (E : X → H →L[ℝ] V) (C : ℝ) (hE : ∀ (x : X), ‖E x‖ ≤ C) (u : ℝ → H) (u' : H) (t : ℝ) (x : X) (hu : HasDerivAt u u' t) (D : X →L[ℝ] V) (hx : HasFDerivAt (fun (y : X) => (E y) (u t)) D x) (hc : ContinuousAt (fun (y : X) => (E y) u') x) : HasFDerivAt (fun (q : ℝ × X) => (E q.2) (u q.1)) (ContinuousLinearMap.toSpanSingleton ℝ ((E x) u') ∘SL ContinuousLinearMap.fst ℝ ℝ X + D ∘SL ContinuousLinearMap.snd ℝ ℝ X) (t, x)

noncomputable def EulerAllOrderCorrectionData.FieldTower.rawField {P T : ℝ} [Fact (0 < P)] (A : FieldTower P T) (hT : 0 ≤ T) (q : ℝ × EulerLiftedGradientSpace.LiftTangent) : EulerLiftedGradientSpace.Vector3

Raw field, given by A.pointField (projIcc 0 T hT q.1) (coveringMap P q.2).

Equations

• A.rawField hT q = A.pointField (Set.projIcc 0 T hT q.1) (EulerLiftedGradientSpace.coveringMap P q.2)

theorem EulerAllOrderCorrectionData.FieldTower.rawField_hasFDerivAt {P T : ℝ} [Fact (0 < P)] (A : FieldTower P T) (hT : 0 ≤ T) (t : ℝ) (ht : t ∈ Set.Icc 0 T) (u' : ↥(EulerCylinderSobolevSpace.SobolevSpace P 3)) (hd : HasDerivAt (EulerVolterraConvolution.extendPath T hT (A.realization 3)) u' t) (z : EulerLiftedGradientSpace.LiftTangent) : HasFDerivAt (A.rawField hT) (ContinuousLinearMap.toSpanSingleton ℝ ((EulerSobolevPointEvaluation.pointEvaluation P (EulerLiftedGradientSpace.coveringMap P z)) u') ∘SL ContinuousLinearMap.fst ℝ ℝ EulerLiftedGradientSpace.LiftTangent + EulerLiftedWeakDerivative.fieldFDeriv P (A.pointField ⟨t, ht⟩) (EulerLiftedGradientSpace.coveringMap P z) ∘SL ContinuousLinearMap.snd ℝ ℝ EulerLiftedGradientSpace.LiftTangent) (t, z)

noncomputable def EulerAllOrderDriftCorrection.ExactLiftedPacket.rawVelocity {P T : ℝ} [Fact (0 < P)] {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data P T} {B : Budget P hT A} (S : ExactLiftedPacket P hT A B) : ℝ × EulerLiftedGradientSpace.LiftTangent → EulerLiftedGradientSpace.Vector3

Raw velocity, given by S.velocity.rawField hT.le.

Equations

• S.rawVelocity = S.velocity.rawField ⋯

noncomputable def EulerAllOrderDriftCorrection.ExactLiftedPacket.rawPressure {P T : ℝ} [Fact (0 < P)] {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data P T} {B : Budget P hT A} (S : ExactLiftedPacket P hT A B) : ℝ × EulerLiftedGradientSpace.LiftTangent → EulerLiftedGradientSpace.Vector3

Raw pressure, given by S.pressure.rawField hT.le.

Equations

• S.rawPressure = S.pressure.rawField ⋯

theorem EulerAllOrderDriftCorrection.ExactLiftedPacket.rawVelocity_hasFDerivAt {P T : ℝ} [Fact (0 < P)] {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data P T} {B : Budget P hT A} (S : ExactLiftedPacket P hT A B) (t : ℝ) (ht : t ∈ Set.Ioo 0 T) (z : EulerLiftedGradientSpace.LiftTangent) : HasFDerivAt S.rawVelocity (ContinuousLinearMap.toSpanSingleton ℝ (S.pointTimeDerivative ⟨t, ⋯⟩ (EulerLiftedGradientSpace.coveringMap P z)) ∘SL ContinuousLinearMap.fst ℝ ℝ EulerLiftedGradientSpace.LiftTangent + EulerLiftedWeakDerivative.fieldFDeriv P (S.velocity.pointField ⟨t, ⋯⟩) (EulerLiftedGradientSpace.coveringMap P z) ∘SL ContinuousLinearMap.snd ℝ ℝ EulerLiftedGradientSpace.LiftTangent) (t, z)

theorem EulerAllOrderDriftCorrection.ExactLiftedPacket.raw_normalized_equation {P T : ℝ} [Fact (0 < P)] {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data P T} {B : Budget P hT A} (S : ExactLiftedPacket P hT A B) (t : ℝ) (ht : t ∈ Set.Ioo 0 T) (z : EulerLiftedGradientSpace.LiftTangent) : (fderiv ℝ S.rawVelocity (t, z)) (1, 0) + ((A.linear.coefficient ⟨t, ⋯⟩).coefficient (EulerLiftedGradientSpace.coveringMap P z)) (S.rawVelocity (t, z)) + (fderiv ℝ S.rawVelocity (t, z)) (0, EulerMetricTransport.transportDirection A.κ A.direction (S.rawVelocity (t, z))) + ∑ i : Fin 3, (S.rawVelocity (t, z)).ofLp i • (((A.quadratic i).coefficient ⟨t, ⋯⟩).coefficient (EulerLiftedGradientSpace.coveringMap P z)) (S.rawVelocity (t, z)) + ((A.metric.coefficient ⟨t, ⋯⟩).coefficient (EulerLiftedGradientSpace.coveringMap P z)) (S.rawPressure (t, z)) = 0

The normalized equation now uses the genuine full Fréchet derivative of the actual covering-space field, as required by physical coordinate change.