English
Let f be locally integrable and let g depend on a parameter p in a subset s of a parameter space P, with a fixed compact support k in G and with g_p continuous on s × univ and vanishing outside k. Then the map (p, x) ↦ (f ⋆ g_p)(x) is continuous on s × univ.
Русский
Пусть f локально интегрируема, а g зависит от параметра p в подмножестве s пространства параметров P, опора функций g_p ограничена в фиксированном компакте k; при этом g_p непрерывна по p на s × univ и обращена в ноль вне k. Тогда отображение (p, x) ↦ (f ⋆ g_p)(x) непрерывно на s × univ.
LaTeX
$$$\text{IsCompact}(k) \implies \text{ContinuousOn} (\lambda (p,x) . (f ⋆[L, μ] g p) x) (s \times univ).$$$
Lean4
/-- The convolution `f * g` is continuous if `f` is locally integrable and `g` is continuous and
compactly supported. Version where `g` depends on an additional parameter in a subset `s` of
a parameter space `P` (and the compact support `k` is independent of the parameter in `s`). -/
theorem continuousOn_convolution_right_with_param {g : P → G → E'} {s : Set P} {k : Set G} (hk : IsCompact k)
(hgs : ∀ p, ∀ x, p ∈ s → x ∉ k → g p x = 0) (hf : LocallyIntegrable f μ) (hg : ContinuousOn ↿g (s ×ˢ univ)) :
ContinuousOn (fun q : P × G => (f ⋆[L, μ] g q.1) q.2) (s ×ˢ univ) := by
/- First get rid of the case where the space is not locally compact. Then `g` vanishes everywhere
and the conclusion is trivial. -/
by_cases H : ∀ p ∈ s, ∀ x, g p x = 0
· apply (continuousOn_const (c := 0)).congr
rintro ⟨p, x⟩ ⟨hp, -⟩
apply integral_eq_zero_of_ae (Eventually.of_forall (fun y ↦ ?_))
simp [H p hp _]
have : LocallyCompactSpace G := by
push_neg at H
rcases H with ⟨p, hp, x, hx⟩
have A : support (g p) ⊆ k := support_subset_iff'.2 (fun y hy ↦ hgs p y hp hy)
have B : Continuous (g p) := by
refine hg.comp_continuous (.prodMk_right _) fun x => ?_
simpa only [prodMk_mem_set_prod_eq, mem_univ, and_true] using hp
rcases eq_zero_or_locallyCompactSpace_of_support_subset_isCompact_of_addGroup hk A B with H | H
· simp [H] at hx
· exact H
rintro ⟨q₀, x₀⟩ ⟨hq₀, -⟩
obtain ⟨t, t_comp, ht⟩ : ∃ t, IsCompact t ∧ t ∈ 𝓝 x₀ := exists_compact_mem_nhds x₀
let k' : Set G := (-k) +ᵥ t
have k'_comp : IsCompact k' := IsCompact.vadd_set hk.neg t_comp
let g' : (P × G) → G → E' := fun p x ↦ g p.1 (p.2 - x)
let s' : Set (P × G) := s ×ˢ t
have A : ContinuousOn g'.uncurry (s' ×ˢ univ) :=
by
have : g'.uncurry = g.uncurry ∘ (fun w ↦ (w.1.1, w.1.2 - w.2)) := by ext y; rfl
rw [this]
refine hg.comp (by fun_prop) ?_
simp +contextual [s', MapsTo]
have B : ContinuousOn (fun a ↦ ∫ x, L (f x) (g' a x) ∂μ) s' :=
by
apply
continuousOn_integral_bilinear_of_locally_integrable_of_compact_support L k'_comp A _
(hf.integrableOn_isCompact k'_comp)
rintro ⟨p, x⟩ y ⟨hp, hx⟩ hy
apply hgs p _ hp
contrapose! hy
exact ⟨y - x, by simpa using hy, x, hx, by simp⟩
apply ContinuousWithinAt.mono_of_mem_nhdsWithin (B (q₀, x₀) ⟨hq₀, mem_of_mem_nhds ht⟩)
exact mem_nhdsWithin_prod_iff.2 ⟨s, self_mem_nhdsWithin, t, nhdsWithin_le_nhds ht, Subset.rfl⟩
