y_neg — Mathlib

English

For D>0, D<1, and x in the closed ball of radius 1−D about 0, y(D,x)=1.

Русский

При D>0, D<1 и x в замкнутом шаре радиуса 1−D вокруг 0, имеет место y(D,x)=1.

LaTeX

$$y(D,x)=1$$

Lean4

theorem y_neg (D : ℝ) (x : E) : y D (-x) = y D x :=
  by
  apply convolution_neg_of_neg_eq
  · filter_upwards with x
    simp only [w_def, mul_inv_rev, smul_neg, u_neg, smul_eq_mul]
  · filter_upwards with x
    simp only [φ, indicator, mem_closedBall, dist_zero_right, norm_neg]

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