lipschitzWith_of_hasCompactSupport

English

A C^1 function with compact support is Lipschitz.

Русский

Fункция C^1 с компактной опорой является Lipschitz.

LaTeX

$$$$\exists C,\ LipschitzWith C f.$$$$

Lean4

/-- A `C^1` function with compact support is Lipschitz. -/
theorem lipschitzWith_of_hasCompactSupport {f : E' → F'} (hf : HasCompactSupport f) (h'f : ContDiff 𝕂 n f)
    (hn : 1 ≤ n) : ∃ C, LipschitzWith C f :=
  by
  obtain ⟨C, hC⟩ := (hf.fderiv 𝕂).exists_bound_of_continuous (h'f.continuous_fderiv hn)
  refine ⟨⟨max C 0, le_max_right _ _⟩, ?_⟩
  apply lipschitzWith_of_nnnorm_fderiv_le (h'f.differentiable hn) (fun x ↦ ?_)
  simp [← NNReal.coe_le_coe, hC x]

Похожие утверждения