English
A continuous linear map L commutes with circleAverage: circleAverage(L ∘ f) c R = L(circleAverage f c R).
Русский
Постоянно непрерывное линейное отображение L commute со средним по окружности: circleAverage(L ∘ f) c R = L(circleAverage f c R).
LaTeX
$$$circleAverage\ (L \circ f)\ c\ R = L\big(circleAverage\ f\ c\ R\big)$$$
Lean4
/-- If `f x` is smaller than `a` on for every point of the circle, then the circle average of `f` is
smaller than `a`.
-/
theorem circleAverage_mono_on_of_le_circle {f : ℂ → ℝ} {a : ℝ} (hf : CircleIntegrable f c R)
(h₂f : ∀ x ∈ Metric.sphere c |R|, f x ≤ a) : circleAverage f c R ≤ a :=
by
rw [← circleAverage_const a c |R|, circleAverage, circleAverage, smul_eq_mul, smul_eq_mul,
mul_le_mul_iff_of_pos_left (inv_pos.2 two_pi_pos)]
exact
intervalIntegral.integral_mono_on_of_le_Ioo (le_of_lt two_pi_pos) hf intervalIntegrable_const
(fun θ _ ↦ h₂f (circleMap c R θ) (circleMap_mem_sphere' c R θ))
