The actual normalized scalar pressure for the transverse history

The pressure is the literal mean-zero angular integral of the normal residual of the constructed history. Its L² realization, zero mean, spatial smoothness, support, and pointwise equation (11) are proved here.

@[reducible, inline]

noncomputable abbrev EulerTransversePacketProvider.HistoryData.forceField {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : Data U} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (t : ↑(Set.Icc 0 D.T)) (x : EulerLiftedGradientSpace.LiftDomain P) : EulerSmoothLimit.Space

Force field: an abbreviation for pointField P (forcingPath G) G.path_orbit t.

Equations

• EulerTransversePacketProvider.HistoryData.forceField G t = EulerCylinderSmoothOrbit.pointField P (EulerTransversePacketProvider.HistoryData.forcingPath G) ⋯ t

noncomputable def EulerTransversePacketProvider.HistoryData.normalResidual {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) : ℝ

Normal residual, given by (⟪D.normal.field t x.1,forceField G t x⟫_ℝ - 2*⟪D.normal.field t x.1,D.M.field t x.1 (B.field G t x)⟫_ℝ)/‖D.normal.field t x.1‖^2.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def EulerTransversePacketProvider.HistoryData.residualPath {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) : C(↑(Set.Icc 0 D.T), ↥(EulerLpCylinderTranslation.CylinderL2 P ℝ))

Residual path, given by sourceResidual P D.M D.normal D.normalLower D.normalLower_pos D.normal_lower (forcingPath G) (B.velocityPath G).

Equations

• B.residualPath G = EulerSourceNormalResidualBounds.sourceResidual P D.M D.normal D.normalLower ⋯ ⋯ (EulerTransversePacketProvider.HistoryData.forcingPath G) (B.velocityPath G)

theorem EulerTransversePacketProvider.HistoryData.residualPath_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.residualPath G)

theorem EulerTransversePacketProvider.HistoryData.residualPath_slice_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)) : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) ((B.residualPath G) t)

theorem EulerTransversePacketProvider.HistoryData.residualPath_average_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)) : (EulerCylinderAngleAverage.average P) ((B.residualPath G) t) = 0

theorem EulerTransversePacketProvider.HistoryData.normalResidual_continuous {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)) : Continuous (B.normalResidual G t)

theorem EulerTransversePacketProvider.HistoryData.normalResidual_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.normalResidual G t) x)

theorem EulerTransversePacketProvider.HistoryData.residualPath_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.residualPath G) t) =ᵐ[EulerLiftedGradientSpace.liftMeasure P] B.normalResidual G t

The actual scalar L² source equals the literal normal quotient.

theorem EulerTransversePacketProvider.HistoryData.normalResidual_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)) (y : EulerSmoothLimit.Space) : ∫ (θ : ℝ) in 0..P, B.normalResidual G t (y, ↑θ) = 0

noncomputable def EulerTransversePacketProvider.HistoryData.pressureField {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)) : EulerLiftedGradientSpace.LiftDomain P → ℝ

The actual mean-zero periodic angular integral.

Equations

• B.pressureField G t = EulerCylinderScalarPrimitive.classicalPrimitive P (B.normalResidual G t) ⋯ ⋯

theorem EulerTransversePacketProvider.HistoryData.pressureField_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.pressurePath G) t) =ᵐ[EulerLiftedGradientSpace.liftMeasure P] B.pressureField G t

theorem EulerTransversePacketProvider.HistoryData.pressureField_angle {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)) (y : EulerSmoothLimit.Space) (θ : ℝ) : HasDerivAt (fun (s : ℝ) => B.pressureField G t (y, ↑s)) (B.normalResidual G t (y, ↑θ)) θ

theorem EulerTransversePacketProvider.HistoryData.pressureField_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)) (y : EulerSmoothLimit.Space) : ∫ (θ : ℝ) in 0..P, B.pressureField G t (y, ↑θ) = 0

theorem EulerTransversePacketProvider.HistoryData.pressureField_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.pressureField G t) x)

theorem EulerTransversePacketProvider.HistoryData.pressureField_eq_scalarPointField {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.pressureField G t = EulerCylinderScalarPrimitive.scalarPointField P (B.pressurePath G) ⋯ t

theorem EulerTransversePacketProvider.HistoryData.normalResidual_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)) (y : EulerSmoothLimit.Space) (hy : y ∉ D.support) (θ : AddCircle P) : B.normalResidual G t (y, θ) = 0

theorem EulerTransversePacketProvider.HistoryData.pressureField_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)) (y : EulerSmoothLimit.Space) (hy : y ∉ D.support) (θ : AddCircle P) : B.pressureField G t (y, θ) = 0

theorem EulerTransversePacketProvider.HistoryData.field_balance {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) : B.derivativeField G t x + ((D.M.field t) x.1) (B.field G t x) + B.normalResidual G t x • (D.normal.field t) x.1 = forceField G t x

Equation (11) before taking the angular integral, valid at every point.

theorem EulerTransversePacketProvider.HistoryData.field_pressure_equation {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)) (y : EulerSmoothLimit.Space) (θ : ℝ) : B.derivativeField G t (y, ↑θ) + ((D.M.field t) y) (B.field G t (y, ↑θ)) + deriv (fun (s : ℝ) => B.pressureField G t (y, ↑s)) θ • (D.normal.field t) y = raw (↑t, y, θ)

The constructed history and its literal normalized pressure solve (11).