English
Composition with a temperate growth g defines a continuous semilinear map between Schwartz spaces
Русский
Компоновка по правой части через g задаёт непрерывное полупространство между пространствами Шварца.
LaTeX
$$$compCLM {g:\\ D→E} (hg: g.HasTemperateGrowth) (hg_upper: ∃ k C, ∀ x, ‖x‖ ≤ C(1+‖g x‖)^k) : 𝓢(E,F) →SL[σ] 𝓢(D,F)$$$
Lean4
/-- Composition with a function on the right is a continuous linear map on Schwartz space
provided that the function is temperate and growths polynomially near infinity. -/
def compCLM {g : D → E} (hg : g.HasTemperateGrowth) (hg_upper : ∃ (k : ℕ) (C : ℝ), ∀ x, ‖x‖ ≤ C * (1 + ‖g x‖) ^ k) :
𝓢(E, F) →L[𝕜] 𝓢(D, F) :=
by
refine mkCLM (fun f => f ∘ g) (fun _ _ _ => by simp) (fun _ _ _ => rfl) (fun f => (f.smooth ⊤).comp hg.1) ?_
rintro ⟨k, n⟩
rcases hg.norm_iteratedFDeriv_le_uniform_aux n with ⟨l, C, hC, hgrowth⟩
rcases hg_upper with ⟨kg, Cg, hg_upper'⟩
have hCg : 1 ≤ 1 + Cg := by
refine le_add_of_nonneg_right ?_
specialize hg_upper' 0
rw [norm_zero] at hg_upper'
exact nonneg_of_mul_nonneg_left hg_upper' (by positivity)
let k' := kg * (k + l * n)
use Finset.Iic (k', n), (1 + Cg) ^ (k + l * n) * ((C + 1) ^ n * n ! * 2 ^ k'), by positivity
intro f x
let seminorm_f := ((Finset.Iic (k', n)).sup (schwartzSeminormFamily 𝕜 _ _)) f
have hg_upper'' : (1 + ‖x‖) ^ (k + l * n) ≤ (1 + Cg) ^ (k + l * n) * (1 + ‖g x‖) ^ k' :=
by
rw [pow_mul, ← mul_pow]
gcongr
rw [add_mul]
refine add_le_add ?_ (hg_upper' x)
nth_rw 1 [← one_mul (1 : ℝ)]
gcongr
apply one_le_pow₀
simp only [le_add_iff_nonneg_right, norm_nonneg]
have hbound (i) (hi : i ≤ n) : ‖iteratedFDeriv ℝ i f (g x)‖ ≤ 2 ^ k' * seminorm_f / (1 + ‖g x‖) ^ k' :=
by
have hpos : 0 < (1 + ‖g x‖) ^ k' := by positivity
rw [le_div_iff₀' hpos]
change i ≤ (k', n).snd at hi
exact one_add_le_sup_seminorm_apply le_rfl hi _ _
have hgrowth' (N : ℕ) (hN₁ : 1 ≤ N) (hN₂ : N ≤ n) : ‖iteratedFDeriv ℝ N g x‖ ≤ ((C + 1) * (1 + ‖x‖) ^ l) ^ N :=
by
refine (hgrowth N hN₂ x).trans ?_
rw [mul_pow]
have hN₁' := (lt_of_lt_of_le zero_lt_one hN₁).ne'
gcongr
· exact le_trans (by simp) (le_self_pow₀ (by simp [hC]) hN₁')
· refine le_self_pow₀ (one_le_pow₀ ?_) hN₁'
simp only [le_add_iff_nonneg_right, norm_nonneg]
have := norm_iteratedFDeriv_comp_le (f.smooth ⊤) hg.1 (mod_cast le_top) x hbound hgrowth'
have hxk : ‖x‖ ^ k ≤ (1 + ‖x‖) ^ k :=
pow_le_pow_left₀ (norm_nonneg _) (by simp only [zero_le_one, le_add_iff_nonneg_left]) _
grw [hxk, this]
have rearrange :
(1 + ‖x‖) ^ k * (n ! * (2 ^ k' * seminorm_f / (1 + ‖g x‖) ^ k') * ((C + 1) * (1 + ‖x‖) ^ l) ^ n) =
(1 + ‖x‖) ^ (k + l * n) / (1 + ‖g x‖) ^ k' * ((C + 1) ^ n * n ! * 2 ^ k' * seminorm_f) :=
by
rw [mul_pow, pow_add, ← pow_mul]
ring
rw [rearrange]
have hgxk' : 0 < (1 + ‖g x‖) ^ k' := by positivity
rw [← div_le_iff₀ hgxk'] at hg_upper''
grw [hg_upper'', ← mul_assoc]
