Source indexedtheorem · leanprover/lean4:v4.32.0

ContinuousOn.const_isBigOWithUniformlyOn_isCompact

PrimeNumberTheoremAnd.Mathlib.Analysis.Asymptotics.Uniformly · PrimeNumberTheoremAnd/Mathlib/Analysis/Asymptotics/Uniformly.lean:105 to 114

Source documentation

A family of constant functions f (i, x) = C i is uniformly bounded w.r.t. s by ⨆ i ∈ s, ‖C i‖, if s is compact and C is continuous.

Exact Lean statement

theorem _root_.ContinuousOn.const_isBigOWithUniformlyOn_isCompact
    (hf : ContinuousOn C s) (hs : IsCompact s) (hc : ‖c‖ ≠ 0) (l : Filter α) :
    IsBigOWith (sSup (norm '' (C '' s)) / ‖c‖) (𝓟 s ×ˢ l)
    (fun (i, _x) ↦ C i) fun _ => c

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem _root_.ContinuousOn.const_isBigOWithUniformlyOn_isCompact    (hf : ContinuousOn C s) (hs : IsCompact s) (hc : ‖c‖ ≠ 0) (l : Filter α) :    IsBigOWith (sSup (norm '' (C '' s)) / ‖c‖) (𝓟 s ×ˢ l)    (fun (i, _x) ↦ C i) fun _ => c := by  refine isBigOWith_iff.mpr <| eventually_of_mem ?_ (fun x hx ↦ ?_) (U := s ×ˢ Set.univ)  · exact prod_mem_prod (mem_principal_self s) univ_mem  · rw [div_mul_cancel₀ _ hc]    replace hs := hs.image_of_continuousOn hf |>.image continuous_norm    have h_sSup := hs.isLUB_sSup <| Set.image_nonempty.mpr <| Set.image_nonempty.mpr ⟨x.1, hx.1⟩    exact h_sSup.1 <| Set.mem_image_of_mem _ <| Set.mem_image_of_mem _ hx.1