circleAverage_log_norm_sub_const_of_mem_closedBall

English

If u lies in the closed ball with center c and radius R, then circleAverage(log ‖· − u‖) c R = log R.

Русский

Если u лежит в замкнутой окружности с центром в c и радиусом R, то circleAverage(log ‖· − u‖) c R = log R.

LaTeX

$$$$u\in \overline{B}(c,|R|) \implies circleAverage(\log \|\cdot - u\|)\, c\, R = \log R.$$$$

Lean4

/-- Trivial corollary of
`circleAverage_log_norm_sub_const_eq_log_radius_add_posLog`: If `u : ℂ` lies within the closed ball
with center `c` and radius `R`, then the circle average
`circleAverage (log ‖· - u‖) c R` equals `log R`.
-/
theorem circleAverage_log_norm_sub_const_of_mem_closedBall (hu : a ∈ closedBall c |R|) :
    circleAverage (log ‖· - a‖) c R = log R := by
  by_cases hR : R = 0
  · simp_all
  rw [circleAverage_log_norm_sub_const_eq_log_radius_add_posLog hR, add_eq_left, posLog_eq_zero_iff, abs_mul, abs_inv,
    abs_of_nonneg (norm_nonneg (c - a))]
  rw [mem_closedBall, dist_eq_norm'] at hu
  apply inv_mul_le_one_of_le₀ hu (abs_nonneg R)

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