English
The circle average over the unit circle is invariant under z ↦ z^{-1}.
Русский
Среднее по единичной окружности не изменяется при замене z на z^{-1}.
LaTeX
$$$circleAverage\ (f\cdot^{-1})\ 0\ 1 = circleAverage\ f\ 0\ 1$$$
Lean4
/-- The circle average of a function `f` on the unit sphere equals the circle average of the function
`z ↦ f z⁻¹`.
-/
@[simp]
theorem circleAverage_zero_one_congr_inv {f : ℂ → E} : circleAverage (f ·⁻¹) 0 1 = circleAverage f 0 1 :=
by
unfold circleAverage
congr 1
calc
∫ θ in 0..2 * π, f (circleMap 0 1 θ)⁻¹
_ = ∫ θ in 0..2 * π, f (circleMap 0 1 (-θ)) := by simp [circleMap_zero_inv]
_ = ∫ θ in 0..2 * π, f (circleMap 0 1 θ) :=
by
rw [intervalIntegral.integral_comp_neg (fun w ↦ f (circleMap 0 1 w))]
have t₀ : Function.Periodic (fun w ↦ f (circleMap 0 1 w)) (2 * π) := fun x ↦ by simp [periodic_circleMap 0 1 x]
simpa using (t₀.intervalIntegral_add_eq_of_pos two_pi_pos (-(2 * π)) 0)
