English
For all x and D>0, if the base parameters are satisfied, then y(D,x) ≤ 1.
Русский
Для всех x и D>0 выполняется y(D,x) ≤ 1.
LaTeX
$$y(D,x) ≤ 1$$
Lean4
theorem y_pos_of_mem_ball {D : ℝ} {x : E} (Dpos : 0 < D) (D_lt_one : D < 1) (hx : x ∈ ball (0 : E) (1 + D)) :
0 < y D x := by
simp only [mem_ball_zero_iff] at hx
refine (integral_pos_iff_support_of_nonneg (w_mul_φ_nonneg D x) ?_).2 ?_
· have F_comp : HasCompactSupport (w D) := w_compact_support E Dpos
have B : LocallyIntegrable (φ : E → ℝ) μ := (locallyIntegrable_const _).indicator measurableSet_closedBall
have C : Continuous (w D : E → ℝ) := continuous_const.mul ((u_continuous E).comp (continuous_id.const_smul _))
exact (F_comp.convolutionExists_left (lsmul ℝ ℝ : ℝ →L[ℝ] ℝ →L[ℝ] ℝ) C B x).integrable
· set z := (D / (1 + D)) • x with hz
have B : 0 < 1 + D := by linarith
have C : ball z (D * (1 + D - ‖x‖) / (1 + D)) ⊆ support fun y : E => w D y * φ (x - y) :=
by
intro y hy
simp only [support_mul, w_support E Dpos]
simp only [φ, mem_inter_iff, mem_support, Ne, indicator_apply_eq_zero, mem_closedBall_zero_iff, one_ne_zero,
not_forall, not_false_iff, exists_prop, and_true]
constructor
· apply ball_subset_ball' _ hy
simp only [hz, norm_smul, abs_of_nonneg Dpos.le, abs_of_nonneg B.le, dist_zero_right, Real.norm_eq_abs, abs_div]
field_simp
linarith only
· have ID : ‖D / (1 + D) - 1‖ = 1 / (1 + D) :=
by
rw [Real.norm_of_nonpos]
· simp [field]
· field_simp
linarith only
rw [← mem_closedBall_iff_norm']
apply closedBall_subset_closedBall' _ (ball_subset_closedBall hy)
rw [← one_smul ℝ x, dist_eq_norm, hz, ← sub_smul, one_smul, norm_smul, ID]
field_simp
nlinarith only [hx, D_lt_one]
apply lt_of_lt_of_le _ (measure_mono C)
apply measure_ball_pos
exact div_pos (mul_pos Dpos (by linarith only [hx])) B
