The primary pressure is the actual mean-zero angular primitive of the normal residual. Its field satisfies the homogeneous packet equation.
noncomputable def
EulerTransversePacketPrimary.normalResidual
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(Y : EulerTransversePacketProvider.InitialData P D)
(t : ↑(Set.Icc 0 D.T))
(x : EulerLiftedGradientSpace.LiftDomain P)
:
Normal residual as an element of ℝ.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
EulerTransversePacketPrimary.residualPath
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(Y : EulerTransversePacketProvider.InitialData P D)
:
Residual path, given by sourceResidual P D.M D.normal D.normalLower D.normalLower_pos D.normal_lower 0 (velocityPath τ hτ hτT B Y).
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerTransversePacketPrimary.residualPath_orbit
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(Y : EulerTransversePacketProvider.InitialData P D)
:
ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a) (residualPath τ hτ hτT B Y)
theorem
EulerTransversePacketPrimary.residualPath_slice_smooth
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(Y : EulerTransversePacketProvider.InitialData P D)
(t : ↑(Set.Icc 0 D.T))
:
ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.translate P a) ((residualPath τ hτ hτT B Y) t)
theorem
EulerTransversePacketPrimary.residualPath_average_zero
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(Y : EulerTransversePacketProvider.InitialData P D)
(t : ↑(Set.Icc 0 D.T))
:
theorem
EulerTransversePacketPrimary.normalResidual_continuous
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(Y : EulerTransversePacketProvider.InitialData P D)
(t : ↑(Set.Icc 0 D.T))
:
Continuous (normalResidual τ hτ hτT B Y t)
theorem
EulerTransversePacketPrimary.normalResidual_smooth
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(Y : EulerTransversePacketProvider.InitialData P D)
(t : ↑(Set.Icc 0 D.T))
(x : EulerLiftedGradientSpace.LiftDomain P)
:
ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P (normalResidual τ hτ hτT B Y t) x)
theorem
EulerTransversePacketPrimary.residualPath_ae
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(Y : EulerTransversePacketProvider.InitialData P D)
(t : ↑(Set.Icc 0 D.T))
:
↑↑((residualPath τ hτ hτT B Y) t) =ᵐ[EulerLiftedGradientSpace.liftMeasure P] normalResidual τ hτ hτT B Y t
theorem
EulerTransversePacketPrimary.normalResidual_mean_zero
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(Y : EulerTransversePacketProvider.InitialData P D)
(t : ↑(Set.Icc 0 D.T))
(y : EulerSmoothLimit.Space)
:
noncomputable def
EulerTransversePacketPrimary.pressureField
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(Y : EulerTransversePacketProvider.InitialData P D)
(t : ↑(Set.Icc 0 D.T))
:
Pressure field, constructed using classicalPrimitive.
Equations
- EulerTransversePacketPrimary.pressureField τ hτ hτT B Y t = EulerCylinderScalarPrimitive.classicalPrimitive P (EulerTransversePacketPrimary.normalResidual τ hτ hτT B Y t) ⋯ ⋯
Instances For
theorem
EulerTransversePacketPrimary.pressureField_ae
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(Y : EulerTransversePacketProvider.InitialData P D)
(t : ↑(Set.Icc 0 D.T))
:
↑↑((pressurePath τ hτ hτT B Y) t) =ᵐ[EulerLiftedGradientSpace.liftMeasure P] pressureField τ hτ hτT B Y t
theorem
EulerTransversePacketPrimary.pressureField_smooth
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(Y : EulerTransversePacketProvider.InitialData P D)
(t : ↑(Set.Icc 0 D.T))
(x : EulerLiftedGradientSpace.LiftDomain P)
:
ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P (pressureField τ hτ hτT B Y t) x)
theorem
EulerTransversePacketPrimary.pressureField_eq_scalarPointField
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(Y : EulerTransversePacketProvider.InitialData P D)
(t : ↑(Set.Icc 0 D.T))
:
pressureField τ hτ hτT B Y t = EulerCylinderScalarPrimitive.scalarPointField P (pressurePath τ hτ hτT B Y) ⋯ t
theorem
EulerTransversePacketPrimary.scalar_eq_pressureField
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(Y : EulerTransversePacketProvider.InitialData P D)
(t : ↑(Set.Icc 0 D.T))
(x : EulerSmoothLimit.Space)
(θ : ℝ)
:
theorem
EulerTransversePacketPrimary.pressureField_angle
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(Y : EulerTransversePacketProvider.InitialData P D)
(t : ↑(Set.Icc 0 D.T))
(x : EulerSmoothLimit.Space)
(θ : ℝ)
:
HasDerivAt (fun (s : ℝ) => pressureField τ hτ hτT B Y t (x, ↑s)) (normalResidual τ hτ hτT B Y t (x, ↑θ)) θ
theorem
EulerTransversePacketPrimary.scalar_normalized
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(Y : EulerTransversePacketProvider.InitialData P D)
(t : ↑(Set.Icc 0 D.T))
(x : EulerSmoothLimit.Space)
:
theorem
EulerTransversePacketPrimary.normalResidual_zero_outside
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(Y : EulerTransversePacketProvider.InitialData P D)
(t : ↑(Set.Icc 0 D.T))
(y : EulerSmoothLimit.Space)
(hy : y ∉ D.support)
(θ : AddCircle P)
:
theorem
EulerTransversePacketPrimary.scalar_zero_outside
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(Y : EulerTransversePacketProvider.InitialData P D)
(t : ℝ)
(x : EulerSmoothLimit.Space)
(hx : x ∉ D.support)
(θ : ℝ)
:
theorem
EulerTransversePacketPrimary.scalarGradient_zero_outside
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(Y : EulerTransversePacketProvider.InitialData P D)
(t : ℝ)
(x : EulerSmoothLimit.Space)
(hx : x ∉ D.support)
(θ : ℝ)
:
theorem
EulerTransversePacketPrimary.field_balance
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(Y : EulerTransversePacketProvider.InitialData P D)
(t : ↑(Set.Icc 0 D.T))
(x : EulerLiftedGradientSpace.LiftDomain P)
:
EulerCylinderSmoothOrbit.pointField P (derivativePath τ hτ hτT B Y) ⋯ t x + ((D.M.field t) x.1) (EulerCylinderSmoothOrbit.pointField P (velocityPath τ hτ hτT B Y) ⋯ t x) + normalResidual τ hτ hτT B Y t x • (D.normal.field t) x.1 = 0
theorem
EulerTransversePacketPrimary.equation
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(Y : EulerTransversePacketProvider.InitialData P D)
(t : ↑(Set.Icc 0 D.T))
(x : EulerSmoothLimit.Space)
(θ : ℝ)
:
theorem
EulerTransversePacketPrimary.jet_equation
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(Y : EulerTransversePacketProvider.InitialData P D)
(t : ↑(Set.Icc 0 D.T))
(x : EulerSmoothLimit.Space)
(θ : ℝ)
:
theorem
EulerTransversePacketPrimary.normalResidual_odd
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(Y : EulerTransversePacketProvider.InitialData P D)
(hSym : ∀ (x : EulerSmoothLimit.Space), -x ∈ D.support ↔ x ∈ D.support)
(hF : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), (D.F.field t) (-x) = (D.F.field t) x)
(hM : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), (D.M.field t) (-x) = (D.M.field t) x)
(hH : ∀ (t : ↑(Set.Icc 0 (D.initial τ hτ ⋯).T)) (x : EulerSmoothLimit.Space), (B.H.field t) (-x) = (B.H.field t) x)
(hY : (EulerCylinderFieldReflection.reflection P) ↑Y.value = -↑Y.value)
(t : ↑(Set.Icc 0 D.T))
(x : EulerSmoothLimit.Space)
(θ : ℝ)
:
theorem
EulerTransversePacketPrimary.scalar_even
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(Y : EulerTransversePacketProvider.InitialData P D)
(hSym : ∀ (x : EulerSmoothLimit.Space), -x ∈ D.support ↔ x ∈ D.support)
(hF : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), (D.F.field t) (-x) = (D.F.field t) x)
(hM : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), (D.M.field t) (-x) = (D.M.field t) x)
(hH : ∀ (t : ↑(Set.Icc 0 (D.initial τ hτ ⋯).T)) (x : EulerSmoothLimit.Space), (B.H.field t) (-x) = (B.H.field t) x)
(hY : (EulerCylinderFieldReflection.reflection P) ↑Y.value = -↑Y.value)
(t : ↑(Set.Icc 0 D.T))
(x : EulerSmoothLimit.Space)
(θ : ℝ)
:
theorem
EulerTransversePacketPrimary.scalarGradient_odd
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(Y : EulerTransversePacketProvider.InitialData P D)
(hSym : ∀ (x : EulerSmoothLimit.Space), -x ∈ D.support ↔ x ∈ D.support)
(hF : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), (D.F.field t) (-x) = (D.F.field t) x)
(hM : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), (D.M.field t) (-x) = (D.M.field t) x)
(hH : ∀ (t : ↑(Set.Icc 0 (D.initial τ hτ ⋯).T)) (x : EulerSmoothLimit.Space), (B.H.field t) (-x) = (B.H.field t) x)
(hY : (EulerCylinderFieldReflection.reflection P) ↑Y.value = -↑Y.value)
(t : ↑(Set.Icc 0 D.T))
(x : EulerSmoothLimit.Space)
(θ : ℝ)
: