English
If f is continuous on a compact set s and c ≠ 0, then f is bounded by a multiple of c on s, i.e., IsBigOWith constant bound relative to the principal filter on s.
Русский
Если f непрерывна на компактном множестве s и c ≠ 0, то f ограничена сверху на s отношением к постоянной f, то есть IsBigOWith с константой, равной sSupNorm(c).
LaTeX
$$$ \\text{ContinuousOn } f s \\Rightarrow \\text{IsCompact } s \\Rightarrow \\|c\\| \\neq 0 \\Rightarrow IsBigOWith \\left( \\frac{\\mathrm{sSup}(\\|\\cdot\\|) \\!''(f''s)}{\\|c\\|} \\right) (\\mathcal{P} s) f (\\lambda _ => c)$$$
Lean4
protected theorem isBigOWith_principal (hf : ContinuousOn f s) (hs : IsCompact s) (hc : ‖c‖ ≠ 0) :
IsBigOWith (sSup (Norm.norm '' (f '' s)) / ‖c‖) (𝓟 s) f fun _ => c :=
by
rw [isBigOWith_principal, div_mul_cancel₀ _ hc]
exact fun x hx ↦
hs.image_of_continuousOn hf |>.image continuous_norm |>.isLUB_sSup
(Set.image_nonempty.mpr <| Set.image_nonempty.mpr ⟨x, hx⟩) |>.left <|
Set.mem_image_of_mem _ <| Set.mem_image_of_mem _ hx
