Mathlib/Analysis/Calculus/ContDiff/Convolution.lean

Exact source: Mathlib/Analysis/Calculus/ContDiff/Convolution.lean

Pinned GitHub source · Raw UTF-8 source

Back to Differentiating a local mollification through its kernel

1/-2Copyright (c) 2022 Floris van Doorn. All rights reserved.3Released under Apache 2.0 license as described in the file LICENSE.4Authors: Floris van Doorn5-/6module78public import Mathlib.Analysis.Calculus.ContDiff.Comp9public import Mathlib.Analysis.Calculus.ParametricIntegral10public import Mathlib.Analysis.Convolution1112/-!13# Differentiability of a convolution of functions1415Criteria for a convolution of functions to be differentiable.1617## Main Results1819* `HasCompactSupport.hasFDerivAt_convolution_right` and20  `HasCompactSupport.hasFDerivAt_convolution_left`: we can compute the total derivative21  of the convolution as a convolution with the total derivative of the right (left) function.22* `HasCompactSupport.contDiff_convolution_right` and23  `HasCompactSupport.contDiff_convolution_left`: the convolution is `𝒞ⁿ` if one of the functions24  is `𝒞ⁿ` with compact support and the other function in locally integrable.2526-/2728public section29open Set Function Filter MeasureTheory MeasureTheory.Measure TopologicalSpace3031open Bornology ContinuousLinearMap Metric Topology32open scoped Pointwise NNReal Filter3334universe u𝕜 uG uE uE' uE'' uF uF' uF'' uP3536variable {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {E'' : Type uE''} {F : Type uF}37  {F' : Type uF'} {F'' : Type uF''} {P : Type uP}3839variable [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup E'']40  [NormedAddCommGroup F] {f f' : G → E} {g g' : G → E'} {x x' : G} {y y' : E}4142namespace MeasureTheory4344open scoped Convolution4546section RCLike47variable [RCLike 𝕜]48variable [NormedSpace 𝕜 E]49variable [NormedSpace 𝕜 E']50variable [NormedSpace 𝕜 E'']51variable [NormedSpace ℝ F] [NormedSpace 𝕜 F]52variable {n : ℕ∞}53variable [MeasurableSpace G] {μ ν : Measure G}54variable (L : E →L[𝕜] E' →L[𝕜] F)5556variable [NormedAddCommGroup G] [BorelSpace G]5758variable [NormedSpace 𝕜 G] [SFinite μ] [IsAddLeftInvariant μ]5960/-- Compute the total derivative of `f ⋆ g` if `g` is `C^1` with compact support and `f` is locally61integrable. To write down the total derivative as a convolution, we use62`ContinuousLinearMap.precompR`. -/63theorem _root_.HasCompactSupport.hasFDerivAt_convolution_right (hcg : HasCompactSupport g)64    (hf : LocallyIntegrable f μ) (hg : ContDiff 𝕜 1 g) (x₀ : G) :65    HasFDerivAt (f ⋆[L, μ] g) ((f ⋆[L.precompR G, μ] fderiv 𝕜 g) x₀) x₀ := by66  rcases hcg.eq_zero_or_finiteDimensional 𝕜 hg.continuous with (rfl | fin_dim)67  · have : fderiv 𝕜 (0 : G → E') = 0 := fderiv_const (0 : E')68    simp only [this, convolution_zero, Pi.zero_apply]69    exact hasFDerivAt_const (0 : F) x₀70  have : ProperSpace G := FiniteDimensional.proper_rclike 𝕜 G71  set L' := L.precompR G72  have h1 : ∀ᶠ x in 𝓝 x₀, AEStronglyMeasurable (fun t => L (f t) (g (x - t))) μ :=73    Eventually.of_forall74      (hf.aestronglyMeasurable.convolution_integrand_snd L hg.continuous.aestronglyMeasurable)75  have h2 : ∀ x, AEStronglyMeasurable (fun t => L' (f t) (fderiv 𝕜 g (x - t))) μ :=76    hf.aestronglyMeasurable.convolution_integrand_snd L'77      (hg.continuous_fderiv one_ne_zero).aestronglyMeasurable78  have h3 : ∀ x t, HasFDerivAt (fun x => g (x - t)) (fderiv 𝕜 g (x - t)) x := fun x t ↦ by79    simpa using!80      (hg.differentiable one_ne_zero).differentiableAt.hasFDerivAt.comp x81        ((hasFDerivAt_id x).sub (hasFDerivAt_const t x))82  let K' := -tsupport (fderiv 𝕜 g) + closedBall x₀ 183  have hK' : IsCompact K' := (hcg.fderiv 𝕜).isCompact.neg.add (isCompact_closedBall x₀ 1)84  apply hasFDerivAt_integral_of_dominated_of_fderiv_le (ball_mem_nhds _ zero_lt_one) h1 _ (h2 x₀)85  · filter_upwards with t x hx using86      (hcg.fderiv 𝕜).convolution_integrand_bound_right L' (hg.continuous_fderiv one_ne_zero)87        (ball_subset_closedBall hx)88  · rw [integrable_indicator_iff hK'.measurableSet]89    exact ((hf.integrableOn_isCompact hK').norm.const_mul _).mul_const _90  · exact Eventually.of_forall fun t x _ => (L _).hasFDerivAt.comp x (h3 x t)91  · exact hcg.convolutionExists_right L hf hg.continuous x₀9293theorem _root_.HasCompactSupport.hasFDerivAt_convolution_left [IsNegInvariant μ]94    (hcf : HasCompactSupport f) (hf : ContDiff 𝕜 1 f) (hg : LocallyIntegrable g μ) (x₀ : G) :95    HasFDerivAt (f ⋆[L, μ] g) ((fderiv 𝕜 f ⋆[L.precompL G, μ] g) x₀) x₀ := by96  simp +singlePass only [← convolution_flip]97  exact hcf.hasFDerivAt_convolution_right L.flip hg hf x₀9899end RCLike100101section Real102103/-! The one-variable case -/104105variable [RCLike 𝕜]106variable [NormedSpace 𝕜 E]107variable [NormedSpace 𝕜 E']108variable [NormedSpace ℝ F] [NormedSpace 𝕜 F]109variable {f₀ : 𝕜 → E} {g₀ : 𝕜 → E'}110variable {n : ℕ∞}111variable (L : E →L[𝕜] E' →L[𝕜] F)112variable {μ : Measure 𝕜}113variable [IsAddLeftInvariant μ] [SFinite μ]114115theorem _root_.HasCompactSupport.hasDerivAt_convolution_right (hf : LocallyIntegrable f₀ μ)116    (hcg : HasCompactSupport g₀) (hg : ContDiff 𝕜 1 g₀) (x₀ : 𝕜) :117    HasDerivAt (f₀ ⋆[L, μ] g₀) ((f₀ ⋆[L, μ] deriv g₀) x₀) x₀ := by118  convert (hcg.hasFDerivAt_convolution_right L hf hg x₀).hasDerivAt119  rw [convolution_precompR_apply L hf (hcg.fderiv 𝕜) (hg.continuous_fderiv one_ne_zero)]120  rfl121122theorem _root_.HasCompactSupport.hasDerivAt_convolution_left [IsNegInvariant μ]123    (hcf : HasCompactSupport f₀) (hf : ContDiff 𝕜 1 f₀) (hg : LocallyIntegrable g₀ μ) (x₀ : 𝕜) :124    HasDerivAt (f₀ ⋆[L, μ] g₀) ((deriv f₀ ⋆[L, μ] g₀) x₀) x₀ := by125  simp +singlePass only [← convolution_flip]126  exact hcf.hasDerivAt_convolution_right L.flip hg hf x₀127128end Real129130section WithParam131132variable [RCLike 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 E''] [NormedSpace ℝ F]133  [NormedSpace 𝕜 F] [MeasurableSpace G] [NormedAddCommGroup G] [BorelSpace G]134  [NormedSpace 𝕜 G] [NormedAddCommGroup P] [NormedSpace 𝕜 P] {μ : Measure G}135  (L : E →L[𝕜] E' →L[𝕜] F)136137/-- The derivative of the convolution `f * g` is given by `f * Dg`, when `f` is locally integrable138and `g` is `C^1` and compactly supported. Version where `g` depends on an additional parameter in an139open subset `s` of a parameter space `P` (and the compact support `k` is independent of the140parameter in `s`). -/141theorem hasFDerivAt_convolution_right_with_param {g : P → G → E'} {s : Set P} {k : Set G}142    (hs : IsOpen s) (hk : IsCompact k) (hgs : ∀ p, ∀ x, p ∈ s → x ∉ k → g p x = 0)143    (hf : LocallyIntegrable f μ) (hg : ContDiffOn 𝕜 1 ↿g (s ×ˢ univ)) (q₀ : P × G)144    (hq₀ : q₀.1 ∈ s) :145    HasFDerivAt (fun q : P × G => (f ⋆[L, μ] g q.1) q.2)146      ((f ⋆[L.precompR (P × G), μ] fun x : G => fderiv 𝕜 ↿g (q₀.1, x)) q₀.2) q₀ := by147  let g' := fderiv 𝕜 ↿g148  have A : ∀ p ∈ s, Continuous (g p) := fun p hp ↦ by149    refine hg.continuousOn.comp_continuous (.prodMk_right _) fun x => ?_150    simpa only [prodMk_mem_set_prod_eq, mem_univ, and_true] using hp151  have A' : ∀ q : P × G, q.1 ∈ s → s ×ˢ univ ∈ 𝓝 q := fun q hq ↦ by152    apply (hs.prod isOpen_univ).mem_nhds153    simpa only [mem_prod, mem_univ, and_true] using hq154  -- The derivative of `g` vanishes away from `k`.155  have g'_zero : ∀ p x, p ∈ s → x ∉ k → g' (p, x) = 0 := by156    intro p x hp hx157    refine (hasFDerivAt_zero_of_eventually_const 0 ?_).fderiv158    have M2 : kᶜ ∈ 𝓝 x := hk.isClosed.isOpen_compl.mem_nhds hx159    have M1 : s ∈ 𝓝 p := hs.mem_nhds hp160    rw [nhds_prod_eq]161    filter_upwards [prod_mem_prod M1 M2]162    rintro ⟨p, y⟩ ⟨hp, hy⟩163    exact hgs p y hp hy164  /- We find a small neighborhood of `{q₀.1} × k` on which the derivative is uniformly bounded. This165    follows from the continuity at all points of the compact set `k`. -/166  obtain ⟨ε, C, εpos, h₀ε, hε⟩ :167      ∃ ε C, 0 < ε ∧ ball q₀.1 ε ⊆ s ∧ ∀ p x, ‖p - q₀.1‖ < ε → ‖g' (p, x)‖ ≤ C := by168    have A : IsCompact ({q₀.1} ×ˢ k) := isCompact_singleton.prod hk169    obtain ⟨t, kt, t_open, ht⟩ : ∃ t, {q₀.1} ×ˢ k ⊆ t ∧ IsOpen t ∧ IsBounded (g' '' t) := by170      have B : ContinuousOn g' (s ×ˢ univ) :=171        hg.continuousOn_fderiv_of_isOpen (hs.prod isOpen_univ) le_rfl172      apply exists_isOpen_isBounded_image_of_isCompact_of_continuousOn A (hs.prod isOpen_univ) _ B173      simp only [prod_subset_prod_iff, hq₀, singleton_subset_iff, subset_univ, and_self_iff,174        true_or]175    obtain ⟨ε, εpos, hε, h'ε⟩ :176      ∃ ε : ℝ, 0 < ε ∧ thickening ε ({q₀.fst} ×ˢ k) ⊆ t ∧ ball q₀.1 ε ⊆ s := by177      obtain ⟨ε, εpos, hε⟩ : ∃ ε : ℝ, 0 < ε ∧ thickening ε (({q₀.fst} : Set P) ×ˢ k) ⊆ t :=178        A.exists_thickening_subset_open t_open kt179      obtain ⟨δ, δpos, hδ⟩ : ∃ δ : ℝ, 0 < δ ∧ ball q₀.1 δ ⊆ s := Metric.isOpen_iff.1 hs _ hq₀180      refine ⟨min ε δ, lt_min εpos δpos, ?_, ?_⟩181      · exact Subset.trans (thickening_mono (min_le_left _ _) _) hε182      · exact Subset.trans (ball_subset_ball (min_le_right _ _)) hδ183    obtain ⟨C, Cpos, hC⟩ : ∃ C, 0 < C ∧ g' '' t ⊆ closedBall 0 C := ht.subset_closedBall_lt 0 0184    refine ⟨ε, C, εpos, h'ε, fun p x hp => ?_⟩185    have hps : p ∈ s := h'ε (mem_ball_iff_norm.2 hp)186    by_cases hx : x ∈ k187    · have H : (p, x) ∈ t := by188        apply hε189        refine mem_thickening_iff.2 ⟨(q₀.1, x), ?_, ?_⟩190        · simp only [hx, singleton_prod, mem_image, Prod.mk_inj, true_and, exists_eq_right]191        · rw [← dist_eq_norm] at hp192          simpa only [Prod.dist_eq, εpos, dist_self, max_lt_iff, and_true] using hp193      have : g' (p, x) ∈ closedBall (0 : P × G →L[𝕜] E') C := hC (mem_image_of_mem _ H)194      rwa [mem_closedBall_zero_iff] at this195    · have : g' (p, x) = 0 := g'_zero _ _ hps hx196      rw [this]197      simpa only [norm_zero] using Cpos.le198  /- Now, we wish to apply a theorem on differentiation of integrals. For this, we need to check199    trivial measurability or integrability assumptions (in `I1`, `I2`, `I3`), as well as a uniform200    integrability assumption over the derivative (in `I4` and `I5`) and pointwise differentiability201    in `I6`. -/202  have I1 :203    ∀ᶠ x : P × G in 𝓝 q₀, AEStronglyMeasurable (fun a : G => L (f a) (g x.1 (x.2 - a))) μ := by204    filter_upwards [A' q₀ hq₀]205    rintro ⟨p, x⟩ ⟨hp, -⟩206    refine (HasCompactSupport.convolutionExists_right L ?_ hf (A _ hp) _).1207    apply hk.of_isClosed_subset (isClosed_tsupport _)208    exact closure_minimal (support_subset_iff'.2 fun z hz => hgs _ _ hp hz) hk.isClosed209  have I2 : Integrable (fun a : G => L (f a) (g q₀.1 (q₀.2 - a))) μ := by210    have M : HasCompactSupport (g q₀.1) := HasCompactSupport.intro hk fun x hx => hgs q₀.1 x hq₀ hx211    apply M.convolutionExists_right L hf (A q₀.1 hq₀) q₀.2212  have I3 : AEStronglyMeasurable (fun a : G => (L (f a)).comp (g' (q₀.fst, q₀.snd - a))) μ := by213    have T : HasCompactSupport fun y => g' (q₀.1, y) :=214      HasCompactSupport.intro hk fun x hx => g'_zero q₀.1 x hq₀ hx215    apply (HasCompactSupport.convolutionExists_right (L.precompR (P × G) :) T hf _ q₀.2).1216    have : ContinuousOn g' (s ×ˢ univ) :=217      hg.continuousOn_fderiv_of_isOpen (hs.prod isOpen_univ) le_rfl218    apply this.comp_continuous (.prodMk_right _)219    intro x220    simpa only [prodMk_mem_set_prod_eq, mem_univ, and_true] using hq₀221  set K' := (-k + {q₀.2} : Set G) with K'_def222  have hK' : IsCompact K' := hk.neg.add isCompact_singleton223  obtain ⟨U, U_open, K'U, hU⟩ : ∃ U, IsOpen U ∧ K' ⊆ U ∧ IntegrableOn f U μ :=224    hf.integrableOn_nhds_isCompact hK'225  obtain ⟨δ, δpos, δε, hδ⟩ : ∃ δ, (0 : ℝ) < δ ∧ δ ≤ ε ∧ K' + ball 0 δ ⊆ U := by226    obtain ⟨V, V_mem, hV⟩ : ∃ V ∈ 𝓝 (0 : G), K' + V ⊆ U :=227      compact_open_separated_add_right hK' U_open K'U228    rcases Metric.mem_nhds_iff.1 V_mem with ⟨δ, δpos, hδ⟩229    refine ⟨min δ ε, lt_min δpos εpos, min_le_right δ ε, ?_⟩230    exact (add_subset_add_left ((ball_subset_ball (min_le_left _ _)).trans hδ)).trans hV231  letI := ContinuousLinearMap.hasOpNorm (𝕜 := 𝕜) (𝕜₂ := 𝕜) (E := E)232    (F := (P × G →L[𝕜] E') →L[𝕜] P × G →L[𝕜] F) (σ₁₂ := RingHom.id 𝕜)233  let bound : G → ℝ := indicator U fun t => ‖(L.precompR (P × G))‖ * ‖f t‖ * C234  have I4 : ∀ᵐ a : G ∂μ, ∀ x : P × G, dist x q₀ < δ →235      ‖L.precompR (P × G) (f a) (g' (x.fst, x.snd - a))‖ ≤ bound a := by236    filter_upwards with a x hx237    rw [Prod.dist_eq, dist_eq_norm, dist_eq_norm] at hx238    have : (-tsupport fun a => g' (x.1, a)) + ball q₀.2 δ ⊆ U := by239      apply Subset.trans _ hδ240      rw [K'_def, add_assoc]241      apply add_subset_add242      · rw [neg_subset_neg]243        refine closure_minimal (support_subset_iff'.2 fun z hz => ?_) hk.isClosed244        apply g'_zero x.1 z (h₀ε _) hz245        rw [mem_ball_iff_norm]246        exact ((le_max_left _ _).trans_lt hx).trans_le δε247      · simp only [add_ball, thickening_singleton, zero_vadd, subset_rfl]248    apply convolution_integrand_bound_right_of_le_of_subset _ _ _ this249    · intro y250      exact hε _ _ (((le_max_left _ _).trans_lt hx).trans_le δε)251    · rw [mem_ball_iff_norm]252      exact (le_max_right _ _).trans_lt hx253  have I5 : Integrable bound μ := by254    rw [integrable_indicator_iff U_open.measurableSet]255    exact (hU.norm.const_mul _).mul_const _256  have I6 : ∀ᵐ a : G ∂μ, ∀ x : P × G, dist x q₀ < δ →257      HasFDerivAt (fun x : P × G => L (f a) (g x.1 (x.2 - a)))258        ((L (f a)).comp (g' (x.fst, x.snd - a))) x := by259    filter_upwards with a x hx260    apply (L _).hasFDerivAt.comp x261    have N : s ×ˢ univ ∈ 𝓝 (x.1, x.2 - a) := by262      apply A'263      apply h₀ε264      rw [Prod.dist_eq] at hx265      exact lt_of_lt_of_le (lt_of_le_of_lt (le_max_left _ _) hx) δε266    have Z := ((hg.differentiableOn one_ne_zero).differentiableAt N).hasFDerivAt267    have Z' :268        HasFDerivAt (fun x : P × G => (x.1, x.2 - a)) (ContinuousLinearMap.id 𝕜 (P × G)) x := by269      have : (fun x : P × G => (x.1, x.2 - a)) = _root_.id - fun x => (0, a) := by270        ext x <;> simp only [Pi.sub_apply, _root_.id, Prod.fst_sub, sub_zero, Prod.snd_sub]271      rw [this]272      exact (hasFDerivAt_id x).sub_const (0, a)273    exact Z.comp x Z'274  exact hasFDerivAt_integral_of_dominated_of_fderiv_le (ball_mem_nhds _ δpos) I1 I2 I3 I4 I5 I6275276/-- The convolution `f * g` is `C^n` when `f` is locally integrable and `g` is `C^n` and compactly277supported. Version where `g` depends on an additional parameter in an open subset `s` of a278parameter space `P` (and the compact support `k` is independent of the parameter in `s`).279In this version, all the types belong to the same universe (to get an induction working in the280proof). Use instead `contDiffOn_convolution_right_with_param`, which removes this restriction. -/281theorem contDiffOn_convolution_right_with_param_aux {G : Type uP} {E' : Type uP} {F : Type uP}282    {P : Type uP} [NormedAddCommGroup E'] [NormedAddCommGroup F] [NormedSpace 𝕜 E']283    [NormedSpace ℝ F] [NormedSpace 𝕜 F] [MeasurableSpace G]284    {μ : Measure G}285    [NormedAddCommGroup G] [BorelSpace G] [NormedSpace 𝕜 G] [NormedAddCommGroup P] [NormedSpace 𝕜 P]286    {f : G → E} {n : ℕ∞} (L : E →L[𝕜] E' →L[𝕜] F) {g : P → G → E'} {s : Set P} {k : Set G}287    (hs : IsOpen s) (hk : IsCompact k) (hgs : ∀ p, ∀ x, p ∈ s → x ∉ k → g p x = 0)288    (hf : LocallyIntegrable f μ) (hg : ContDiffOn 𝕜 n ↿g (s ×ˢ univ)) :289    ContDiffOn 𝕜 n (fun q : P × G => (f ⋆[L, μ] g q.1) q.2) (s ×ˢ univ) := by290  /- We have a formula for the derivation of `f * g`, which is of the same form, thanks to291    `hasFDerivAt_convolution_right_with_param`. Therefore, we can prove the result by induction on292    `n` (but for this we need the spaces at the different steps of the induction to live in the same293    universe, which is why we make the assumption in the lemma that all the relevant spaces294    come from the same universe). -/295  induction n using ENat.nat_induction generalizing g E' F with296  | zero =>297    rw [WithTop.coe_zero, contDiffOn_zero] at hg ⊢298    exact continuousOn_convolution_right_with_param L hk hgs hf hg299  | succ n ih =>300    simp only [Nat.succ_eq_add_one, Nat.cast_add, Nat.cast_one, WithTop.coe_add,301      WithTop.coe_natCast, WithTop.coe_one] at hg ⊢302    let f' : P → G → P × G →L[𝕜] F := fun p a =>303      (f ⋆[L.precompR (P × G), μ] fun x : G => fderiv 𝕜 (uncurry g) (p, x)) a304    have A : ∀ q₀ : P × G, q₀.1 ∈ s →305        HasFDerivAt (fun q : P × G => (f ⋆[L, μ] g q.1) q.2) (f' q₀.1 q₀.2) q₀ :=306      hasFDerivAt_convolution_right_with_param L hs hk hgs hf hg.one_of_succ307    rw [contDiffOn_succ_iff_fderiv_of_isOpen (hs.prod (@isOpen_univ G _))] at hg ⊢308    refine ⟨?_, by simp, ?_⟩309    · rintro ⟨p, x⟩ ⟨hp, -⟩310      exact (A (p, x) hp).differentiableAt.differentiableWithinAt311    · suffices H : ContDiffOn 𝕜 n ↿f' (s ×ˢ univ) by312        apply H.congr313        rintro ⟨p, x⟩ ⟨hp, -⟩314        exact (A (p, x) hp).fderiv315      have B : ∀ (p : P) (x : G), p ∈ s → x ∉ k → fderiv 𝕜 (uncurry g) (p, x) = 0 := by316        intro p x hp hx317        apply (hasFDerivAt_zero_of_eventually_const (0 : E') _).fderiv318        have M2 : kᶜ ∈ 𝓝 x := IsOpen.mem_nhds hk.isClosed.isOpen_compl hx319        have M1 : s ∈ 𝓝 p := hs.mem_nhds hp320        rw [nhds_prod_eq]321        filter_upwards [prod_mem_prod M1 M2]322        rintro ⟨p, y⟩ ⟨hp, hy⟩323        exact hgs p y hp hy324      apply ih (L.precompR (P × G) :) B325      convert! hg.2.2326  | top ih =>327    rw [contDiffOn_infty] at hg ⊢328    exact fun n ↦ ih n L hgs (hg n)329330/-- The convolution `f * g` is `C^n` when `f` is locally integrable and `g` is `C^n` and compactly331supported. Version where `g` depends on an additional parameter in an open subset `s` of a332parameter space `P` (and the compact support `k` is independent of the parameter in `s`). -/333theorem contDiffOn_convolution_right_with_param {f : G → E} {n : ℕ∞} (L : E →L[𝕜] E' →L[𝕜] F)334    {g : P → G → E'} {s : Set P} {k : Set G} (hs : IsOpen s) (hk : IsCompact k)335    (hgs : ∀ p, ∀ x, p ∈ s → x ∉ k → g p x = 0) (hf : LocallyIntegrable f μ)336    (hg : ContDiffOn 𝕜 n ↿g (s ×ˢ univ)) :337    ContDiffOn 𝕜 n (fun q : P × G => (f ⋆[L, μ] g q.1) q.2) (s ×ˢ univ) := by338  /- The result is known when all the universes are the same, from339    `contDiffOn_convolution_right_with_param_aux`. We reduce to this situation by pushing340    everything through `ULift` continuous linear equivalences. -/341  let eG : Type max uG uE' uF uP := ULift.{max uE' uF uP} G342  borelize eG343  let eE' : Type max uE' uG uF uP := ULift.{max uG uF uP} E'344  let eF : Type max uF uG uE' uP := ULift.{max uG uE' uP} F345  let eP : Type max uP uG uE' uF := ULift.{max uG uE' uF} P346  let isoG : eG ≃L[𝕜] G := ContinuousLinearEquiv.ulift347  let isoE' : eE' ≃L[𝕜] E' := ContinuousLinearEquiv.ulift348  let isoF : eF ≃L[𝕜] F := ContinuousLinearEquiv.ulift349  let isoP : eP ≃L[𝕜] P := ContinuousLinearEquiv.ulift350  let ef := f ∘ isoG351  let eμ : Measure eG := Measure.map isoG.symm μ352  let eg : eP → eG → eE' := fun ep ex => isoE'.symm (g (isoP ep) (isoG ex))353  let eL :=354    ContinuousLinearMap.comp355      ((ContinuousLinearEquiv.arrowCongr isoE' isoF).symm : (E' →L[𝕜] F) →L[𝕜] eE' →L[𝕜] eF) L356  let R := fun q : eP × eG => (ef ⋆[eL, eμ] eg q.1) q.2357  have R_contdiff : ContDiffOn 𝕜 n R ((isoP ⁻¹' s) ×ˢ univ) := by358    have hek : IsCompact (isoG ⁻¹' k) := isoG.toHomeomorph.isClosedEmbedding.isCompact_preimage hk359    have hes : IsOpen (isoP ⁻¹' s) := isoP.continuous.isOpen_preimage _ hs360    refine contDiffOn_convolution_right_with_param_aux eL hes hek ?_ ?_ ?_361    · intro p x hp hx362      simp only [eg,363        ContinuousLinearEquiv.map_eq_zero_iff]364      exact hgs _ _ hp hx365    · exact (locallyIntegrable_map_homeomorph isoG.symm.toHomeomorph).2 hf366    · apply isoE'.symm.contDiff.comp_contDiffOn367      apply hg.comp (isoP.prodCongr isoG).contDiff.contDiffOn368      rintro ⟨p, x⟩ ⟨hp, -⟩369      simpa only [mem_preimage, ContinuousLinearEquiv.prodCongr_apply, prodMk_mem_set_prod_eq,370        mem_univ, and_true] using hp371  have A : ContDiffOn 𝕜 n (isoF ∘ R ∘ (isoP.prodCongr isoG).symm) (s ×ˢ univ) := by372    apply isoF.contDiff.comp_contDiffOn373    apply R_contdiff.comp (ContinuousLinearEquiv.contDiff _).contDiffOn374    rintro ⟨p, x⟩ ⟨hp, -⟩375    simpa only [mem_preimage, mem_prod, mem_univ, and_true, ContinuousLinearEquiv.prodCongr_symm,376      ContinuousLinearEquiv.prodCongr_apply, ContinuousLinearEquiv.apply_symm_apply] using hp377  have : isoF ∘ R ∘ (isoP.prodCongr isoG).symm = fun q : P × G => (f ⋆[L, μ] g q.1) q.2 := by378    apply funext379    rintro ⟨p, x⟩380    simp only [(· ∘ ·), ContinuousLinearEquiv.prodCongr_symm, ContinuousLinearEquiv.prodCongr_apply]381    simp only [R, convolution]382    rw [IsClosedEmbedding.integral_map, ← isoF.integral_comp_comm]383    · rfl384    · exact isoG.symm.toHomeomorph.isClosedEmbedding385  simp_rw [this] at A386  exact A387388/-- The convolution `f * g` is `C^n` when `f` is locally integrable and `g` is `C^n` and compactly389supported. Version where `g` depends on an additional parameter in an open subset `s` of a390parameter space `P` (and the compact support `k` is independent of the parameter in `s`),391given in terms of composition with an additional `C^n` function. -/392theorem contDiffOn_convolution_right_with_param_comp {n : ℕ∞} (L : E →L[𝕜] E' →L[𝕜] F) {s : Set P}393    {v : P → G} (hv : ContDiffOn 𝕜 n v s) {f : G → E} {g : P → G → E'} {k : Set G} (hs : IsOpen s)394    (hk : IsCompact k) (hgs : ∀ p, ∀ x, p ∈ s → x ∉ k → g p x = 0) (hf : LocallyIntegrable f μ)395    (hg : ContDiffOn 𝕜 n ↿g (s ×ˢ univ)) : ContDiffOn 𝕜 n (fun x => (f ⋆[L, μ] g x) (v x)) s := by396  apply (contDiffOn_convolution_right_with_param L hs hk hgs hf hg).comp (contDiffOn_id.prodMk hv)397  intro x hx398  simp only [hx, prodMk_mem_set_prod_eq, mem_univ, and_self_iff, _root_.id]399400/-- The convolution `g * f` is `C^n` when `f` is locally integrable and `g` is `C^n` and compactly401supported. Version where `g` depends on an additional parameter in an open subset `s` of a402parameter space `P` (and the compact support `k` is independent of the parameter in `s`). -/403theorem contDiffOn_convolution_left_with_param [μ.IsAddLeftInvariant] [μ.IsNegInvariant]404    (L : E' →L[𝕜] E →L[𝕜] F) {f : G → E} {n : ℕ∞} {g : P → G → E'} {s : Set P} {k : Set G}405    (hs : IsOpen s) (hk : IsCompact k) (hgs : ∀ p, ∀ x, p ∈ s → x ∉ k → g p x = 0)406    (hf : LocallyIntegrable f μ) (hg : ContDiffOn 𝕜 n ↿g (s ×ˢ univ)) :407    ContDiffOn 𝕜 n (fun q : P × G => (g q.1 ⋆[L, μ] f) q.2) (s ×ˢ univ) := by408  simpa only [convolution_flip] using contDiffOn_convolution_right_with_param L.flip hs hk hgs hf hg409410/-- The convolution `g * f` is `C^n` when `f` is locally integrable and `g` is `C^n` and compactly411supported. Version where `g` depends on an additional parameter in an open subset `s` of a412parameter space `P` (and the compact support `k` is independent of the parameter in `s`),413given in terms of composition with additional `C^n` functions. -/414theorem contDiffOn_convolution_left_with_param_comp [μ.IsAddLeftInvariant] [μ.IsNegInvariant]415    (L : E' →L[𝕜] E →L[𝕜] F) {s : Set P} {n : ℕ∞} {v : P → G} (hv : ContDiffOn 𝕜 n v s) {f : G → E}416    {g : P → G → E'} {k : Set G} (hs : IsOpen s) (hk : IsCompact k)417    (hgs : ∀ p, ∀ x, p ∈ s → x ∉ k → g p x = 0) (hf : LocallyIntegrable f μ)418    (hg : ContDiffOn 𝕜 n ↿g (s ×ˢ univ)) : ContDiffOn 𝕜 n (fun x => (g x ⋆[L, μ] f) (v x)) s := by419  apply (contDiffOn_convolution_left_with_param L hs hk hgs hf hg).comp (contDiffOn_id.prodMk hv)420  intro x hx421  simp only [hx, prodMk_mem_set_prod_eq, mem_univ, and_self_iff, _root_.id]422423theorem _root_.HasCompactSupport.contDiff_convolution_right {n : ℕ∞} (hcg : HasCompactSupport g)424    (hf : LocallyIntegrable f μ) (hg : ContDiff 𝕜 n g) : ContDiff 𝕜 n (f ⋆[L, μ] g) := by425  rcases exists_compact_iff_hasCompactSupport.2 hcg with ⟨k, hk, h'k⟩426  rw [← contDiffOn_univ]427  exact contDiffOn_convolution_right_with_param_comp L contDiffOn_id isOpen_univ hk428    (fun p x _ hx => h'k x hx) hf (hg.comp contDiff_snd).contDiffOn429430theorem _root_.HasCompactSupport.contDiff_convolution_left [μ.IsAddLeftInvariant] [μ.IsNegInvariant]431    {n : ℕ∞} (hcf : HasCompactSupport f) (hf : ContDiff 𝕜 n f) (hg : LocallyIntegrable g μ) :432    ContDiff 𝕜 n (f ⋆[L, μ] g) := by433  rw [← convolution_flip]434  exact hcf.contDiff_convolution_right L.flip hg hf435436end WithParam437438end MeasureTheory