The mean of a genuine derivative of a periodic field is zero.

theorem EulerPeriodicDerivativeMean.integral_derivative_eq_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (P : ℝ) (f f' : ℝ → E) (hf : ∀ (θ : ℝ), HasDerivAt f (f' θ) θ) (hf' : Continuous f') (hper : Function.Periodic f P) : ∫ (θ : ℝ) in 0..P, f' θ = 0

theorem EulerPeriodicDerivativeMean.integral_constant_smul_derivative_eq_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (P c : ℝ) (f f' : ℝ → E) (hf : ∀ (θ : ℝ), HasDerivAt f (f' θ) θ) (hf' : Continuous f') (hper : Function.Periodic f P) : ∫ (θ : ℝ) in 0..P, c • f' θ = 0

A coefficient independent of angle cannot change this zero-mean conclusion.