circleAverage_abs_radius — Mathlib

English

Replacing radius by its absolute value does not change the circle average: circleAverage f c |R| = circleAverage f c R.

Русский

Заменяя радиус на его модуль, получаем то же самое среднее: circleAverage f c |R| = circleAverage f c R.

LaTeX

$$$circleAverage\ f\ c\ |R| = circleAverage\ f\ c\ R$$$

Lean4

/-- Circle averages do not change when replacing the radius by its absolute value. -/
@[simp]
theorem circleAverage_abs_radius : circleAverage f c |R| = circleAverage f c R :=
  by
  by_cases hR : 0 ≤ R
  · rw [abs_of_nonneg hR]
  · rw [abs_of_neg (not_le.1 hR), circleAverage_neg_radius]

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