English
If f is continuous on s and hC: ∀ i ∈ s, f(i) ≠ 0, then there exists c such that IsBigOWith(∥c∥/sInf(‖f‖''(f''s))) with principal filter bounds f by c on s.
Русский
Если f непрерывна на s и ∀ i ∈ s f(i) ≠ 0, то существует c, удовлетворяющее IsBigOWith(∥c∥/sInf(‖f‖ по s) c, f, и т. д.
LaTeX
$$$ \\text{ContinuousOn } f s \\Rightarrow \\text{IsCompact } s \\Rightarrow \\forall i\\in s, f(i) \\neq 0 \\Rightarrow \\text{IsBigOWith}( \\frac{\\|c\\|}{\\mathrm{sInf}(\\|f\\|''(f''s))} ) (\\mathcal{P} s) f (\\lambda _ => c) $$$
Lean4
protected theorem isBigOWith_rev_principal (hf : ContinuousOn f s) (hs : IsCompact s) (hC : ∀ i ∈ s, f i ≠ 0) (c : F) :
IsBigOWith (‖c‖ / sInf (Norm.norm '' (f '' s))) (𝓟 s) (fun _ => c) f :=
by
refine isBigOWith_principal.mpr fun x hx ↦ ?_
rw [mul_comm_div]
replace hs := hs.image_of_continuousOn hf |>.image continuous_norm
have h_sInf := hs.isGLB_sInf <| Set.image_nonempty.mpr <| Set.image_nonempty.mpr ⟨x, hx⟩
refine
le_mul_of_one_le_right (norm_nonneg c) <|
(one_le_div ?_).mpr <| h_sInf.1 <| Set.mem_image_of_mem _ <| Set.mem_image_of_mem _ hx
obtain ⟨_, ⟨x, hx, hCx⟩, hnormCx⟩ := hs.sInf_mem h_sInf.nonempty
rw [← hnormCx, ← hCx]
exact (norm_ne_zero_iff.mpr (hC x hx)).symm.lt_of_le (norm_nonneg _)
