English
Let f: ℝ → F be C^1 with compact support in a normed space F. Then for every x ∈ ℝ, the norm of f(x) is bounded by the integral of the norm of its derivative up to x:
Русский
Пусть f: ℝ → F имеет производную и компактную опору; тогда для каждого x ∈ ℝ выполняется неравенство
LaTeX
$$$$ \|f(x)\|_F \le \int_{y \in Iic x} \|\ deriv f(y)\|_F \, dy, \quad \forall x \in \mathbb{R}. $$$$
Lean4
theorem _root_.HasCompactSupport.enorm_le_lintegral_Ici_deriv {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
{f : ℝ → F} (hf : ContDiff ℝ 1 f) (h'f : HasCompactSupport f) (x : ℝ) : ‖f x‖ₑ ≤ ∫⁻ y in Iic x, ‖deriv f y‖ₑ :=
by
let I : F →L[ℝ] Completion F := Completion.toComplL
let f' : ℝ → Completion F := I ∘ f
have hf' : ContDiff ℝ 1 f' := hf.continuousLinearMap_comp I
have h'f' : HasCompactSupport f' := h'f.comp_left rfl
have : ‖f' x‖ₑ ≤ ∫⁻ y in Iic x, ‖deriv f' y‖ₑ :=
by
rw [← HasCompactSupport.integral_Iic_deriv_eq hf' h'f' x]
exact enorm_integral_le_lintegral_enorm _
convert this with y
· simp [f', I, Completion.enorm_coe]
· rw [fderiv_comp_deriv _ I.differentiableAt (hf.differentiable le_rfl _)]
simp only [ContinuousLinearMap.fderiv]
simp [I]
