The genuine cylinder L² angular operator represents the literal classical primitive.

A translation-kernel formula for the literal normalized periodic primitive.

theorem EulerAngleMeanZeroPrimitive.primitive_eq_translation_kernel {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (P : ℝ) (hP : P ≠ 0) (f : ℝ → E) (hf : Continuous f) (hper : Function.Periodic f P) (hmean : ∫ (s : ℝ) in 0..P, f s = 0) (θ : ℝ) : primitive P f θ = P⁻¹ • ∫ (s : ℝ) in 0..P, s • f (θ + s)

This formula realizes the angular primitive as an integral of translations.

theorem EulerCylinderAnglePrimitive.sobolevKernel_continuous (P : ℝ) [Fact (0 < P)] {q : ℕ} (u : ↥(EulerCylinderSobolevSpace.SobolevSpace P q)) : Continuous fun (s : ℝ) => s • (EulerCylinderSobolevSpace.sobolevTranslation P q (angleShift P s)) u

theorem EulerCylinderAnglePrimitive.sobolevPrimitive_eq_integral (P : ℝ) [Fact (0 < P)] {q : ℕ} (u : ↥(EulerCylinderSobolevSpace.SobolevSpace P q)) : (sobolevPrimitive P q) u = P⁻¹ • ∫ (s : ℝ) in 0..P, s • (EulerCylinderSobolevSpace.sobolevTranslation P q (angleShift P s)) u

The lifted operator is also the actual Bochner integral in the Sobolev space.

theorem EulerCylinderAnglePrimitive.pointEvaluation_translation (P : ℝ) [Fact (0 < P)] (u : ↥(EulerCylinderSobolevSpace.SobolevSpace P 3)) (a x : EulerLiftedGradientSpace.LiftDomain P) : (EulerSobolevPointEvaluation.pointEvaluation P x) ((EulerCylinderSobolevSpace.sobolevTranslation P 3 a) u) = EulerSobolevPointEvaluation.representative P u (x + a)

theorem EulerCylinderAnglePrimitive.pointEvaluation_primitive_kernel (P : ℝ) [Fact (0 < P)] (u : ↥(EulerCylinderSobolevSpace.SobolevSpace P 3)) (x : EulerLiftedGradientSpace.LiftDomain P) : (EulerSobolevPointEvaluation.pointEvaluation P x) ((sobolevPrimitive P 3) u) = P⁻¹ • ∫ (s : ℝ) in 0..P, s • EulerSobolevPointEvaluation.representative P u (x + angleShift P s)

theorem EulerCylinderAnglePrimitive.pointEvaluation_primitive_classical (P : ℝ) [Fact (0 < P)] (u : ↥(EulerCylinderSobolevSpace.SobolevSpace P 3)) (f : EulerLiftedGradientSpace.LiftDomain P → EulerLiftedGradientSpace.Vector3) (hf : Continuous f) (hrep : ↑↑(EulerCylinderSobolevSpace.value P u) =ᵐ[EulerLiftedGradientSpace.liftMeasure P] f) (hmean : ∀ (y : EulerLiftedGradientSpace.Vector3), ∫ (s : ℝ) in 0..P, f (y, ↑s) = 0) (y : EulerLiftedGradientSpace.Vector3) (θ : ℝ) : (EulerSobolevPointEvaluation.pointEvaluation P (y, ↑θ)) ((sobolevPrimitive P 3) u) = EulerAngleMeanZeroPrimitive.primitive P (fun (s : ℝ) => f (y, ↑s)) θ

Evaluation of the constructed L² operator gives the actual normalized integral.

theorem EulerCylinderAnglePrimitive.primitive_ae_classical (P : ℝ) [Fact (0 < P)] (u : ↥(EulerCylinderSobolevSpace.SobolevSpace P 3)) (f q : EulerLiftedGradientSpace.LiftDomain P → EulerLiftedGradientSpace.Vector3) (hf : Continuous f) (hrep : ↑↑(EulerCylinderSobolevSpace.value P u) =ᵐ[EulerLiftedGradientSpace.liftMeasure P] f) (hmean : ∀ (y : EulerLiftedGradientSpace.Vector3), ∫ (s : ℝ) in 0..P, f (y, ↑s) = 0) (hq : ∀ (y : EulerLiftedGradientSpace.Vector3) (θ : ℝ), q (y, ↑θ) = EulerAngleMeanZeroPrimitive.primitive P (fun (s : ℝ) => f (y, ↑s)) θ) : ↑↑((primitive P) (EulerCylinderSobolevSpace.value P u)) =ᵐ[EulerLiftedGradientSpace.liftMeasure P] q

Classical identification holds as equality of actual L² representatives.