Asymptotic equivalence up to a constant

In this file we prove basic properties of the equivalence relation given by f =Θ[l] g ↔ f =O[l] g ∧ g =O[l] f.

theorem Asymptotics.isTheta_refl {α : Type u_1} {E : Type u_3} [Norm E] (f : α → E) (l : Filter α) : f =Θ[l] f

theorem Asymptotics.isTheta_rfl {α : Type u_1} {E : Type u_3} [Norm E] {f : α → E} {l : Filter α} : f =Θ[l] f

theorem Asymptotics.IsTheta.symm {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : α → E} {g : α → F} {l : Filter α} (h : f =Θ[l] g) : g =Θ[l] f

theorem Asymptotics.isTheta_comm {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : α → E} {g : α → F} {l : Filter α} : f =Θ[l] g ↔ g =Θ[l] f

theorem Asymptotics.IsTheta.trans {α : Type u_1} {E : Type u_3} {G : Type u_5} {F' : Type u_7} [Norm E] [Norm G] [SeminormedAddCommGroup F'] {l : Filter α} {f : α → E} {g : α → F'} {k : α → G} (h₁ : f =Θ[l] g) (h₂ : g =Θ[l] k) : f =Θ[l] k

@[implicit_reducible]

instance Asymptotics.instTransForallIsTheta {α : Type u_1} {E : Type u_3} {G : Type u_5} {F' : Type u_7} [Norm E] [Norm G] [SeminormedAddCommGroup F'] {l : Filter α} : Trans (IsTheta l) (IsTheta l) (IsTheta l)

Equations

• Asymptotics.instTransForallIsTheta = { trans := ⋯ }

theorem Asymptotics.IsBigO.trans_isTheta {α : Type u_1} {E : Type u_3} {G : Type u_5} {F' : Type u_7} [Norm E] [Norm G] [SeminormedAddCommGroup F'] {l : Filter α} {f : α → E} {g : α → F'} {k : α → G} (h₁ : f =O[l] g) (h₂ : g =Θ[l] k) : f =O[l] k

@[implicit_reducible]

instance Asymptotics.instTransForallIsBigOIsTheta {α : Type u_1} {E : Type u_3} {G : Type u_5} {F' : Type u_7} [Norm E] [Norm G] [SeminormedAddCommGroup F'] {l : Filter α} : Trans (IsBigO l) (IsTheta l) (IsBigO l)

Equations

• Asymptotics.instTransForallIsBigOIsTheta = { trans := ⋯ }

theorem Asymptotics.IsTheta.trans_isBigO {α : Type u_1} {E : Type u_3} {G : Type u_5} {F' : Type u_7} [Norm E] [Norm G] [SeminormedAddCommGroup F'] {l : Filter α} {f : α → E} {g : α → F'} {k : α → G} (h₁ : f =Θ[l] g) (h₂ : g =O[l] k) : f =O[l] k

@[implicit_reducible]

instance Asymptotics.instTransForallIsThetaIsBigO {α : Type u_1} {E : Type u_3} {G : Type u_5} {F' : Type u_7} [Norm E] [Norm G] [SeminormedAddCommGroup F'] {l : Filter α} : Trans (IsTheta l) (IsBigO l) (IsBigO l)

Equations

• Asymptotics.instTransForallIsThetaIsBigO = { trans := ⋯ }

theorem Asymptotics.IsLittleO.trans_isTheta {α : Type u_1} {E : Type u_3} {F : Type u_4} {G' : Type u_8} [Norm E] [Norm F] [SeminormedAddCommGroup G'] {l : Filter α} {f : α → E} {g : α → F} {k : α → G'} (h₁ : f =o[l] g) (h₂ : g =Θ[l] k) : f =o[l] k

@[implicit_reducible]

instance Asymptotics.instTransForallIsLittleOIsTheta {α : Type u_1} {E : Type u_3} {F' : Type u_7} {G' : Type u_8} [Norm E] [SeminormedAddCommGroup F'] [SeminormedAddCommGroup G'] {l : Filter α} : Trans (IsLittleO l) (IsTheta l) (IsLittleO l)

Equations

• Asymptotics.instTransForallIsLittleOIsTheta = { trans := ⋯ }

theorem Asymptotics.IsTheta.trans_isLittleO {α : Type u_1} {E : Type u_3} {G : Type u_5} {F' : Type u_7} [Norm E] [Norm G] [SeminormedAddCommGroup F'] {l : Filter α} {f : α → E} {g : α → F'} {k : α → G} (h₁ : f =Θ[l] g) (h₂ : g =o[l] k) : f =o[l] k

@[implicit_reducible]

instance Asymptotics.instTransForallIsThetaIsLittleO {α : Type u_1} {E : Type u_3} {G : Type u_5} {F' : Type u_7} [Norm E] [Norm G] [SeminormedAddCommGroup F'] {l : Filter α} : Trans (IsTheta l) (IsLittleO l) (IsLittleO l)

Equations

• Asymptotics.instTransForallIsThetaIsLittleO = { trans := ⋯ }

theorem Asymptotics.IsTheta.trans_eventuallyEq {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {l : Filter α} {f : α → E} {g₁ g₂ : α → F} (h : f =Θ[l] g₁) (hg : g₁ =ᶠ[l] g₂) : f =Θ[l] g₂

@[implicit_reducible]

instance Asymptotics.instTransForallIsThetaEventuallyEq {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {l : Filter α} : Trans (IsTheta l) l.EventuallyEq (IsTheta l)

Equations

• Asymptotics.instTransForallIsThetaEventuallyEq = { trans := ⋯ }

theorem Filter.EventuallyEq.trans_isTheta {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {l : Filter α} {f₁ f₂ : α → E} {g : α → F} (hf : f₁ =ᶠ[l] f₂) (h : f₂ =Θ[l] g) : f₁ =Θ[l] g

@[implicit_reducible]

instance Asymptotics.instTransForallEventuallyEqIsTheta {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {l : Filter α} : Trans l.EventuallyEq (IsTheta l) (IsTheta l)

Equations

• Asymptotics.instTransForallEventuallyEqIsTheta = { trans := ⋯ }

theorem Filter.EventuallyEq.isTheta {α : Type u_1} {E : Type u_3} [Norm E] {l : Filter α} {f g : α → E} (h : f =ᶠ[l] g) : f =Θ[l] g

@[simp]

theorem Asymptotics.isTheta_bot {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : α → E} {g : α → F} : f =Θ[⊥] g

@[simp]

theorem Asymptotics.isTheta_norm_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] [SeminormedAddCommGroup E'] {g : α → F} {f' : α → E'} {l : Filter α} : (fun (x : α) => ‖f' x‖) =Θ[l] g ↔ f' =Θ[l] g

@[simp]

theorem Asymptotics.isTheta_norm_right {α : Type u_1} {E : Type u_3} {F' : Type u_7} [Norm E] [SeminormedAddCommGroup F'] {f : α → E} {g' : α → F'} {l : Filter α} : (f =Θ[l] fun (x : α) => ‖g' x‖) ↔ f =Θ[l] g'

theorem Asymptotics.IsTheta.of_norm_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] [SeminormedAddCommGroup E'] {g : α → F} {f' : α → E'} {l : Filter α} : (fun (x : α) => ‖f' x‖) =Θ[l] g → f' =Θ[l] g

Alias of the forward direction of Asymptotics.isTheta_norm_left.

theorem Asymptotics.IsTheta.norm_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] [SeminormedAddCommGroup E'] {g : α → F} {f' : α → E'} {l : Filter α} : f' =Θ[l] g → (fun (x : α) => ‖f' x‖) =Θ[l] g

Alias of the reverse direction of Asymptotics.isTheta_norm_left.

theorem Asymptotics.IsTheta.norm_right {α : Type u_1} {E : Type u_3} {F' : Type u_7} [Norm E] [SeminormedAddCommGroup F'] {f : α → E} {g' : α → F'} {l : Filter α} : f =Θ[l] g' → f =Θ[l] fun (x : α) => ‖g' x‖

Alias of the reverse direction of Asymptotics.isTheta_norm_right.

theorem Asymptotics.IsTheta.of_norm_right {α : Type u_1} {E : Type u_3} {F' : Type u_7} [Norm E] [SeminormedAddCommGroup F'] {f : α → E} {g' : α → F'} {l : Filter α} : (f =Θ[l] fun (x : α) => ‖g' x‖) → f =Θ[l] g'

Alias of the forward direction of Asymptotics.isTheta_norm_right.

theorem Asymptotics.IsTheta.of_norm_eventuallyEq_norm {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : α → E} {g : α → F} {l : Filter α} (h : (fun (x : α) => ‖f x‖) =ᶠ[l] fun (x : α) => ‖g x‖) : f =Θ[l] g

theorem Asymptotics.IsTheta.of_norm_eventuallyEq {α : Type u_1} {E' : Type u_6} [SeminormedAddCommGroup E'] {f' : α → E'} {l : Filter α} {g : α → ℝ} (h : (fun (x : α) => ‖f' x‖) =ᶠ[l] g) : f' =Θ[l] g

theorem Asymptotics.IsTheta.isLittleO_congr_left {α : Type u_1} {G : Type u_5} {E' : Type u_6} {F' : Type u_7} [Norm G] [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] {k : α → G} {f' : α → E'} {g' : α → F'} {l : Filter α} (h : f' =Θ[l] g') : f' =o[l] k ↔ g' =o[l] k

theorem Asymptotics.IsTheta.isLittleO_congr_right {α : Type u_1} {E : Type u_3} {F' : Type u_7} {G' : Type u_8} [Norm E] [SeminormedAddCommGroup F'] [SeminormedAddCommGroup G'] {f : α → E} {g' : α → F'} {k' : α → G'} {l : Filter α} (h : g' =Θ[l] k') : f =o[l] g' ↔ f =o[l] k'

theorem Asymptotics.IsTheta.isBigO_congr_left {α : Type u_1} {G : Type u_5} {E' : Type u_6} {F' : Type u_7} [Norm G] [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] {k : α → G} {f' : α → E'} {g' : α → F'} {l : Filter α} (h : f' =Θ[l] g') : f' =O[l] k ↔ g' =O[l] k

theorem Asymptotics.IsTheta.isBigO_congr_right {α : Type u_1} {E : Type u_3} {F' : Type u_7} {G' : Type u_8} [Norm E] [SeminormedAddCommGroup F'] [SeminormedAddCommGroup G'] {f : α → E} {g' : α → F'} {k' : α → G'} {l : Filter α} (h : g' =Θ[l] k') : f =O[l] g' ↔ f =O[l] k'

theorem Asymptotics.IsTheta.isTheta_congr_left {α : Type u_1} {G : Type u_5} {E' : Type u_6} {F' : Type u_7} [Norm G] [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] {k : α → G} {f' : α → E'} {g' : α → F'} {l : Filter α} (h : f' =Θ[l] g') : f' =Θ[l] k ↔ g' =Θ[l] k

theorem Asymptotics.IsTheta.isTheta_congr_right {α : Type u_1} {G : Type u_5} {E' : Type u_6} {F' : Type u_7} [Norm G] [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] {k : α → G} {f' : α → E'} {g' : α → F'} {l : Filter α} (h : f' =Θ[l] g') : k =Θ[l] f' ↔ k =Θ[l] g'

theorem Asymptotics.IsTheta.mono {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : α → E} {g : α → F} {l l' : Filter α} (h : f =Θ[l] g) (hl : l' ≤ l) : f =Θ[l'] g

theorem Asymptotics.IsTheta.sup {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] {f' : α → E'} {g' : α → F'} {l l' : Filter α} (h : f' =Θ[l] g') (h' : f' =Θ[l'] g') : f' =Θ[l ⊔ l'] g'

@[simp]

theorem Asymptotics.isTheta_sup {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] {f' : α → E'} {g' : α → F'} {l l' : Filter α} : f' =Θ[l ⊔ l'] g' ↔ f' =Θ[l] g' ∧ f' =Θ[l'] g'

theorem Asymptotics.IsTheta.eq_zero_iff {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} [NormedAddCommGroup E''] [NormedAddCommGroup F''] {f'' : α → E''} {g'' : α → F''} {l : Filter α} (h : f'' =Θ[l] g'') : ∀ᶠ (x : α) in l, f'' x = 0 ↔ g'' x = 0

theorem Asymptotics.IsTheta.tendsto_zero_iff {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} [NormedAddCommGroup E''] [NormedAddCommGroup F''] {f'' : α → E''} {g'' : α → F''} {l : Filter α} (h : f'' =Θ[l] g'') : Filter.Tendsto f'' l (nhds 0) ↔ Filter.Tendsto g'' l (nhds 0)

theorem Asymptotics.IsTheta.tendsto_norm_atTop_iff {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] {f' : α → E'} {g' : α → F'} {l : Filter α} (h : f' =Θ[l] g') : Filter.Tendsto (norm ∘ f') l Filter.atTop ↔ Filter.Tendsto (norm ∘ g') l Filter.atTop

theorem Asymptotics.IsTheta.isBoundedUnder_le_iff {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] {f' : α → E'} {g' : α → F'} {l : Filter α} (h : f' =Θ[l] g') : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) l (norm ∘ f') ↔ Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) l (norm ∘ g')

theorem Asymptotics.IsTheta.smul {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {𝕜 : Type u_14} {𝕜' : Type u_15} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] [NormedField 𝕜] [NormedField 𝕜'] {l : Filter α} [NormedSpace 𝕜 E'] [NormedSpace 𝕜' F'] {f₁ : α → 𝕜} {f₂ : α → 𝕜'} {g₁ : α → E'} {g₂ : α → F'} (hf : f₁ =Θ[l] f₂) (hg : g₁ =Θ[l] g₂) : (fun (x : α) => f₁ x • g₁ x) =Θ[l] fun (x : α) => f₂ x • g₂ x

theorem Asymptotics.IsTheta.mul {α : Type u_1} {𝕜 : Type u_14} {𝕜' : Type u_15} [NormedField 𝕜] [NormedField 𝕜'] {l : Filter α} {f₁ f₂ : α → 𝕜} {g₁ g₂ : α → 𝕜'} (h₁ : f₁ =Θ[l] g₁) (h₂ : f₂ =Θ[l] g₂) : (fun (x : α) => f₁ x * f₂ x) =Θ[l] fun (x : α) => g₁ x * g₂ x

theorem Asymptotics.IsTheta.listProd {α : Type u_1} {𝕜 : Type u_14} {𝕜' : Type u_15} [NormedField 𝕜] [NormedField 𝕜'] {l : Filter α} {ι : Type u_16} {L : List ι} {f : ι → α → 𝕜} {g : ι → α → 𝕜'} (h : ∀ i ∈ L, f i =Θ[l] g i) : (fun (x : α) => (List.map (fun (x_1 : ι) => f x_1 x) L).prod) =Θ[l] fun (x : α) => (List.map (fun (x_1 : ι) => g x_1 x) L).prod

theorem Asymptotics.IsTheta.multisetProd {α : Type u_1} {𝕜 : Type u_14} {𝕜' : Type u_15} [NormedField 𝕜] [NormedField 𝕜'] {l : Filter α} {ι : Type u_16} {s : Multiset ι} {f : ι → α → 𝕜} {g : ι → α → 𝕜'} (h : ∀ i ∈ s, f i =Θ[l] g i) : (fun (x : α) => (Multiset.map (fun (x_1 : ι) => f x_1 x) s).prod) =Θ[l] fun (x : α) => (Multiset.map (fun (x_1 : ι) => g x_1 x) s).prod

theorem Asymptotics.IsTheta.finsetProd {α : Type u_1} {𝕜 : Type u_14} {𝕜' : Type u_15} [NormedField 𝕜] [NormedField 𝕜'] {l : Filter α} {ι : Type u_16} {s : Finset ι} {f : ι → α → 𝕜} {g : ι → α → 𝕜'} (h : ∀ i ∈ s, f i =Θ[l] g i) : (fun (x : α) => ∏ i ∈ s, f i x) =Θ[l] fun (x : α) => ∏ i ∈ s, g i x

theorem Asymptotics.IsTheta.inv {α : Type u_1} {𝕜 : Type u_14} {𝕜' : Type u_15} [NormedField 𝕜] [NormedField 𝕜'] {l : Filter α} {f : α → 𝕜} {g : α → 𝕜'} (h : f =Θ[l] g) : (fun (x : α) => (f x)⁻¹) =Θ[l] fun (x : α) => (g x)⁻¹

@[simp]

theorem Asymptotics.isTheta_inv {α : Type u_1} {𝕜 : Type u_14} {𝕜' : Type u_15} [NormedField 𝕜] [NormedField 𝕜'] {l : Filter α} {f : α → 𝕜} {g : α → 𝕜'} : ((fun (x : α) => (f x)⁻¹) =Θ[l] fun (x : α) => (g x)⁻¹) ↔ f =Θ[l] g

theorem Asymptotics.IsTheta.div {α : Type u_1} {𝕜 : Type u_14} {𝕜' : Type u_15} [NormedField 𝕜] [NormedField 𝕜'] {l : Filter α} {f₁ f₂ : α → 𝕜} {g₁ g₂ : α → 𝕜'} (h₁ : f₁ =Θ[l] g₁) (h₂ : f₂ =Θ[l] g₂) : (fun (x : α) => f₁ x / f₂ x) =Θ[l] fun (x : α) => g₁ x / g₂ x

theorem Asymptotics.IsTheta.pow {α : Type u_1} {𝕜 : Type u_14} {𝕜' : Type u_15} [NormedField 𝕜] [NormedField 𝕜'] {l : Filter α} {f : α → 𝕜} {g : α → 𝕜'} (h : f =Θ[l] g) (n : ℕ) : (fun (x : α) => f x ^ n) =Θ[l] fun (x : α) => g x ^ n

theorem Asymptotics.IsTheta.zpow {α : Type u_1} {𝕜 : Type u_14} {𝕜' : Type u_15} [NormedField 𝕜] [NormedField 𝕜'] {l : Filter α} {f : α → 𝕜} {g : α → 𝕜'} (h : f =Θ[l] g) (n : ℤ) : (fun (x : α) => f x ^ n) =Θ[l] fun (x : α) => g x ^ n

theorem Asymptotics.isTheta_const_const {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} [NormedAddCommGroup E''] [NormedAddCommGroup F''] {l : Filter α} {c₁ : E''} {c₂ : F''} (h₁ : c₁ ≠ 0) (h₂ : c₂ ≠ 0) : (fun (x : α) => c₁) =Θ[l] fun (x : α) => c₂

@[simp]

theorem Asymptotics.isTheta_const_const_iff {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} [NormedAddCommGroup E''] [NormedAddCommGroup F''] {l : Filter α} [l.NeBot] {c₁ : E''} {c₂ : F''} : ((fun (x : α) => c₁) =Θ[l] fun (x : α) => c₂) ↔ (c₁ = 0 ↔ c₂ = 0)

@[simp]

theorem Asymptotics.isTheta_zero_left {α : Type u_1} {E' : Type u_6} {F'' : Type u_10} [SeminormedAddCommGroup E'] [NormedAddCommGroup F''] {g'' : α → F''} {l : Filter α} : (fun (x : α) => 0) =Θ[l] g'' ↔ g'' =ᶠ[l] 0

@[simp]

theorem Asymptotics.isTheta_zero_right {α : Type u_1} {F' : Type u_7} {E'' : Type u_9} [SeminormedAddCommGroup F'] [NormedAddCommGroup E''] {f'' : α → E''} {l : Filter α} : (f'' =Θ[l] fun (x : α) => 0) ↔ f'' =ᶠ[l] 0

theorem Asymptotics.isTheta_const_smul_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} {𝕜 : Type u_14} [Norm F] [SeminormedAddCommGroup E'] [NormedField 𝕜] {g : α → F} {f' : α → E'} {l : Filter α} [NormedSpace 𝕜 E'] {c : 𝕜} (hc : c ≠ 0) : (fun (x : α) => c • f' x) =Θ[l] g ↔ f' =Θ[l] g

theorem Asymptotics.IsTheta.of_const_smul_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} {𝕜 : Type u_14} [Norm F] [SeminormedAddCommGroup E'] [NormedField 𝕜] {g : α → F} {f' : α → E'} {l : Filter α} [NormedSpace 𝕜 E'] {c : 𝕜} (hc : c ≠ 0) : (fun (x : α) => c • f' x) =Θ[l] g → f' =Θ[l] g

Alias of the forward direction of Asymptotics.isTheta_const_smul_left.

theorem Asymptotics.IsTheta.const_smul_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} {𝕜 : Type u_14} [Norm F] [SeminormedAddCommGroup E'] [NormedField 𝕜] {g : α → F} {f' : α → E'} {l : Filter α} [NormedSpace 𝕜 E'] {c : 𝕜} (hc : c ≠ 0) : f' =Θ[l] g → (fun (x : α) => c • f' x) =Θ[l] g

Alias of the reverse direction of Asymptotics.isTheta_const_smul_left.

theorem Asymptotics.isTheta_const_smul_right {α : Type u_1} {E : Type u_3} {F' : Type u_7} {𝕜 : Type u_14} [Norm E] [SeminormedAddCommGroup F'] [NormedField 𝕜] {f : α → E} {g' : α → F'} {l : Filter α} [NormedSpace 𝕜 F'] {c : 𝕜} (hc : c ≠ 0) : (f =Θ[l] fun (x : α) => c • g' x) ↔ f =Θ[l] g'

theorem Asymptotics.IsTheta.of_const_smul_right {α : Type u_1} {E : Type u_3} {F' : Type u_7} {𝕜 : Type u_14} [Norm E] [SeminormedAddCommGroup F'] [NormedField 𝕜] {f : α → E} {g' : α → F'} {l : Filter α} [NormedSpace 𝕜 F'] {c : 𝕜} (hc : c ≠ 0) : (f =Θ[l] fun (x : α) => c • g' x) → f =Θ[l] g'

Alias of the forward direction of Asymptotics.isTheta_const_smul_right.

theorem Asymptotics.IsTheta.const_smul_right {α : Type u_1} {E : Type u_3} {F' : Type u_7} {𝕜 : Type u_14} [Norm E] [SeminormedAddCommGroup F'] [NormedField 𝕜] {f : α → E} {g' : α → F'} {l : Filter α} [NormedSpace 𝕜 F'] {c : 𝕜} (hc : c ≠ 0) : f =Θ[l] g' → f =Θ[l] fun (x : α) => c • g' x

Alias of the reverse direction of Asymptotics.isTheta_const_smul_right.

theorem Asymptotics.isTheta_const_mul_left {α : Type u_1} {F : Type u_4} {𝕜 : Type u_14} [Norm F] [NormedField 𝕜] {g : α → F} {l : Filter α} {c : 𝕜} {f : α → 𝕜} (hc : c ≠ 0) : (fun (x : α) => c * f x) =Θ[l] g ↔ f =Θ[l] g

theorem Asymptotics.IsTheta.const_mul_left {α : Type u_1} {F : Type u_4} {𝕜 : Type u_14} [Norm F] [NormedField 𝕜] {g : α → F} {l : Filter α} {c : 𝕜} {f : α → 𝕜} (hc : c ≠ 0) : f =Θ[l] g → (fun (x : α) => c * f x) =Θ[l] g

Alias of the reverse direction of Asymptotics.isTheta_const_mul_left.

theorem Asymptotics.IsTheta.of_const_mul_left {α : Type u_1} {F : Type u_4} {𝕜 : Type u_14} [Norm F] [NormedField 𝕜] {g : α → F} {l : Filter α} {c : 𝕜} {f : α → 𝕜} (hc : c ≠ 0) : (fun (x : α) => c * f x) =Θ[l] g → f =Θ[l] g

Alias of the forward direction of Asymptotics.isTheta_const_mul_left.

theorem Asymptotics.isTheta_const_mul_right {α : Type u_1} {E : Type u_3} {𝕜 : Type u_14} [Norm E] [NormedField 𝕜] {f : α → E} {l : Filter α} {c : 𝕜} {g : α → 𝕜} (hc : c ≠ 0) : (f =Θ[l] fun (x : α) => c * g x) ↔ f =Θ[l] g

theorem Asymptotics.IsTheta.of_const_mul_right {α : Type u_1} {E : Type u_3} {𝕜 : Type u_14} [Norm E] [NormedField 𝕜] {f : α → E} {l : Filter α} {c : 𝕜} {g : α → 𝕜} (hc : c ≠ 0) : (f =Θ[l] fun (x : α) => c * g x) → f =Θ[l] g

Alias of the forward direction of Asymptotics.isTheta_const_mul_right.

theorem Asymptotics.IsTheta.const_mul_right {α : Type u_1} {E : Type u_3} {𝕜 : Type u_14} [Norm E] [NormedField 𝕜] {f : α → E} {l : Filter α} {c : 𝕜} {g : α → 𝕜} (hc : c ≠ 0) : f =Θ[l] g → f =Θ[l] fun (x : α) => c * g x

Alias of the reverse direction of Asymptotics.isTheta_const_mul_right.

theorem Asymptotics.IsLittleO.right_isTheta_add {α : Type u_1} {E' : Type u_6} [SeminormedAddCommGroup E'] {l : Filter α} {f₁ f₂ : α → E'} (h : f₁ =o[l] f₂) : f₂ =Θ[l] (f₁ + f₂)

theorem Asymptotics.IsLittleO.right_isTheta_add' {α : Type u_1} {E' : Type u_6} [SeminormedAddCommGroup E'] {l : Filter α} {f₁ f₂ : α → E'} (h : f₁ =o[l] f₂) : f₂ =Θ[l] (f₂ + f₁)

theorem Asymptotics.IsTheta.add_isLittleO {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] [SeminormedAddCommGroup E'] {l : Filter α} {f₁ f₂ : α → E'} {g : α → F} (hΘ : f₁ =Θ[l] g) (ho : f₂ =o[l] g) : (f₁ + f₂) =Θ[l] g

theorem Asymptotics.IsLittleO.add_isTheta {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] [SeminormedAddCommGroup E'] {l : Filter α} {f₁ f₂ : α → E'} {g : α → F} (ho : f₁ =o[l] g) (hΘ : f₂ =Θ[l] g) : (f₁ + f₂) =Θ[l] g

theorem Asymptotics.isTheta_of_div_tendsto_nhds_ne_zero {α : Type u_1} {𝕜 : Type u_14} [NormedField 𝕜] {l : Filter α} {c : 𝕜} {f g : α → 𝕜} (h : Filter.Tendsto (fun (x : α) => g x / f x) l (nhds c)) (hc : c ≠ 0) : f =Θ[l] g

theorem Asymptotics.IsTheta.fiberwise_right {α : Type u_1} {β : Type u_2} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {l : Filter α} {f : α × β → E} {g : α × β → F} {l' : Filter β} : f =Θ[l ×ˢ l'] g → ∀ᶠ (x : α) in l, (fun (x_1 : β) => f (x, x_1)) =Θ[l'] fun (x_1 : β) => g (x, x_1)

theorem Asymptotics.IsTheta.fiberwise_left {α : Type u_1} {β : Type u_2} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {l : Filter α} {f : α × β → E} {g : α × β → F} {l' : Filter β} : f =Θ[l ×ˢ l'] g → ∀ᶠ (y : β) in l', (fun (x : α) => f (x, y)) =Θ[l] fun (x : α) => g (x, y)

theorem Asymptotics.IsTheta.comp_fst {α : Type u_1} {β : Type u_2} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : α → E} {g : α → F} {l : Filter α} (l' : Filter β) : f =Θ[l] g → (f ∘ Prod.fst) =Θ[l ×ˢ l'] (g ∘ Prod.fst)

theorem Asymptotics.IsTheta.comp_snd {α : Type u_1} {β : Type u_2} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : α → E} {g : α → F} {l : Filter α} (l' : Filter β) : f =Θ[l] g → (f ∘ Prod.snd) =Θ[l' ×ˢ l] (g ∘ Prod.snd)

theorem ContinuousOn.isTheta_principal {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddGroup E] [SeminormedAddGroup F] [TopologicalSpace α] {s : Set α} {f : α → E} {c : F} (hf : ContinuousOn f s) (hs : IsCompact s) (hc : ‖c‖ ≠ 0) (hC : ∀ i ∈ s, f i ≠ 0) : f =Θ[Filter.principal s] fun (x : α) => c