English
The auxiliary form of the parametric right convolution differentiability principle ensures compatibility across universe-mapping constructions.
Русский
Вспомогательная форма принципа дифференцируемости правой свёртки с параметром обеспечивает совместимость через отображения между вселенными.
LaTeX
$$$$\\text{contDiffOn}_\\mathbb{C} (f⋆[L, μ] g) = \\text{contDiffOn}_\\mathbb{C} (f⋆[L, μ] g) \\text{ (auxiliary)}.$$$$
Lean4
/-- The convolution `f * g` is `C^n` when `f` is locally integrable and `g` is `C^n` 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`).
In this version, all the types belong to the same universe (to get an induction working in the
proof). Use instead `contDiffOn_convolution_right_with_param`, which removes this restriction. -/
theorem contDiffOn_convolution_right_with_param_aux {G : Type uP} {E' : Type uP} {F : Type uP} {P : Type uP}
[NormedAddCommGroup E'] [NormedAddCommGroup F] [NormedSpace 𝕜 E'] [NormedSpace ℝ F] [NormedSpace 𝕜 F]
[MeasurableSpace G] {μ : Measure G} [NormedAddCommGroup G] [BorelSpace G] [NormedSpace 𝕜 G] [NormedAddCommGroup P]
[NormedSpace 𝕜 P] {f : G → E} {n : ℕ∞} (L : E →L[𝕜] E' →L[𝕜] F) {g : P → G → E'} {s : Set P} {k : Set G}
(hs : IsOpen s) (hk : IsCompact k) (hgs : ∀ p, ∀ x, p ∈ s → x ∉ k → g p x = 0) (hf : LocallyIntegrable f μ)
(hg : ContDiffOn 𝕜 n ↿g (s ×ˢ univ)) : ContDiffOn 𝕜 n (fun q : P × G => (f ⋆[L, μ] g q.1) q.2) (s ×ˢ univ) := by
/- We have a formula for the derivation of `f * g`, which is of the same form, thanks to
`hasFDerivAt_convolution_right_with_param`. Therefore, we can prove the result by induction on
`n` (but for this we need the spaces at the different steps of the induction to live in the same
universe, which is why we make the assumption in the lemma that all the relevant spaces
come from the same universe). -/
induction n using ENat.nat_induction generalizing g E' F with
| zero =>
rw [WithTop.coe_zero, contDiffOn_zero] at hg ⊢
exact continuousOn_convolution_right_with_param L hk hgs hf hg
| succ n
ih =>
simp only [Nat.succ_eq_add_one, Nat.cast_add, Nat.cast_one, WithTop.coe_add, WithTop.coe_natCast,
WithTop.coe_one] at hg ⊢
let f' : P → G → P × G →L[𝕜] F := fun p a => (f ⋆[L.precompR (P × G), μ] fun x : G => fderiv 𝕜 (uncurry g) (p, x)) a
have A : ∀ q₀ : P × G, q₀.1 ∈ s → HasFDerivAt (fun q : P × G => (f ⋆[L, μ] g q.1) q.2) (f' q₀.1 q₀.2) q₀ :=
hasFDerivAt_convolution_right_with_param L hs hk hgs hf hg.one_of_succ
rw [contDiffOn_succ_iff_fderiv_of_isOpen (hs.prod (@isOpen_univ G _))] at hg ⊢
refine ⟨?_, by simp, ?_⟩
· rintro ⟨p, x⟩ ⟨hp, -⟩
exact (A (p, x) hp).differentiableAt.differentiableWithinAt
· suffices H : ContDiffOn 𝕜 n ↿f' (s ×ˢ univ) by
apply H.congr
rintro ⟨p, x⟩ ⟨hp, -⟩
exact (A (p, x) hp).fderiv
have B : ∀ (p : P) (x : G), p ∈ s → x ∉ k → fderiv 𝕜 (uncurry g) (p, x) = 0 :=
by
intro p x hp hx
apply (hasFDerivAt_zero_of_eventually_const (0 : E') _).fderiv
have M2 : kᶜ ∈ 𝓝 x := IsOpen.mem_nhds hk.isClosed.isOpen_compl hx
have M1 : s ∈ 𝓝 p := hs.mem_nhds hp
rw [nhds_prod_eq]
filter_upwards [prod_mem_prod M1 M2]
rintro ⟨p, y⟩ ⟨hp, hy⟩
exact hgs p y hp hy
apply ih (L.precompR (P × G) :) B
convert hg.2.2
| top ih =>
rw [contDiffOn_infty] at hg ⊢
exact fun n ↦ ih n L hgs (hg n)
