English
There is a construction mkCLM that yields a continuous semilinear map between Schwartz spaces given a suitable A and growth bounds.
Русский
Существует конструктор mkCLM, который даёт непрерывное полупространство между пространствами Шварца, если задано A и ограничения роста.
LaTeX
$$$mkCLM(A,hadd,hsmul,hsmooth,hbound): 𝓢(D,E) →SL[σ] 𝓢(F,G)$ with continuity bound.$$
Lean4
/-- The map `f ↦ (x ↦ B (f x) (g x))` as a continuous `𝕜`-linear map on Schwartz space,
where `B` is a continuous `𝕜`-linear map and `g` is a function of temperate growth. -/
def bilinLeftCLM (B : E →L[𝕜] F →L[𝕜] G) {g : D → F} (hg : g.HasTemperateGrowth) : 𝓢(D, E) →L[𝕜] 𝓢(D, G) :=
by
refine
mkCLM (fun f x => B (f x) (g x)) (fun _ _ _ => by simp) (fun _ _ _ => by simp)
(fun f => (B.bilinearRestrictScalars ℝ).isBoundedBilinearMap.contDiff.comp ((f.smooth ⊤).prodMk hg.1)) ?_
rintro ⟨k, n⟩
rcases hg.norm_iteratedFDeriv_le_uniform_aux n with ⟨l, C, hC, hgrowth⟩
use Finset.Iic (l + k, n), ‖B‖ * ((n : ℝ) + (1 : ℝ)) * n.choose (n / 2) * (C * 2 ^ (l + k)), by positivity
intro f x
have hxk : 0 ≤ ‖x‖ ^ k := by positivity
simp_rw [← ContinuousLinearMap.bilinearRestrictScalars_apply_apply ℝ B]
have hnorm_mul :=
ContinuousLinearMap.norm_iteratedFDeriv_le_of_bilinear (B.bilinearRestrictScalars ℝ) (f.smooth ⊤) hg.1 x (n := n)
(mod_cast le_top)
grw [hnorm_mul]
rw [ContinuousLinearMap.norm_bilinearRestrictScalars]
move_mul [← ‖B‖]
simp_rw [mul_assoc ‖B‖]
gcongr _ * ?_
rw [Finset.mul_sum]
have : (∑ _x ∈ Finset.range (n + 1), (1 : ℝ)) = n + 1 := by simp
simp_rw [mul_assoc ((n : ℝ) + 1)]
rw [← this, Finset.sum_mul]
refine Finset.sum_le_sum fun i hi => ?_
simp only [one_mul]
move_mul [(Nat.choose n i : ℝ), (Nat.choose n (n / 2) : ℝ)]
gcongr ?_ * ?_
swap
· norm_cast
exact i.choose_le_middle n
specialize hgrowth (n - i) (by simp only [tsub_le_self]) x
grw [hgrowth]
move_mul [C]
gcongr ?_ * C
rw [Finset.mem_range_succ_iff] at hi
change i ≤ (l + k, n).snd at hi
refine le_trans ?_ (one_add_le_sup_seminorm_apply le_rfl hi f x)
rw [pow_add]
move_mul [(1 + ‖x‖) ^ l]
gcongr
simp
