The actual angular primitive is jointly smooth in spatial labels and angle.

theorem EulerAngleMeanZeroPrimitive.rawPrimitive_fixed_interval {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : ℝ → E) (θ : ℝ) : rawPrimitive f θ = θ • ∫ (s : ℝ) in 0..1, f (θ * s)

theorem EulerAngleMeanZeroPrimitive.rawPrimitive_joint_contDiff {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {X : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] [ProperSpace X] (F : X × ℝ → E) (hF : ContDiff ℝ (↑⊤) F) : ContDiff ℝ ↑⊤ fun (p : X × ℝ) => rawPrimitive (fun (θ : ℝ) => F (p.1, θ)) p.2

theorem EulerAngleMeanZeroPrimitive.primitive_joint_contDiff {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {X : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] [ProperSpace X] (P : ℝ) (hP : 0 ≤ P) (F : X × ℝ → E) (hF : ContDiff ℝ (↑⊤) F) : ContDiff ℝ ↑⊤ fun (p : X × ℝ) => primitive P (fun (θ : ℝ) => F (p.1, θ)) p.2

theorem EulerAngleMeanZeroPrimitive.rawPrimitive_joint_continuous {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {Y : Type u_1} [TopologicalSpace Y] [FirstCountableTopology Y] [LocallyCompactSpace Y] (F : Y × ℝ → E) (hF : Continuous F) : Continuous fun (p : Y × ℝ) => rawPrimitive (fun (θ : ℝ) => F (p.1, θ)) p.2

theorem EulerAngleMeanZeroPrimitive.primitive_joint_continuous {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {Y : Type u_1} [TopologicalSpace Y] [FirstCountableTopology Y] [LocallyCompactSpace Y] (P : ℝ) (hP : 0 ≤ P) (F : Y × ℝ → E) (hF : Continuous F) : Continuous fun (p : Y × ℝ) => primitive P (fun (θ : ℝ) => F (p.1, θ)) p.2