circleAverage_zero — Mathlib

English

If the radius is zero, the circleAverage reduces to the center value: circleAverage f c 0 = f(c).

Русский

Если радиус нулевой, то среднее по окружности равно значению функции в центре: circleAverage f c 0 = f(c).

LaTeX

$$$circleAverage\ f\ c\ 0 = f(c)$$$

Lean4

/-- Interval averages for zero radii equal values at the center point. -/
@[simp]
theorem circleAverage_zero [CompleteSpace E] : circleAverage f c 0 = f c :=
  by
  rw [circleAverage]
  simp only [circleMap_zero_radius, Function.const_apply, intervalIntegral.integral_const, sub_zero, ← smul_assoc,
    smul_eq_mul, inv_mul_cancel₀ (mul_ne_zero two_ne_zero pi_ne_zero), one_smul]

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