The literal periodic scalar pressure primitive, with actual smoothness and normalization.

theorem EulerCylinderScalarPrimitive.scalarAngle_periodic (P : ℝ) (f : EulerLiftedGradientSpace.LiftDomain P → ℝ) (y : EulerSmoothLimit.Space) : Function.Periodic (fun (s : ℝ) => f (y, ↑s)) P

noncomputable def EulerCylinderScalarPrimitive.classicalPrimitive (P : ℝ) (f : EulerLiftedGradientSpace.LiftDomain P → ℝ) (hf : Continuous f) (hmean : ∀ (y : EulerLiftedGradientSpace.Vector3), ∫ (s : ℝ) in 0..P, f (y, ↑s) = 0) (x : EulerLiftedGradientSpace.LiftDomain P) : ℝ

The normalized integral descended to the actual periodic cylinder.

Equations

• EulerCylinderScalarPrimitive.classicalPrimitive P f hf hmean x = ⋯.lift x.2

theorem EulerCylinderScalarPrimitive.classicalPrimitive_cover (P : ℝ) (f : EulerLiftedGradientSpace.LiftDomain P → ℝ) (hf : Continuous f) (hmean : ∀ (y : EulerLiftedGradientSpace.Vector3), ∫ (s : ℝ) in 0..P, f (y, ↑s) = 0) (y : EulerSmoothLimit.Space) (θ : ℝ) : classicalPrimitive P f hf hmean (y, ↑θ) = EulerAngleMeanZeroPrimitive.primitive P (fun (s : ℝ) => f (y, ↑s)) θ

theorem EulerCylinderScalarPrimitive.classicalPrimitive_angle (P : ℝ) (f : EulerLiftedGradientSpace.LiftDomain P → ℝ) (hf : Continuous f) (hmean : ∀ (y : EulerLiftedGradientSpace.Vector3), ∫ (s : ℝ) in 0..P, f (y, ↑s) = 0) (y : EulerSmoothLimit.Space) (θ : ℝ) : HasDerivAt (fun (s : ℝ) => classicalPrimitive P f hf hmean (y, ↑s)) (f (y, ↑θ)) θ

The literal angular derivative is the original scalar field.

theorem EulerCylinderScalarPrimitive.classicalPrimitive_mean_zero (P : ℝ) [Fact (0 < P)] (f : EulerLiftedGradientSpace.LiftDomain P → ℝ) (hf : Continuous f) (hmean : ∀ (y : EulerLiftedGradientSpace.Vector3), ∫ (s : ℝ) in 0..P, f (y, ↑s) = 0) (y : EulerSmoothLimit.Space) : ∫ (θ : ℝ) in 0..P, classicalPrimitive P f hf hmean (y, ↑θ) = 0

theorem EulerCylinderScalarPrimitive.classicalPrimitive_smooth (P : ℝ) [Fact (0 < P)] (f : EulerLiftedGradientSpace.LiftDomain P → ℝ) (hf : Continuous f) (hmean : ∀ (y : EulerLiftedGradientSpace.Vector3), ∫ (s : ℝ) in 0..P, f (y, ↑s) = 0) (hfs : ∀ (x : EulerLiftedGradientSpace.LiftDomain P), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P f x)) (x : EulerLiftedGradientSpace.LiftDomain P) : ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P (classicalPrimitive P f hf hmean) x)

The actual normalized integral is smooth in all cylinder variables.

theorem EulerCylinderScalarPrimitive.classicalPrimitive_continuous (P : ℝ) [Fact (0 < P)] (f : EulerLiftedGradientSpace.LiftDomain P → ℝ) (hf : Continuous f) (hmean : ∀ (y : EulerLiftedGradientSpace.Vector3), ∫ (s : ℝ) in 0..P, f (y, ↑s) = 0) (hfs : ∀ (x : EulerLiftedGradientSpace.LiftDomain P), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P f x)) : Continuous (classicalPrimitive P f hf hmean)

theorem EulerCylinderScalarPrimitive.classicalPrimitive_zero (P : ℝ) (f : EulerLiftedGradientSpace.LiftDomain P → ℝ) (hf : Continuous f) (hmean : ∀ (y : EulerLiftedGradientSpace.Vector3), ∫ (s : ℝ) in 0..P, f (y, ↑s) = 0) (y : EulerSmoothLimit.Space) (hy : ∀ (θ : AddCircle P), f (y, θ) = 0) (θ : AddCircle P) : classicalPrimitive P f hf hmean (y, θ) = 0

Angular integration does not spread spatial support.