circleAverage_log_norm_add_const_eq_posLog

English

The circle average equals log⁺ ‖a‖ for all a, with the three cases collapsing to the same formula: circleAverage(log ‖· − a‖) 0 1 = log⁺ ‖a‖.

Русский

Круговое среднее равно log⁺ ‖a‖ для любого a; три случая сводятся к одной формуле: circleAverage(log ‖z − 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_add_const_eq_posLog : circleAverage (log ‖· + a‖) 0 1 = log⁺ ‖a‖ :=
  by
  have : (log ‖· + a‖) = (log ‖· - -a‖) := by simp
  simp [this]

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