English
Same as the previous, under the appropriate hypotheses, the convolution value at x0 equals the integral against g(x0).
Русский
Аналогично предыдущему утверждению под подходящими условиями, значение свертки в точке x0 равно интегралу по g(x0).
LaTeX
$$(hf : support f ⊆ ball 0 R) ∧ (hg : ∀ x ∈ ball x0 R, g x = g x0) → (f ⋆[L, μ] g) x0 = ∫ t, L (f t) (g x0) ∂μ$$
Lean4
/-- Compute `(f ⋆ g) x₀` if the support of the `f` is within `Metric.ball 0 R`, and `g` is constant
on `Metric.ball x₀ R`.
We can simplify the RHS further if we assume `f` is integrable, but also if `L = (•)` or more
generally if `L` has an `AntilipschitzWith`-condition. -/
theorem convolution_eq_right' {x₀ : G} {R : ℝ} (hf : support f ⊆ ball (0 : G) R) (hg : ∀ x ∈ ball x₀ R, g x = g x₀) :
(f ⋆[L, μ] g) x₀ = ∫ t, L (f t) (g x₀) ∂μ :=
by
have h2 : ∀ t, L (f t) (g (x₀ - t)) = L (f t) (g x₀) := fun t ↦
by
by_cases ht : t ∈ support f
· have h2t := hf ht
rw [mem_ball_zero_iff] at h2t
specialize hg (x₀ - t)
rw [sub_eq_add_neg, add_mem_ball_iff_norm, norm_neg, ← sub_eq_add_neg] at hg
rw [hg h2t]
· rw [notMem_support] at ht
simp_rw [ht, L.map_zero₂]
simp_rw [convolution_def, h2]
