Source indexedtheorem · leanprover/lean4:v4.32.0

ContinuousOn.const_isBigOWithUniformlyOn_isCompact_rev

PrimeNumberTheoremAnd.Mathlib.Analysis.Asymptotics.Uniformly · PrimeNumberTheoremAnd/Mathlib/Analysis/Asymptotics/Uniformly.lean:131 to 144

Source documentation

A family of constant functions f (i, x) = C i is uniformly bounded below 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_rev
    (hf : ContinuousOn C s) (hs : IsCompact s) (hC : ∀ i ∈ s, C i ≠ 0) (l : Filter α) :
    IsBigOWith (‖c‖ / sInf (norm '' (C '' s))) (𝓟 s ×ˢ l)
    (fun _ => c) fun (i, _x) ↦ C i

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem _root_.ContinuousOn.const_isBigOWithUniformlyOn_isCompact_rev    (hf : ContinuousOn C s) (hs : IsCompact s) (hC : ∀ i ∈ s, C i ≠ 0) (l : Filter α) :    IsBigOWith (‖c‖ / sInf (norm '' (C '' s))) (𝓟 s ×ˢ l)    (fun _ => c) fun (i, _x) ↦ C i := 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  · rewrite [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.1, hx.1⟩    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.1    obtain ⟨_, ⟨x, hx, hCx⟩, hnormCx⟩ := hs.sInf_mem h_sInf.nonempty    rewrite [← hnormCx, ← hCx]    exact (norm_ne_zero_iff.mpr (hC x hx)).symm.lt_of_le (norm_nonneg _)