circleAverage_congr_sphere — Mathlib

English

If f1 and f2 agree on the circle, their circle averages coincide.

Русский

Если f1 и f2 совпадают на окружности, их окружные средние совпадают.

LaTeX

$$$circleAverage\ f_1\ c\ R = circleAverage\ f_2\ c\ R \quad\text{whenever } f_1=f_2\text{ on }\operatorname{sphere}(c,|R|)$$$

Lean4

/-- If two functions agree on the circle, then their circle averages agree. -/
theorem circleAverage_congr_sphere {f₁ f₂ : ℂ → E} (hf : Set.EqOn f₁ f₂ (sphere c |R|)) :
    circleAverage f₁ c R = circleAverage f₂ c R :=
  by
  unfold circleAverage
  congr 1
  exact intervalIntegral.integral_congr (fun x ↦ by simp [hf (circleMap_mem_sphere' c R x)])

Похожие утверждения