circleAverage_log_norm_sub_const_eq_posLog

English

The circle average of log ‖· − a‖ equals the positive part of the logarithm of ‖a‖: circleAverage(log ‖· − a‖) 0 1 = log⁺ ‖a‖.

Русский

Круговое среднее log ‖z − a‖ равно положительной части логарифма ‖a‖: circleAverage(log ‖· − a‖) 0 1 = log⁺ ‖a‖.

LaTeX

$$$$circleAverage(\log \|\cdot - a\|)\,0\,1 = \log^+ \|a\|.$$$$

Lean4

/-- The `circleAverage (log ‖· - a‖) 0 1` equals `log⁺ ‖a‖`.
-/
@[simp]
theorem circleAverage_log_norm_sub_const_eq_posLog : circleAverage (log ‖· - a‖) 0 1 = log⁺ ‖a‖ :=
  by
  rcases lt_trichotomy 1 ‖a‖ with h | h | h
  · rw [circleAverage_log_norm_sub_const₂ h]
    apply (posLog_eq_log _).symm
    simp_all [le_of_lt h]
  · rw [eq_comm, circleAverage_log_norm_sub_const₁ h.symm, posLog_eq_zero_iff]
    simp_all
  · rw [eq_comm, circleAverage_log_norm_sub_const₀ h, posLog_eq_zero_iff]
    simp_all [le_of_lt h]

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