The literal raw-field corrector operator used by the recursive packet definition.

Zero angular mean of the actual transverse potential, corrector, and time derivatives.

theorem EulerTransversePacketProvider.Forcing.fullVelocityPath_average_zero {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (I : InitialData P D) : (EulerCylinderAngleAverage.pathAverage P) (G.fullVelocityPath I) = 0

theorem EulerTransversePacketProvider.Forcing.fullDerivativePath_average_zero {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (I : InitialData P D) : (EulerCylinderAngleAverage.pathAverage P) (G.fullDerivativePath I) = 0

theorem EulerTransversePacketProvider.Forcing.potentialPath_average_zero {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (I : InitialData P D) : (EulerCylinderAngleAverage.pathAverage P) (G.potentialPath I) = 0

theorem EulerTransversePacketProvider.Forcing.potentialTimePath_average_zero {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (I : InitialData P D) : (EulerCylinderAngleAverage.pathAverage P) (G.potentialTimePath I) = 0

theorem EulerTransversePacketProvider.Forcing.correctorPath_average_zero {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (I : InitialData P D) : (EulerCylinderAngleAverage.pathAverage P) (G.correctorPath I) = 0

theorem EulerTransversePacketProvider.Forcing.correctorTimePath_average_zero {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (I : InitialData P D) : (EulerCylinderAngleAverage.pathAverage P) (G.correctorTimePath I) = 0

theorem EulerTransversePacketProvider.Forcing.corrector_mean_zero {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (I : InitialData P D) (t : ℝ) (x : EulerSmoothLimit.Space) : ∫ (θ : ℝ) in 0..P, G.corrector I (t, x, θ) = 0

theorem EulerTransversePacketProvider.Forcing.correctorDerivative_mean_zero {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (I : InitialData P D) (t : ℝ) (x : EulerSmoothLimit.Space) : ∫ (θ : ℝ) in 0..P, G.correctorDerivative I (t, x, θ) = 0

noncomputable def EulerTransversePacketProvider.Data.rawPotential {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) (P : ℝ) (A : EulerPacketProfileRecursion.VectorField) : EulerPacketProfileRecursion.VectorField

The specified mean-zero angular primitive, applied directly to a raw field.

Equations

• D.rawPotential P A z = EulerPacketAngularPotential.potential P ((D.normal.field (D.clamp z.1)) z.2.1) (fun (θ : ℝ) => A (z.1, z.2.1, θ)) z.2.2

noncomputable def EulerTransversePacketProvider.Data.curlCorrector {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) (P : ℝ) (A : EulerPacketProfileRecursion.VectorField) : EulerPacketProfileRecursion.VectorField

The actual slow curl in deformation coordinates; this defines a total raw-field operator.

Equations

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

theorem EulerTransversePacketProvider.Forcing.rawPotential_eq {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (I : InitialData P D) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : D.rawPotential P (G.vector I) (↑t, x, θ) = EulerCylinderSmoothOrbit.pointField P (G.potentialPath I) ⋯ t (x, ↑θ)

theorem EulerTransversePacketProvider.Forcing.curlCorrector_eq {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (I : InitialData P D) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : D.curlCorrector P (G.vector I) (↑t, x, θ) = G.corrector I (↑t, x, θ)

noncomputable def EulerTransversePacketProvider.Forcing.curlCorrectorField {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (I : InitialData P D) : EulerPacketCylinderField.Field P D.T (D.curlCorrector P (G.vector I))

The literal recursion operator has the already-constructed continuous L² witness.

Equations

• G.curlCorrectorField I = { path := G.correctorPath I, orbit := ⋯, raw_eq := ⋯ }

theorem EulerTransversePacketProvider.Forcing.curlCorrectorField_time {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (I : InitialData P D) : EulerPacketCylinderField.TimeDerivative ⋯ (G.curlCorrectorField I) (G.correctorDerivativeField I)

theorem EulerTransversePacketProvider.Forcing.curlCorrector_mean_zero {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (I : InitialData P D) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) : ∫ (θ : ℝ) in 0..P, D.curlCorrector P (G.vector I) (↑t, x, θ) = 0