feat: continuity of parametric integrals with weaker assumptions (#8247)

The current version of continuity of parametric integrals assume a first countable topology, to apply the dominated convergence theorem. When one deals with continuous compactly supported functions, this is not necessary, and a direct elementary approach makes it possible to remove the first countable assumption.

Author: sgouezel

Mathlib/Analysis/Convolution.lean

@@ -433,7 +433,7 @@ end CommGroup
 
 end ConvolutionExists
 
-variable [NormedSpace ℝ F] [CompleteSpace F]
+variable [NormedSpace ℝ F]
 
 /-- The convolution of two functions `f` and `g` with respect to a continuous bilinear map `L` and
 measure `μ`. It is defined to be `(f ⋆[L, μ] g) x = ∫ t, L (f t) (g (x - t)) ∂μ`. -/
@@ -443,13 +443,16 @@ noncomputable def convolution [Sub G] (f : G → E) (g : G → E') (L : E →L[
 #align convolution convolution
 
 -- mathport name: convolution
+/-- The convolution of two functions with respect to a bilinear operation `L` and a measure `μ`. -/
 scoped[Convolution] notation:67 f " ⋆[" L:67 ", " μ:67 "] " g:66 => convolution f g L μ
 
 -- mathport name: convolution.volume
+/-- The convolution of two functions with respect to a bilinear operation `L` and the volume. -/
 scoped[Convolution]
   notation:67 f " ⋆[" L:67 "]" g:66 => convolution f g L MeasureTheory.MeasureSpace.volume
 
 -- mathport name: convolution.lsmul
+/-- The convolution of two real-valued functions with respect to volume. -/
 scoped[Convolution]
   notation:67 f " ⋆ " g:66 =>
     convolution f g (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.MeasureSpace.volume
@@ -590,136 +593,73 @@ protected theorem HasCompactSupport.convolution [T2Space G] (hcf : HasCompactSup
       (hcg.isCompact.add hcf).isClosed
 #align has_compact_support.convolution HasCompactSupport.convolution
 
-variable [BorelSpace G] [FirstCountableTopology G] [TopologicalSpace P] [FirstCountableTopology P]
+variable [BorelSpace G] [TopologicalSpace P]
 
 /-- 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`),
-not assuming `T2Space G`. -/
-theorem continuousOn_convolution_right_with_param' {g : P → G → E'} {s : Set P} {k : Set G}
-    (hk : IsCompact k) (h'k : IsClosed k) (hgs : ∀ p, ∀ x, p ∈ s → x ∉ k → g p x = 0)
+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
-  intro q₀ hq₀
-  replace hq₀ : q₀.1 ∈ s; · simpa only [mem_prod, mem_univ, and_true] using hq₀
-  have A : ∀ p ∈ s, Continuous (g p) := fun p hp ↦ by
-    refine hg.comp_continuous (continuous_const.prod_mk continuous_id') fun x => ?_
-    simpa only [prod_mk_mem_set_prod_eq, mem_univ, and_true] using hp
-  have B : ∀ p ∈ s, tsupport (g p) ⊆ k := fun p hp =>
-    closure_minimal (support_subset_iff'.2 fun z hz => hgs _ _ hp hz) h'k
-  /- We find a small neighborhood of `{q₀.1} × k` on which the function is uniformly bounded.
-      This follows from the continuity at all points of the compact set `k`. -/
-  obtain ⟨w, C, w_open, q₀w, hw⟩ :
-    ∃ w C, IsOpen w ∧ q₀.1 ∈ w ∧ ∀ p x, p ∈ w ∩ s → ‖g p x‖ ≤ C := by
-    have A : IsCompact ({q₀.1} ×ˢ k) := isCompact_singleton.prod hk
-    obtain ⟨t, kt, t_open, ht⟩ :
-        ∃ t, {q₀.1} ×ˢ k ⊆ t ∧ IsOpen t ∧ IsBounded (↿g '' (t ∩ s ×ˢ univ)) := by
-      apply exists_isOpen_isBounded_image_inter_of_isCompact_of_continuousOn A _ hg
-      simp only [prod_subset_prod_iff, hq₀, singleton_subset_iff, subset_univ, and_self_iff,
-        true_or_iff]
-    obtain ⟨C, Cpos, hC⟩ : ∃ C, 0 < C ∧ ↿g '' (t ∩ s ×ˢ univ) ⊆ closedBall (0 : E') C :=
-      ht.subset_closedBall_lt 0 0
-    obtain ⟨w, w_open, q₀w, hw⟩ : ∃ w, IsOpen w ∧ q₀.1 ∈ w ∧ w ×ˢ k ⊆ t
-    · obtain ⟨w, v, w_open, -, hw, hv, hvw⟩ :
-        ∃ (w : Set P) (v : Set G), IsOpen w ∧ IsOpen v ∧ {q₀.fst} ⊆ w ∧ k ⊆ v ∧ w ×ˢ v ⊆ t
-      exact generalized_tube_lemma isCompact_singleton hk t_open kt
-      exact ⟨w, w_open, singleton_subset_iff.1 hw, Subset.trans (Set.prod_mono Subset.rfl hv) hvw⟩
-    refine' ⟨w, C, w_open, q₀w, _⟩
-    rintro p x ⟨hp, hps⟩
-    by_cases hx : x ∈ k
-    · have H : (p, x) ∈ t := by
-        apply hw
-        simp only [prod_mk_mem_set_prod_eq, hp, hx, and_true_iff]
-      have H' : (p, x) ∈ (s ×ˢ univ : Set (P × G)) := by
-        simpa only [prod_mk_mem_set_prod_eq, mem_univ, and_true_iff] using hps
-      have : g p x ∈ closedBall (0 : E') C := hC (mem_image_of_mem _ (mem_inter H H'))
-      rwa [mem_closedBall_zero_iff] at this
-    · have : g p x = 0 := hgs _ _ hps hx
-      rw [this]
-      simpa only [norm_zero] using Cpos.le
-  have I1 :
-    ∀ᶠ q : P × G in 𝓝[s ×ˢ univ] q₀,
-      AEStronglyMeasurable (fun a : G => L (f a) (g q.1 (q.2 - a))) μ := by
-    filter_upwards [self_mem_nhdsWithin]
+  /- 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, -⟩
-    refine' (HasCompactSupport.convolutionExists_right L _ hf (A _ hp) _).1
-    exact hk.of_isClosed_subset (isClosed_tsupport _) (B p hp)
-  let K' := -k + {q₀.2}
-  have hK' : IsCompact K' := hk.neg.add isCompact_singleton
-  obtain ⟨U, U_open, K'U, hU⟩ : ∃ U, IsOpen U ∧ K' ⊆ U ∧ IntegrableOn f U μ :=
-    hf.integrableOn_nhds_isCompact hK'
-  let bound : G → ℝ := indicator U fun a => ‖L‖ * ‖f a‖ * C
-  have I2 : ∀ᶠ q : P × G in 𝓝[s ×ˢ univ] q₀, ∀ᵐ a ∂μ, ‖L (f a) (g q.1 (q.2 - a))‖ ≤ bound a := by
-    obtain ⟨V, V_mem, hV⟩ : ∃ V ∈ 𝓝 (0 : G), K' + V ⊆ U :=
-      compact_open_separated_add_right hK' U_open K'U
-    have : ((w ∩ s) ×ˢ ({q₀.2} + V) : Set (P × G)) ∈ 𝓝[s ×ˢ univ] q₀ := by
-      conv_rhs => rw [nhdsWithin_prod_eq, nhdsWithin_univ]
-      refine' Filter.prod_mem_prod _ (singleton_add_mem_nhds_of_nhds_zero q₀.2 V_mem)
-      exact mem_nhdsWithin_iff_exists_mem_nhds_inter.2 ⟨w, w_open.mem_nhds q₀w, Subset.rfl⟩
-    filter_upwards [this]
-    rintro ⟨p, x⟩ hpx
-    simp only [prod_mk_mem_set_prod_eq] at hpx
-    refine eventually_of_forall fun a => ?_
-    apply convolution_integrand_bound_right_of_le_of_subset _ _ hpx.2 _
-    · intro x
-      exact hw _ _ hpx.1
-    · rw [← add_assoc]
-      apply Subset.trans (add_subset_add_right (add_subset_add_right _)) hV
-      rw [neg_subset_neg]
-      exact B p hpx.1.2
-  have I3 : Integrable bound μ := by
-    rw [integrable_indicator_iff U_open.measurableSet]
-    exact (hU.norm.const_mul _).mul_const _
-  have I4 : ∀ᵐ a : G ∂μ,
-      ContinuousWithinAt (fun q : P × G => L (f a) (g q.1 (q.2 - a))) (s ×ˢ univ) q₀ := by
-    refine eventually_of_forall fun a => ?_
-    suffices H : ContinuousWithinAt (fun q : P × G => (f a, g q.1 (q.2 - a))) (s ×ˢ univ) q₀
-    exact L.continuous₂.continuousAt.comp_continuousWithinAt H
-    apply continuousWithinAt_const.prod
-    change ContinuousWithinAt (fun q : P × G => (↿g) (q.1, q.2 - a)) (s ×ˢ univ) q₀
-    have : ContinuousAt (fun q : P × G => (q.1, q.2 - a)) (q₀.1, q₀.2) :=
-      (continuous_fst.prod_mk (continuous_snd.sub continuous_const)).continuousAt
-    have h'q₀ : (q₀.1, q₀.2 - a) ∈ (s ×ˢ univ : Set (P × G)) := ⟨hq₀, mem_univ _⟩
-    refine' ContinuousWithinAt.comp (hg _ h'q₀) this.continuousWithinAt _
-    rintro ⟨q, x⟩ ⟨hq, -⟩
-    exact ⟨hq, mem_univ _⟩
-  exact continuousWithinAt_of_dominated I1 I2 I3 I4
-#align continuous_on_convolution_right_with_param' continuousOn_convolution_right_with_param'
-
-/-- 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 [T2Space G] {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) :=
-  continuousOn_convolution_right_with_param' L hk hk.isClosed hgs hf hg
+    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 (continuous_const.prod_mk continuous_id') fun x => ?_
+      simpa only [prod_mk_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
+  /- Since `G` is locally compact, one may thicken `k` a little bit into a larger compact set
+  `(-k) + t`, outside of which all functions that appear in the convolution vanish. Then we can
+  apply a continuity statement for integrals depending on a parameter, with respect to
+  locally integrable functions and compactly supported continuous functions. -/
+  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 (continuous_fst.fst.prod_mk (continuous_fst.snd.sub
+      continuous_snd)).continuousOn ?_
+    simp (config := {contextual := true}) [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, x, by simpa using hy, hx, by simp⟩
+  apply ContinuousWithinAt.mono_of_mem (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⟩
+#align continuous_on_convolution_right_with_param' continuousOn_convolution_right_with_param
 #align continuous_on_convolution_right_with_param continuousOn_convolution_right_with_param
 
 /-- 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 an open subset `s` of
 a parameter space `P` (and the compact support `k` is independent of the parameter in `s`),
-given in terms of compositions with an additional continuous map.
-Version not assuming `T2Space G`. -/
-theorem continuousOn_convolution_right_with_param_comp' {s : Set P} {v : P → G}
-    (hv : ContinuousOn v s) {g : P → G → E'} {k : Set G} (hk : IsCompact k) (h'k : IsClosed k)
+given in terms of compositions with an additional continuous map. -/
+theorem continuousOn_convolution_right_with_param_comp {s : Set P} {v : P → G}
+    (hv : ContinuousOn v s) {g : P → G → E'} {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 x => (f ⋆[L, μ] g x) (v x)) s := by
   apply
-    (continuousOn_convolution_right_with_param' L hk h'k hgs hf hg).comp (continuousOn_id.prod hv)
+    (continuousOn_convolution_right_with_param L hk hgs hf hg).comp (continuousOn_id.prod hv)
   intro x hx
   simp only [hx, prod_mk_mem_set_prod_eq, mem_univ, and_self_iff, id.def]
-#align continuous_on_convolution_right_with_param_comp' continuousOn_convolution_right_with_param_comp'
-
-/-- 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 an open subset `s` of
-a parameter space `P` (and the compact support `k` is independent of the parameter in `s`),
-given in terms of compositions with an additional continuous map. -/
-theorem continuousOn_convolution_right_with_param_comp [T2Space G] {s : Set P} {v : P → G}
-    (hv : ContinuousOn v s) {g : P → G → E'} {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 x => (f ⋆[L, μ] g x) (v x)) s :=
-  continuousOn_convolution_right_with_param_comp' L hv hk hk.isClosed hgs hf hg
+#align continuous_on_convolution_right_with_param_comp' continuousOn_convolution_right_with_param_comp
 #align continuous_on_convolution_right_with_param_comp continuousOn_convolution_right_with_param_comp
 
 /-- The convolution is continuous if one function is locally integrable and the other has compact
@@ -729,14 +669,15 @@ theorem HasCompactSupport.continuous_convolution_right (hcg : HasCompactSupport
   rw [continuous_iff_continuousOn_univ]
   let g' : G → G → E' := fun _ q => g q
   have : ContinuousOn (↿g') (univ ×ˢ univ) := (hg.comp continuous_snd).continuousOn
-  exact continuousOn_convolution_right_with_param_comp' L
-    (continuous_iff_continuousOn_univ.1 continuous_id) hcg (isClosed_tsupport _)
+  exact continuousOn_convolution_right_with_param_comp L
+    (continuous_iff_continuousOn_univ.1 continuous_id) hcg
     (fun p x _ hx => image_eq_zero_of_nmem_tsupport hx) hf this
 #align has_compact_support.continuous_convolution_right HasCompactSupport.continuous_convolution_right
 
 /-- The convolution is continuous if one function is integrable and the other is bounded and
 continuous. -/
-theorem BddAbove.continuous_convolution_right_of_integrable [SecondCountableTopologyEither G E']
+theorem BddAbove.continuous_convolution_right_of_integrable
+    [FirstCountableTopology G] [SecondCountableTopologyEither G E']
     (hbg : BddAbove (range fun x => ‖g x‖)) (hf : Integrable f μ) (hg : Continuous g) :
     Continuous (f ⋆[L, μ] g) := by
   refine' continuous_iff_continuousAt.mpr fun x₀ => _
@@ -815,7 +756,7 @@ variable [TopologicalAddGroup G]
 
 variable [BorelSpace G]
 
-theorem HasCompactSupport.continuous_convolution_left [FirstCountableTopology G]
+theorem HasCompactSupport.continuous_convolution_left
     (hcf : HasCompactSupport f) (hf : Continuous f) (hg : LocallyIntegrable g μ) :
     Continuous (f ⋆[L, μ] g) := by
   rw [← convolution_flip]

Mathlib/MeasureTheory/Integral/SetIntegral.lean

@@ -1431,3 +1431,92 @@ theorem Integrable.simpleFunc_mul' (hm : m ≤ m0) (g : @SimpleFunc β m ℝ) (h
 end MeasureTheory
 
 end BilinearMap
+
+section ParametricIntegral
+
+variable {α β F G 𝕜 : Type*} [TopologicalSpace α] [TopologicalSpace β] [MeasurableSpace β]
+  [OpensMeasurableSpace β] {μ : Measure β} [NontriviallyNormedField 𝕜] [NormedSpace ℝ E]
+  [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G]
+
+open Metric Function ContinuousLinearMap
+
+/-- Consider a parameterized integral `a ↦ ∫ x, L (g x) (f a x)` where `L` is bilinear,
+`g` is locally integrable and `f` is continuous and uniformly compactly supported. Then the
+integral depends continuously on `a`. -/
+lemma continuousOn_integral_bilinear_of_locally_integrable_of_compact_support
+    [NormedSpace 𝕜 E] (L : F →L[𝕜] G →L[𝕜] E)
+    {f : α → β → G} {s : Set α} {k : Set β} {g : β → F}
+    (hk : IsCompact k) (hf : ContinuousOn f.uncurry (s ×ˢ univ))
+    (hfs : ∀ p, ∀ x, p ∈ s → x ∉ k → f p x = 0) (hg : IntegrableOn g k μ) :
+    ContinuousOn (fun a ↦ ∫ x, L (g x) (f a x) ∂μ) s := by
+  have A : ∀ p ∈ s, Continuous (f p) := fun p hp ↦ by
+    refine hf.comp_continuous (continuous_const.prod_mk continuous_id') fun x => ?_
+    simpa only [prod_mk_mem_set_prod_eq, mem_univ, and_true] using hp
+  intro q hq
+  apply Metric.continuousWithinAt_iff'.2 (fun ε εpos ↦ ?_)
+  obtain ⟨δ, δpos, hδ⟩ : ∃ (δ : ℝ), 0 < δ ∧ ∫ x in k, ‖L‖ * ‖g x‖ * δ ∂μ < ε := by
+    simpa [integral_mul_right] using exists_pos_mul_lt εpos _
+  obtain ⟨v, v_mem, hv⟩ : ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ k, dist (f p x) (f q x) < δ :=
+    hk.mem_uniformity_of_prod
+      (hf.mono (Set.prod_mono_right (subset_univ k))) hq (dist_mem_uniformity δpos)
+  simp_rw [dist_eq_norm] at hv ⊢
+  have I : ∀ p ∈ s, IntegrableOn (fun x ↦ L (g x) (f p x)) k μ := by
+    intro p hp
+    obtain ⟨C, hC⟩ : ∃ C, ∀ x, ‖f p x‖ ≤ C := by
+      have : ContinuousOn (f p) k := by
+        have : ContinuousOn (fun x ↦ (p, x)) k := (Continuous.Prod.mk p).continuousOn
+        exact hf.comp this (by simp [MapsTo, hp])
+      rcases IsCompact.exists_bound_of_continuousOn hk this with ⟨C, hC⟩
+      refine ⟨max C 0, fun x ↦ ?_⟩
+      by_cases hx : x ∈ k
+      · exact (hC x hx).trans (le_max_left _ _)
+      · simp [hfs p x hp hx]
+    have : IntegrableOn (fun x ↦ ‖L‖ * ‖g x‖ * C) k μ :=
+      (hg.norm.const_mul _).mul_const _
+    apply Integrable.mono' this ?_ ?_
+    · borelize G
+      apply L.aestronglyMeasurable_comp₂ hg.aestronglyMeasurable
+      apply StronglyMeasurable.aestronglyMeasurable
+      apply Continuous.stronglyMeasurable_of_support_subset_isCompact (A p hp) hk
+      apply support_subset_iff'.2 (fun x hx ↦ hfs p x hp hx)
+    · apply eventually_of_forall (fun x ↦ (le_op_norm₂ L (g x) (f p x)).trans ?_)
+      gcongr
+      apply hC
+  filter_upwards [v_mem, self_mem_nhdsWithin] with p hp h'p
+  calc
+  ‖∫ x, L (g x) (f p x) ∂μ - ∫ x, L (g x) (f q x) ∂μ‖
+    = ‖∫ x in k, L (g x) (f p x) ∂μ - ∫ x in k, L (g x) (f q x) ∂μ‖ := by
+      congr 2
+      · refine (set_integral_eq_integral_of_forall_compl_eq_zero (fun x hx ↦ ?_)).symm
+        simp [hfs p x h'p hx]
+      · refine (set_integral_eq_integral_of_forall_compl_eq_zero (fun x hx ↦ ?_)).symm
+        simp [hfs q x hq hx]
+  _ = ‖∫ x in k, L (g x) (f p x) - L (g x) (f q x) ∂μ‖ := by rw [integral_sub (I p h'p) (I q hq)]
+  _ ≤ ∫ x in k, ‖L (g x) (f p x) - L (g x) (f q x)‖ ∂μ := norm_integral_le_integral_norm _
+  _ ≤ ∫ x in k, ‖L‖ * ‖g x‖ * δ ∂μ := by
+      apply integral_mono_of_nonneg (eventually_of_forall (fun x ↦ by positivity))
+      · exact (hg.norm.const_mul _).mul_const _
+      · apply eventually_of_forall (fun x ↦ ?_)
+        by_cases hx : x ∈ k
+        · dsimp only
+          specialize hv p hp x hx
+          calc
+          ‖L (g x) (f p x) - L (g x) (f q x)‖
+            = ‖L (g x) (f p x - f q x)‖ := by simp only [map_sub]
+          _ ≤ ‖L‖ * ‖g x‖ * ‖f p x - f q x‖ := le_op_norm₂ _ _ _
+          _ ≤ ‖L‖ * ‖g x‖ * δ := by gcongr
+        · simp only [hfs p x h'p hx, hfs q x hq hx, sub_self, norm_zero, mul_zero]
+          positivity
+  _ < ε := hδ
+
+/-- Consider a parameterized integral `a ↦ ∫ x, f a x` where `f` is continuous and uniformly
+compactly supported. Then the integral depends continuously on `a`. -/
+lemma continuousOn_integral_of_compact_support
+    {f : α → β → E} {s : Set α} {k : Set β} [IsFiniteMeasureOnCompacts μ]
+    (hk : IsCompact k) (hf : ContinuousOn f.uncurry (s ×ˢ univ))
+    (hfs : ∀ p, ∀ x, p ∈ s → x ∉ k → f p x = 0) :
+    ContinuousOn (fun a ↦ ∫ x, f a x ∂μ) s := by
+  simpa using continuousOn_integral_bilinear_of_locally_integrable_of_compact_support (lsmul ℝ ℝ)
+    hk hf hfs (integrableOn_const.2 (Or.inr hk.measure_lt_top)) (μ := μ) (g := fun _ ↦ 1)
+
+end ParametricIntegral