The actual source history with prescribed compact terminal displacement.
Y.value is an L² field of reference-plane coordinates. It is passed to
the constructed affine-endpoint inverse, not imposed as a solution law.
noncomputable def
EulerTransversePacketEndpoint.displacementPath
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
(B : EulerTransversePacketProvider.HistoryData D)
(Y : EulerTransversePacketProvider.InitialData P D)
:
Displacement path, given by B.coefficients.endpointDisplacement P (Y.value : CylinderL2 P U).
Equations
Instances For
noncomputable def
EulerTransversePacketEndpoint.coordinatePath
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
(B : EulerTransversePacketProvider.HistoryData D)
(Y : EulerTransversePacketProvider.InitialData P D)
:
Coordinate path, given by B.coefficients.endpointCoordinate P (Y.value : CylinderL2 P U).
Equations
Instances For
noncomputable def
EulerTransversePacketEndpoint.coordinateDerivativePath
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
(B : EulerTransversePacketProvider.HistoryData D)
(Y : EulerTransversePacketProvider.InitialData P D)
:
Coordinate derivative path, given by B.coefficients.endpointAcceleration P (Y.value : CylinderL2 P U).
Equations
Instances For
noncomputable def
EulerTransversePacketEndpoint.velocityPath
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
(B : EulerTransversePacketProvider.HistoryData D)
(Y : EulerTransversePacketProvider.InitialData P D)
:
Velocity path, given by B.coefficients.endpointVelocity P (Y.value : CylinderL2 P U).
Equations
Instances For
noncomputable def
EulerTransversePacketEndpoint.derivativePath
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
(B : EulerTransversePacketProvider.HistoryData D)
(Y : EulerTransversePacketProvider.InitialData P D)
:
Derivative path, given by B.coefficients.endpointDerivative P (Y.value : CylinderL2 P U).
Equations
Instances For
theorem
EulerTransversePacketEndpoint.displacement_initial
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
(B : EulerTransversePacketProvider.HistoryData D)
(Y : EulerTransversePacketProvider.InitialData P D)
:
theorem
EulerTransversePacketEndpoint.displacement_terminal
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
(B : EulerTransversePacketProvider.HistoryData D)
(Y : EulerTransversePacketProvider.InitialData P D)
:
theorem
EulerTransversePacketEndpoint.coordinatePath_orbit
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
(B : EulerTransversePacketProvider.HistoryData D)
(Y : EulerTransversePacketProvider.InitialData P D)
:
ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a) (coordinatePath B Y)
theorem
EulerTransversePacketEndpoint.coordinateDerivativePath_orbit
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
(B : EulerTransversePacketProvider.HistoryData D)
(Y : EulerTransversePacketProvider.InitialData P D)
:
ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a) (coordinateDerivativePath B Y)
theorem
EulerTransversePacketEndpoint.velocityPath_orbit
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
(B : EulerTransversePacketProvider.HistoryData D)
(Y : EulerTransversePacketProvider.InitialData P D)
:
ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a) (velocityPath B Y)
theorem
EulerTransversePacketEndpoint.derivativePath_orbit
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
(B : EulerTransversePacketProvider.HistoryData D)
(Y : EulerTransversePacketProvider.InitialData P D)
:
ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a) (derivativePath B Y)
theorem
EulerTransversePacketEndpoint.displacementPath_time
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
(B : EulerTransversePacketProvider.HistoryData D)
(Y : EulerTransversePacketProvider.InitialData P D)
(t : ↑(Set.Icc 0 D.T))
:
HasDerivWithinAt (EulerVolterraConvolution.extendPath D.T ⋯ (displacementPath B Y)) ((coordinatePath B Y) t)
(Set.Icc 0 D.T) ↑t
theorem
EulerTransversePacketEndpoint.coordinatePath_time
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
(B : EulerTransversePacketProvider.HistoryData D)
(Y : EulerTransversePacketProvider.InitialData P D)
(t : ↑(Set.Icc 0 D.T))
:
HasDerivWithinAt (EulerVolterraConvolution.extendPath D.T ⋯ (coordinatePath B Y)) ((coordinateDerivativePath B Y) t)
(Set.Icc 0 D.T) ↑t
theorem
EulerTransversePacketEndpoint.velocityPath_time
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
(B : EulerTransversePacketProvider.HistoryData D)
(Y : EulerTransversePacketProvider.InitialData P D)
(t : ↑(Set.Icc 0 D.T))
:
HasDerivWithinAt (EulerVolterraConvolution.extendPath D.T ⋯ (velocityPath B Y)) ((derivativePath B Y) t) (Set.Icc 0 D.T)
↑t
theorem
EulerTransversePacketEndpoint.coordinatePath_supported
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
(B : EulerTransversePacketProvider.HistoryData D)
(Y : EulerTransversePacketProvider.InitialData P D)
(t : ↑(Set.Icc 0 D.T))
:
theorem
EulerTransversePacketEndpoint.velocityPath_supported
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
(B : EulerTransversePacketProvider.HistoryData D)
(Y : EulerTransversePacketProvider.InitialData P D)
(t : ↑(Set.Icc 0 D.T))
:
theorem
EulerTransversePacketEndpoint.derivativePath_supported
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
(B : EulerTransversePacketProvider.HistoryData D)
(Y : EulerTransversePacketProvider.InitialData P D)
(t : ↑(Set.Icc 0 D.T))
:
theorem
EulerTransversePacketEndpoint.coordinatePath_mean_zero
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
(B : EulerTransversePacketProvider.HistoryData D)
(Y : EulerTransversePacketProvider.InitialData P D)
(t : ↑(Set.Icc 0 D.T))
:
theorem
EulerTransversePacketEndpoint.velocityPath_mean_zero
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
(B : EulerTransversePacketProvider.HistoryData D)
(Y : EulerTransversePacketProvider.InitialData P D)
(t : ↑(Set.Icc 0 D.T))
:
theorem
EulerTransversePacketEndpoint.derivativePath_mean_zero
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
(B : EulerTransversePacketProvider.HistoryData D)
(Y : EulerTransversePacketProvider.InitialData P D)
(t : ↑(Set.Icc 0 D.T))
:
noncomputable def
EulerTransversePacketEndpoint.terminalInitial
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
(B : EulerTransversePacketProvider.HistoryData D)
(Y : EulerTransversePacketProvider.InitialData P D)
:
Terminal initial, bundling value, orbit, mean_zero.
Equations
- EulerTransversePacketEndpoint.terminalInitial B Y = { value := ⟨(EulerTransversePacketEndpoint.coordinatePath B Y) ⟨D.T, ⋯⟩, ⋯⟩, orbit := ⋯, mean_zero := ⋯ }
Instances For
theorem
EulerTransversePacketEndpoint.velocityPath_ae
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
(B : EulerTransversePacketProvider.HistoryData D)
(Y : EulerTransversePacketProvider.InitialData P D)
(t : ↑(Set.Icc 0 D.T))
:
↑↑((velocityPath B Y) t) =ᵐ[EulerLiftedGradientSpace.liftMeasure P] fun (x : EulerLiftedGradientSpace.LiftDomain P) =>
((D.frame.field t) x.1) (↑↑((coordinatePath B Y) t) x)
theorem
EulerTransversePacketEndpoint.balance_ae
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
(B : EulerTransversePacketProvider.HistoryData D)
(Y : EulerTransversePacketProvider.InitialData P D)
(t : ↑(Set.Icc 0 D.T))
:
∀ᵐ (x : EulerLiftedGradientSpace.LiftDomain P) ∂EulerLiftedGradientSpace.liftMeasure P, ↑↑((derivativePath B Y) t) x + ((D.M.field t) x.1) (↑↑((velocityPath B Y) t) x) + (-(2 * inner ℝ ((D.normal.field t) x.1) (((D.M.field t) x.1) (↑↑((velocityPath B Y) t) x))) / ‖(D.normal.field t) x.1‖ ^ 2) • (D.normal.field t) x.1 = 0