Bounded linear maps commute with the literal normalized angular integral.

theorem EulerAngleMeanZeroPrimitive.rawPrimitive_map {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] (L : E →L[ℝ] F) (f : ℝ → E) (hf : Continuous f) (θ : ℝ) : L (rawPrimitive f θ) = rawPrimitive (fun (s : ℝ) => L (f s)) θ

theorem EulerAngleMeanZeroPrimitive.primitive_map {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] (L : E →L[ℝ] F) (P : ℝ) (f : ℝ → E) (hf : Continuous f) (θ : ℝ) : L (primitive P f θ) = primitive P (fun (s : ℝ) => L (f s)) θ