English
Circle averages do not change when the integration angle is shifted: circleAverage f c R equals the average of f(circleMap(c,R,(θ+η))).
Русский
Среднее по окружности не меняется при смещении угла интегрирования: circleAverage f c R = среднее от f(circleMap(c,R,(θ+η))).
LaTeX
$$$circleAverage\ f\ c\ R = \frac{1}{2\pi}\int_{0}^{2\pi} f(circleMap\ c\ R\ (\theta+\eta))\,d\theta$$$
Lean4
/-- Circle averages do not change when shifting the angle. -/
theorem circleAverage_eq_integral_add (η : ℝ) :
circleAverage f c R = (2 * π)⁻¹ • ∫ θ in 0..2 * π, f (circleMap c R (θ + η)) :=
by
rw [intervalIntegral.integral_comp_add_right (fun θ ↦ f (circleMap c R θ))]
have t₀ : (fun θ ↦ f (circleMap c R θ)).Periodic (2 * π) := fun x ↦ by simp [periodic_circleMap c R x]
have := t₀.intervalIntegral_add_eq 0 η
rw [zero_add, add_comm] at this
rw [zero_add]
simp only [circleAverage, mul_inv_rev]
congr
