isTheta_principal — Mathlib

English

If f =Θ[l] g, then f ∘ Prod.snd = Θ[l' ×ˢ l] g ∘ Prod.snd.

Русский

Если f =Θ[l] g, то f ∘ Prod.snd = Θ[l' ×ˢ l] g ∘ Prod.snd.

LaTeX

$$$\forall f,g:\; f =Θ[l] g \Rightarrow (f \circ Prod.snd) =Θ[l' \timesˢ l] (g \circ Prod.snd)$$$

Lean4

protected theorem isTheta_principal (hf : ContinuousOn f s) (hs : IsCompact s) (hc : ‖c‖ ≠ 0) (hC : ∀ i ∈ s, f i ≠ 0) :
    f =Θ[𝓟 s] fun _ => c :=
  ⟨hf.isBigO_principal hs hc, hf.isBigO_rev_principal hs hC c⟩

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