English
For real-valued f on the circle, the absolute value of the circle average is bounded by the circle average of the absolute value: |circleAverage f c R| ≤ circleAverage |f| c R.
Русский
Для вещественной функции на окружности модуль усреднения не больше среднего модуля: |circleAverage f c R| ≤ circleAverage |f| c R.
LaTeX
$$$|circleAverage\ f\ c\ R| \leq circleAverage\ |f|\ c\ R$$$
Lean4
/-- Analogue of `intervalIntegral.abs_integral_le_integral_abs`: The absolute value of a circle average
is less than or equal to the circle average of the absolute value of the function.
-/
theorem abs_circleAverage_le_circleAverage_abs {f : ℂ → ℝ} : |circleAverage f c R| ≤ circleAverage |f| c R :=
by
rw [circleAverage, circleAverage, smul_eq_mul, smul_eq_mul, abs_mul, abs_of_pos (inv_pos.2 two_pi_pos),
mul_le_mul_iff_of_pos_left (inv_pos.2 two_pi_pos)]
exact intervalIntegral.abs_integral_le_integral_abs (le_of_lt two_pi_pos)
