y_eq_one_of_mem_closedBall — Mathlib

English

If x lies outside the ball of radius 1+D, then y(D,x)=0.

Русский

Если x лежит вне шарa радиуса 1+D, то y(D,x)=0.

LaTeX

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

Lean4

theorem y_eq_one_of_mem_closedBall {D : ℝ} {x : E} (Dpos : 0 < D) (hx : x ∈ closedBall (0 : E) (1 - D)) : y D x = 1 :=
  by
  change (w D ⋆[lsmul ℝ ℝ, μ] φ) x = 1
  have B : ∀ y : E, y ∈ ball x D → φ y = 1 :=
    by
    have C : ball x D ⊆ ball 0 1 := by
      apply ball_subset_ball'
      simp only [mem_closedBall] at hx
      linarith only [hx]
    intro y hy
    simp only [φ, indicator, mem_closedBall, ite_eq_left_iff, not_le, zero_ne_one]
    intro h'y
    linarith only [mem_ball.1 (C hy), h'y]
  have Bx : φ x = 1 := B _ (mem_ball_self Dpos)
  have B' : ∀ y, y ∈ ball x D → φ y = φ x := by rw [Bx]; exact B
  rw [convolution_eq_right' _ (le_of_eq (w_support E Dpos)) B']
  simp only [lsmul_apply, Algebra.id.smul_eq_mul, integral_mul_const, w_integral E Dpos, Bx, one_mul]

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