The actual forced transverse history on packet fields #
The forcing is an ordinary admissible cylinder path. Source deformation and Hessian data construct its zero-endpoint history, physical velocity, true time derivative, and scalar pressure path. No output regularity or equation is included in the input.
The literal spatial equation of the actual cylinder history #
The Hilbert-space projected equation is an equality of genuine L² fields. The adjoint multiplier identity turns it into the pointwise matrix equation almost everywhere. Its normal residual is exactly the scalar source in (11).
theorem
EulerCylinderDirichlet.Coefficients.coordinate_equation_ae
(P : ℝ)
[Fact (0 < P)]
{T : ℝ}
{U : Type u_1}
{E : Type u_2}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
(D : Coefficients T U E)
(f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P E)))
(t : ↑(Set.Icc 0 T))
:
∀ᵐ (x : EulerLiftedGradientSpace.LiftDomain P) ∂EulerLiftedGradientSpace.liftMeasure P, (EulerTransverseGramInverse.gram ((D.Q t) x.1)) (↑↑((accelerationPath P D f) t) x) = (ContinuousLinearMap.adjoint ((D.Q t) x.1))
(↑↑(f t) x - 2 • ((D.Q₁ t) x.1) (↑↑(((velocityPath P D) (EulerTimeLp.pathLp T ⋯ f)) t) x))
The exact source equation (10) for the actual cylinder representatives.
theorem
EulerCylinderDirichlet.Coefficients.physicalVelocity_ae
(P : ℝ)
[Fact (0 < P)]
{T : ℝ}
{U : Type u_1}
{E : Type u_2}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
(D : Coefficients T U E)
(f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P E)))
(t : ↑(Set.Icc 0 T))
:
↑↑((physicalVelocity P D f) t) =ᵐ[EulerLiftedGradientSpace.liftMeasure P] fun (x : EulerLiftedGradientSpace.LiftDomain P) =>
((D.Q t) x.1) (↑↑(((velocityPath P D) (EulerTimeLp.pathLp T ⋯ f)) t) x)
theorem
EulerCylinderDirichlet.Coefficients.physicalDerivative_ae
(P : ℝ)
[Fact (0 < P)]
{T : ℝ}
{U : Type u_1}
{E : Type u_2}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
(D : Coefficients T U E)
(f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P E)))
(t : ↑(Set.Icc 0 T))
:
↑↑((physicalDerivative P D f) t) =ᵐ[EulerLiftedGradientSpace.liftMeasure P] fun (x : EulerLiftedGradientSpace.LiftDomain P) =>
((D.Q₁ t) x.1) (↑↑(((velocityPath P D) (EulerTimeLp.pathLp T ⋯ f)) t) x) + ((D.Q t) x.1) (↑↑((accelerationPath P D f) t) x)
theorem
EulerCylinderDirichlet.Coefficients.physical_balance_ae
(P : ℝ)
[Fact (0 < P)]
{T : ℝ}
{U : Type u_1}
{E : Type u_2}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
(D : Coefficients T U E)
(f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P E)))
(M : ↑(Set.Icc 0 T) → EulerSmoothLimit.Space → E →L[ℝ] E)
(m : ↑(Set.Icc 0 T) → EulerSmoothLimit.Space → E)
(hm : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), m t x ≠ 0)
(hTangent : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (v : U), inner ℝ (m t x) (((D.Q t) x) v) = 0)
(hRange :
∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (η : E), inner ℝ (m t x) η = 0 → ∃ (v : U), ((D.Q t) x) v = η)
(hFlow : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), (D.Q₁ t) x = M t x ∘SL (D.Q t) x)
(t : ↑(Set.Icc 0 T))
:
∀ᵐ (x : EulerLiftedGradientSpace.LiftDomain P) ∂EulerLiftedGradientSpace.liftMeasure P, ↑↑((physicalDerivative P D f) t) x + (M t x.1) (↑↑((physicalVelocity P D f) t) x) + ((inner ℝ (m t x.1) (↑↑(f t) x) - 2 * inner ℝ (m t x.1) ((M t x.1) (↑↑((physicalVelocity P D f) t) x))) / ‖m t x.1‖ ^ 2) • m t x.1 = ↑↑(f t) x
The scalar normal source in (11), derived from the actual inverse.
@[reducible, inline]
noncomputable abbrev
EulerTransversePacketProvider.HistoryData.forcingPath
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
{D : Data U}
{raw : EulerPacketProfileRecursion.VectorField}
(G : Forcing P D raw)
:
Forcing path: an abbreviation for includePath P D.support D.support_measurable G.path.
Equations
Instances For
noncomputable def
EulerTransversePacketProvider.HistoryData.coordinatePath
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : Data U}
(B : HistoryData D)
{raw : EulerPacketProfileRecursion.VectorField}
(G : Forcing P D raw)
:
Coordinate path, given by B.coefficients.velocityPath P (pathLp D.T D.T_pos.le (forcingPath G)).
Equations
Instances For
noncomputable def
EulerTransversePacketProvider.HistoryData.coordinateDerivativePath
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : Data U}
(B : HistoryData D)
{raw : EulerPacketProfileRecursion.VectorField}
(G : Forcing P D raw)
:
Coordinate derivative path, given by B.coefficients.accelerationPath P (forcingPath G).
Equations
Instances For
noncomputable def
EulerTransversePacketProvider.HistoryData.velocityPath
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : Data U}
(B : HistoryData D)
{raw : EulerPacketProfileRecursion.VectorField}
(G : Forcing P D raw)
:
Velocity path, given by B.coefficients.physicalVelocity P (forcingPath G).
Equations
Instances For
noncomputable def
EulerTransversePacketProvider.HistoryData.derivativePath
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : Data U}
(B : HistoryData D)
{raw : EulerPacketProfileRecursion.VectorField}
(G : Forcing P D raw)
:
Derivative path, given by B.coefficients.physicalDerivative P (forcingPath G).
Equations
Instances For
noncomputable def
EulerTransversePacketProvider.HistoryData.pressurePath
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : Data U}
(B : HistoryData D)
{raw : EulerPacketProfileRecursion.VectorField}
(G : Forcing P D raw)
:
Pressure path, given by sourcePressure P D.M D.normal D.normalLower D.normalLower_pos D.normal_lower (forcingPath G) (B.velocityPath G).
Equations
Instances For
theorem
EulerTransversePacketProvider.HistoryData.coordinatePath_orbit
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : Data U}
(B : HistoryData D)
{raw : EulerPacketProfileRecursion.VectorField}
(G : Forcing P D raw)
:
ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a) (B.coordinatePath G)
theorem
EulerTransversePacketProvider.HistoryData.coordinateDerivativePath_orbit
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : Data U}
(B : HistoryData D)
{raw : EulerPacketProfileRecursion.VectorField}
(G : Forcing P D raw)
:
ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a) (B.coordinateDerivativePath G)
theorem
EulerTransversePacketProvider.HistoryData.velocityPath_orbit
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : Data U}
(B : HistoryData D)
{raw : EulerPacketProfileRecursion.VectorField}
(G : Forcing P D raw)
:
ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a) (B.velocityPath G)
theorem
EulerTransversePacketProvider.HistoryData.derivativePath_orbit
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : Data U}
(B : HistoryData D)
{raw : EulerPacketProfileRecursion.VectorField}
(G : Forcing P D raw)
:
ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a) (B.derivativePath G)
theorem
EulerTransversePacketProvider.HistoryData.pressurePath_orbit
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : Data U}
(B : HistoryData D)
{raw : EulerPacketProfileRecursion.VectorField}
(G : Forcing P D raw)
:
ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a) (B.pressurePath G)
theorem
EulerTransversePacketProvider.HistoryData.coordinatePath_time
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : Data U}
(B : HistoryData D)
{raw : EulerPacketProfileRecursion.VectorField}
(G : Forcing P D raw)
(t : ↑(Set.Icc 0 D.T))
:
HasDerivWithinAt (EulerVolterraConvolution.extendPath D.T ⋯ (B.coordinatePath G)) ((B.coordinateDerivativePath G) t)
(Set.Icc 0 D.T) ↑t
theorem
EulerTransversePacketProvider.HistoryData.velocityPath_time
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : Data U}
(B : HistoryData D)
{raw : EulerPacketProfileRecursion.VectorField}
(G : Forcing P D raw)
(t : ↑(Set.Icc 0 D.T))
:
HasDerivWithinAt (EulerVolterraConvolution.extendPath D.T ⋯ (B.velocityPath G)) ((B.derivativePath G) t) (Set.Icc 0 D.T)
↑t
theorem
EulerTransversePacketProvider.HistoryData.coordinatePath_supported
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : Data U}
(B : HistoryData D)
{raw : EulerPacketProfileRecursion.VectorField}
(G : Forcing P D raw)
(t : ↑(Set.Icc 0 D.T))
:
theorem
EulerTransversePacketProvider.HistoryData.velocityPath_supported
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : Data U}
(B : HistoryData D)
{raw : EulerPacketProfileRecursion.VectorField}
(G : Forcing P D raw)
(t : ↑(Set.Icc 0 D.T))
:
theorem
EulerTransversePacketProvider.HistoryData.derivativePath_supported
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : Data U}
(B : HistoryData D)
{raw : EulerPacketProfileRecursion.VectorField}
(G : Forcing P D raw)
(t : ↑(Set.Icc 0 D.T))
:
theorem
EulerTransversePacketProvider.HistoryData.coordinatePath_mean_zero
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : Data U}
(B : HistoryData D)
{raw : EulerPacketProfileRecursion.VectorField}
(G : Forcing P D raw)
(t : ↑(Set.Icc 0 D.T))
:
theorem
EulerTransversePacketProvider.HistoryData.velocityPath_mean_zero
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : Data U}
(B : HistoryData D)
{raw : EulerPacketProfileRecursion.VectorField}
(G : Forcing P D raw)
(t : ↑(Set.Icc 0 D.T))
:
theorem
EulerTransversePacketProvider.HistoryData.derivativePath_mean_zero
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : Data U}
(B : HistoryData D)
{raw : EulerPacketProfileRecursion.VectorField}
(G : Forcing P D raw)
(t : ↑(Set.Icc 0 D.T))
:
noncomputable def
EulerTransversePacketProvider.HistoryData.field
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : Data U}
(B : HistoryData D)
{raw : EulerPacketProfileRecursion.VectorField}
(G : Forcing P D raw)
(t : ↑(Set.Icc 0 D.T))
:
Field, given by pointField P (B.velocityPath G) (B.velocityPath_orbit G) t.
Equations
- B.field G t = EulerCylinderSmoothOrbit.pointField P (B.velocityPath G) ⋯ t
Instances For
noncomputable def
EulerTransversePacketProvider.HistoryData.derivativeField
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : Data U}
(B : HistoryData D)
{raw : EulerPacketProfileRecursion.VectorField}
(G : Forcing P D raw)
(t : ↑(Set.Icc 0 D.T))
:
Derivative field, given by pointField P (B.derivativePath G) (B.derivativePath_orbit G) t.
Equations
- B.derivativeField G t = EulerCylinderSmoothOrbit.pointField P (B.derivativePath G) ⋯ t
Instances For
theorem
EulerTransversePacketProvider.HistoryData.field_smooth
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : Data U}
(B : HistoryData D)
{raw : EulerPacketProfileRecursion.VectorField}
(G : Forcing P D raw)
(t : ↑(Set.Icc 0 D.T))
(x : EulerLiftedGradientSpace.LiftDomain P)
:
ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P (B.field G t) x)
theorem
EulerTransversePacketProvider.HistoryData.derivativeField_smooth
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : Data U}
(B : HistoryData D)
{raw : EulerPacketProfileRecursion.VectorField}
(G : Forcing P D raw)
(t : ↑(Set.Icc 0 D.T))
(x : EulerLiftedGradientSpace.LiftDomain P)
:
ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P (B.derivativeField G t) x)
theorem
EulerTransversePacketProvider.HistoryData.field_ae
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : Data U}
(B : HistoryData D)
{raw : EulerPacketProfileRecursion.VectorField}
(G : Forcing P D raw)
(t : ↑(Set.Icc 0 D.T))
:
↑↑((B.velocityPath G) t) =ᵐ[EulerLiftedGradientSpace.liftMeasure P] B.field G t
theorem
EulerTransversePacketProvider.HistoryData.derivativeField_ae
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : Data U}
(B : HistoryData D)
{raw : EulerPacketProfileRecursion.VectorField}
(G : Forcing P D raw)
(t : ↑(Set.Icc 0 D.T))
:
↑↑((B.derivativePath G) t) =ᵐ[EulerLiftedGradientSpace.liftMeasure P] B.derivativeField G t
theorem
EulerTransversePacketProvider.HistoryData.field_hasDerivWithinAt
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : Data U}
(B : HistoryData D)
{raw : EulerPacketProfileRecursion.VectorField}
(G : Forcing P D raw)
(t : ↑(Set.Icc 0 D.T))
(x : EulerLiftedGradientSpace.LiftDomain P)
:
HasDerivWithinAt (fun (s : ℝ) => B.field G (D.clamp s) x) (B.derivativeField G t x) (Set.Icc 0 D.T) ↑t
theorem
EulerTransversePacketProvider.HistoryData.field_zero_outside
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : Data U}
(B : HistoryData D)
{raw : EulerPacketProfileRecursion.VectorField}
(G : Forcing P D raw)
(t : ↑(Set.Icc 0 D.T))
(x : EulerLiftedGradientSpace.LiftDomain P)
(hx : x.1 ∉ D.support)
:
theorem
EulerTransversePacketProvider.HistoryData.derivativeField_zero_outside
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : Data U}
(B : HistoryData D)
{raw : EulerPacketProfileRecursion.VectorField}
(G : Forcing P D raw)
(t : ↑(Set.Icc 0 D.T))
(x : EulerLiftedGradientSpace.LiftDomain P)
(hx : x.1 ∉ D.support)
:
theorem
EulerTransversePacketProvider.HistoryData.normal_ne_zero
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
{D : Data U}
(t : ↑(Set.Icc 0 D.T))
(x : EulerSmoothLimit.Space)
:
theorem
EulerTransversePacketProvider.HistoryData.balance_ae
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : Data U}
(B : HistoryData D)
{raw : EulerPacketProfileRecursion.VectorField}
(G : Forcing P D raw)
(t : ↑(Set.Icc 0 D.T))
:
∀ᵐ (x : EulerLiftedGradientSpace.LiftDomain P) ∂EulerLiftedGradientSpace.liftMeasure P, ↑↑((B.derivativePath G) t) x + ((D.M.field t) x.1) (↑↑((B.velocityPath G) t) x) + ((inner ℝ ((D.normal.field t) x.1) (↑↑((forcingPath G) t) x) - 2 * inner ℝ ((D.normal.field t) x.1) (((D.M.field t) x.1) (↑↑((B.velocityPath G) t) x))) / ‖(D.normal.field t) x.1‖ ^ 2) • (D.normal.field t) x.1 = ↑↑((forcingPath G) t) x
theorem
EulerTransversePacketProvider.HistoryData.field_tangent
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : Data U}
(B : HistoryData D)
{raw : EulerPacketProfileRecursion.VectorField}
(G : Forcing P D raw)
(t : ↑(Set.Icc 0 D.T))
(x : EulerLiftedGradientSpace.LiftDomain P)
: