Arithmetic operations on asymptotic relations #
This file develops the behavior of IsBigOWith, IsBigO, and IsLittleO under absolute values,
negation, addition, subtraction, zero, constants, and finite sums.
Simplification: absolute value #
theorem
Asymptotics.IsBigOWith.of_abs_right
{α : Type u_1}
{E : Type u_2}
[Norm E]
{c : ℝ}
{f : α → E}
{l : Filter α}
{u : α → ℝ}
:
(IsBigOWith c l f fun (x : α) => |u x|) → IsBigOWith c l f u
Alias of the forward direction of Asymptotics.isBigOWith_abs_right.
theorem
Asymptotics.IsBigOWith.abs_right
{α : Type u_1}
{E : Type u_2}
[Norm E]
{c : ℝ}
{f : α → E}
{l : Filter α}
{u : α → ℝ}
:
IsBigOWith c l f u → IsBigOWith c l f fun (x : α) => |u x|
Alias of the reverse direction of Asymptotics.isBigOWith_abs_right.
theorem
Asymptotics.IsBigOWith.abs_left
{α : Type u_1}
{F : Type u_3}
[Norm F]
{c : ℝ}
{g : α → F}
{l : Filter α}
{u : α → ℝ}
:
IsBigOWith c l u g → IsBigOWith c l (fun (x : α) => |u x|) g
Alias of the reverse direction of Asymptotics.isBigOWith_abs_left.
theorem
Asymptotics.IsBigOWith.of_abs_left
{α : Type u_1}
{F : Type u_3}
[Norm F]
{c : ℝ}
{g : α → F}
{l : Filter α}
{u : α → ℝ}
:
IsBigOWith c l (fun (x : α) => |u x|) g → IsBigOWith c l u g
Alias of the forward direction of Asymptotics.isBigOWith_abs_left.
theorem
Asymptotics.IsBigOWith.of_abs_abs
{α : Type u_1}
{c : ℝ}
{l : Filter α}
{u v : α → ℝ}
:
(IsBigOWith c l (fun (x : α) => |u x|) fun (x : α) => |v x|) → IsBigOWith c l u v
Alias of the forward direction of Asymptotics.isBigOWith_abs_abs.
theorem
Asymptotics.IsBigOWith.abs_abs
{α : Type u_1}
{c : ℝ}
{l : Filter α}
{u v : α → ℝ}
:
IsBigOWith c l u v → IsBigOWith c l (fun (x : α) => |u x|) fun (x : α) => |v x|
Alias of the reverse direction of Asymptotics.isBigOWith_abs_abs.
Simplification: negate #
@[simp]
theorem
Asymptotics.isBigOWith_neg_right
{α : Type u_1}
{E : Type u_2}
{F' : Type u_5}
[Norm E]
[SeminormedAddCommGroup F']
{c : ℝ}
{f : α → E}
{g' : α → F'}
{l : Filter α}
:
theorem
Asymptotics.IsBigOWith.neg_right
{α : Type u_1}
{E : Type u_2}
{F' : Type u_5}
[Norm E]
[SeminormedAddCommGroup F']
{c : ℝ}
{f : α → E}
{g' : α → F'}
{l : Filter α}
:
IsBigOWith c l f g' → IsBigOWith c l f fun (x : α) => -g' x
Alias of the reverse direction of Asymptotics.isBigOWith_neg_right.
theorem
Asymptotics.IsBigOWith.of_neg_right
{α : Type u_1}
{E : Type u_2}
{F' : Type u_5}
[Norm E]
[SeminormedAddCommGroup F']
{c : ℝ}
{f : α → E}
{g' : α → F'}
{l : Filter α}
:
(IsBigOWith c l f fun (x : α) => -g' x) → IsBigOWith c l f g'
Alias of the forward direction of Asymptotics.isBigOWith_neg_right.
theorem
Asymptotics.IsBigO.neg_right
{α : Type u_1}
{E : Type u_2}
{F' : Type u_5}
[Norm E]
[SeminormedAddCommGroup F']
{f : α → E}
{g' : α → F'}
{l : Filter α}
:
Alias of the reverse direction of Asymptotics.isBigO_neg_right.
theorem
Asymptotics.IsBigO.of_neg_right
{α : Type u_1}
{E : Type u_2}
{F' : Type u_5}
[Norm E]
[SeminormedAddCommGroup F']
{f : α → E}
{g' : α → F'}
{l : Filter α}
:
Alias of the forward direction of Asymptotics.isBigO_neg_right.
theorem
Asymptotics.IsLittleO.of_neg_right
{α : Type u_1}
{E : Type u_2}
{F' : Type u_5}
[Norm E]
[SeminormedAddCommGroup F']
{f : α → E}
{g' : α → F'}
{l : Filter α}
:
Alias of the forward direction of Asymptotics.isLittleO_neg_right.
theorem
Asymptotics.IsLittleO.neg_right
{α : Type u_1}
{E : Type u_2}
{F' : Type u_5}
[Norm E]
[SeminormedAddCommGroup F']
{f : α → E}
{g' : α → F'}
{l : Filter α}
:
Alias of the reverse direction of Asymptotics.isLittleO_neg_right.
@[simp]
theorem
Asymptotics.isBigOWith_neg_left
{α : Type u_1}
{F : Type u_3}
{E' : Type u_4}
[Norm F]
[SeminormedAddCommGroup E']
{c : ℝ}
{g : α → F}
{f' : α → E'}
{l : Filter α}
:
theorem
Asymptotics.IsBigOWith.neg_left
{α : Type u_1}
{F : Type u_3}
{E' : Type u_4}
[Norm F]
[SeminormedAddCommGroup E']
{c : ℝ}
{g : α → F}
{f' : α → E'}
{l : Filter α}
:
IsBigOWith c l f' g → IsBigOWith c l (fun (x : α) => -f' x) g
Alias of the reverse direction of Asymptotics.isBigOWith_neg_left.
theorem
Asymptotics.IsBigOWith.of_neg_left
{α : Type u_1}
{F : Type u_3}
{E' : Type u_4}
[Norm F]
[SeminormedAddCommGroup E']
{c : ℝ}
{g : α → F}
{f' : α → E'}
{l : Filter α}
:
IsBigOWith c l (fun (x : α) => -f' x) g → IsBigOWith c l f' g
Alias of the forward direction of Asymptotics.isBigOWith_neg_left.
theorem
Asymptotics.IsBigO.neg_left
{α : Type u_1}
{F : Type u_3}
{E' : Type u_4}
[Norm F]
[SeminormedAddCommGroup E']
{g : α → F}
{f' : α → E'}
{l : Filter α}
:
Alias of the reverse direction of Asymptotics.isBigO_neg_left.
theorem
Asymptotics.IsBigO.of_neg_left
{α : Type u_1}
{F : Type u_3}
{E' : Type u_4}
[Norm F]
[SeminormedAddCommGroup E']
{g : α → F}
{f' : α → E'}
{l : Filter α}
:
Alias of the forward direction of Asymptotics.isBigO_neg_left.
theorem
Asymptotics.IsLittleO.of_neg_left
{α : Type u_1}
{F : Type u_3}
{E' : Type u_4}
[Norm F]
[SeminormedAddCommGroup E']
{g : α → F}
{f' : α → E'}
{l : Filter α}
:
Alias of the forward direction of Asymptotics.isLittleO_neg_left.
theorem
Asymptotics.IsLittleO.neg_left
{α : Type u_1}
{F : Type u_3}
{E' : Type u_4}
[Norm F]
[SeminormedAddCommGroup E']
{g : α → F}
{f' : α → E'}
{l : Filter α}
:
Alias of the reverse direction of Asymptotics.isLittleO_neg_left.
theorem
Asymptotics.IsBigOWith.eq_zero_imp
{α : Type u_1}
{E'' : Type u_6}
{F'' : Type u_7}
[NormedAddCommGroup E'']
[NormedAddCommGroup F'']
{c : ℝ}
{f'' : α → E''}
{g'' : α → F''}
{l : Filter α}
(h : IsBigOWith c l f'' g'')
:
theorem
Asymptotics.IsBigO.eq_zero_imp
{α : Type u_1}
{E'' : Type u_6}
{F'' : Type u_7}
[NormedAddCommGroup E'']
[NormedAddCommGroup F'']
{f'' : α → E''}
{g'' : α → F''}
{l : Filter α}
(h : f'' =O[l] g'')
:
Addition and subtraction #
theorem
Asymptotics.IsBigOWith.add
{α : Type u_1}
{F : Type u_3}
{E' : Type u_4}
[Norm F]
[SeminormedAddCommGroup E']
{c₁ c₂ : ℝ}
{g : α → F}
{l : Filter α}
{f₁ f₂ : α → E'}
(h₁ : IsBigOWith c₁ l f₁ g)
(h₂ : IsBigOWith c₂ l f₂ g)
:
IsBigOWith (c₁ + c₂) l (fun (x : α) => f₁ x + f₂ x) g
theorem
Asymptotics.IsBigOWith.add_add
{α : Type u_1}
{E' : Type u_4}
[SeminormedAddCommGroup E']
{c₁ c₂ : ℝ}
{l : Filter α}
{f₁ f₂ : α → E'}
{g₁ g₂ : α → ℝ}
(h₁ : IsBigOWith c₁ l f₁ g₁)
(h₂ : IsBigOWith c₂ l f₂ g₂)
:
theorem
Asymptotics.IsBigOWith.add_isLittleO
{α : Type u_1}
{F : Type u_3}
{E' : Type u_4}
[Norm F]
[SeminormedAddCommGroup E']
{c₁ c₂ : ℝ}
{g : α → F}
{l : Filter α}
{f₁ f₂ : α → E'}
(h₁ : IsBigOWith c₁ l f₁ g)
(h₂ : f₂ =o[l] g)
(hc : c₁ < c₂)
:
IsBigOWith c₂ l (fun (x : α) => f₁ x + f₂ x) g
theorem
Asymptotics.IsLittleO.add_isBigOWith
{α : Type u_1}
{F : Type u_3}
{E' : Type u_4}
[Norm F]
[SeminormedAddCommGroup E']
{c₁ c₂ : ℝ}
{g : α → F}
{l : Filter α}
{f₁ f₂ : α → E'}
(h₁ : f₁ =o[l] g)
(h₂ : IsBigOWith c₁ l f₂ g)
(hc : c₁ < c₂)
:
IsBigOWith c₂ l (fun (x : α) => f₁ x + f₂ x) g
theorem
Asymptotics.IsBigOWith.sub
{α : Type u_1}
{F : Type u_3}
{E' : Type u_4}
[Norm F]
[SeminormedAddCommGroup E']
{c₁ c₂ : ℝ}
{g : α → F}
{l : Filter α}
{f₁ f₂ : α → E'}
(h₁ : IsBigOWith c₁ l f₁ g)
(h₂ : IsBigOWith c₂ l f₂ g)
:
IsBigOWith (c₁ + c₂) l (fun (x : α) => f₁ x - f₂ x) g
theorem
Asymptotics.IsBigOWith.sub_isLittleO
{α : Type u_1}
{F : Type u_3}
{E' : Type u_4}
[Norm F]
[SeminormedAddCommGroup E']
{c₁ c₂ : ℝ}
{g : α → F}
{l : Filter α}
{f₁ f₂ : α → E'}
(h₁ : IsBigOWith c₁ l f₁ g)
(h₂ : f₂ =o[l] g)
(hc : c₁ < c₂)
:
IsBigOWith c₂ l (fun (x : α) => f₁ x - f₂ x) g
Lemmas about IsBigO (f₁ - f₂) g l / IsLittleO (f₁ - f₂) g l treated as a binary relation #
theorem
Asymptotics.IsBigOWith.symm
{α : Type u_1}
{F : Type u_3}
{E' : Type u_4}
[Norm F]
[SeminormedAddCommGroup E']
{c : ℝ}
{g : α → F}
{l : Filter α}
{f₁ f₂ : α → E'}
(h : IsBigOWith c l (fun (x : α) => f₁ x - f₂ x) g)
:
IsBigOWith c l (fun (x : α) => f₂ x - f₁ x) g
theorem
Asymptotics.isBigOWith_comm
{α : Type u_1}
{F : Type u_3}
{E' : Type u_4}
[Norm F]
[SeminormedAddCommGroup E']
{c : ℝ}
{g : α → F}
{l : Filter α}
{f₁ f₂ : α → E'}
:
theorem
Asymptotics.IsBigOWith.triangle
{α : Type u_1}
{F : Type u_3}
{E' : Type u_4}
[Norm F]
[SeminormedAddCommGroup E']
{c c' : ℝ}
{g : α → F}
{l : Filter α}
{f₁ f₂ f₃ : α → E'}
(h₁ : IsBigOWith c l (fun (x : α) => f₁ x - f₂ x) g)
(h₂ : IsBigOWith c' l (fun (x : α) => f₂ x - f₃ x) g)
:
IsBigOWith (c + c') l (fun (x : α) => f₁ x - f₃ x) g
Zero and other constants #
theorem
Asymptotics.isLittleO_zero
{α : Type u_1}
{E' : Type u_4}
{F' : Type u_5}
[SeminormedAddCommGroup E']
[SeminormedAddCommGroup F']
(g' : α → F')
(l : Filter α)
:
theorem
Asymptotics.isBigOWith_zero
{α : Type u_1}
{E' : Type u_4}
{F' : Type u_5}
[SeminormedAddCommGroup E']
[SeminormedAddCommGroup F']
{c : ℝ}
(g' : α → F')
(l : Filter α)
(hc : 0 ≤ c)
:
IsBigOWith c l (fun (_x : α) => 0) g'
theorem
Asymptotics.isBigOWith_zero'
{α : Type u_1}
{F : Type u_3}
{E' : Type u_4}
[Norm F]
[SeminormedAddCommGroup E']
(g : α → F)
(l : Filter α)
:
IsBigOWith 0 l (fun (_x : α) => 0) g
theorem
Asymptotics.isBigO_zero
{α : Type u_1}
{F : Type u_3}
{E' : Type u_4}
[Norm F]
[SeminormedAddCommGroup E']
(g : α → F)
(l : Filter α)
:
theorem
Asymptotics.isBigO_refl_left
{α : Type u_1}
{E' : Type u_4}
{F' : Type u_5}
[SeminormedAddCommGroup E']
[SeminormedAddCommGroup F']
{f' : α → E'}
(g' : α → F')
(l : Filter α)
:
theorem
Asymptotics.isLittleO_refl_left
{α : Type u_1}
{E' : Type u_4}
{F' : Type u_5}
[SeminormedAddCommGroup E']
[SeminormedAddCommGroup F']
{f' : α → E'}
(g' : α → F')
(l : Filter α)
:
@[simp]
theorem
Asymptotics.isBigOWith_zero_right_iff
{α : Type u_1}
{F' : Type u_5}
{E'' : Type u_6}
[SeminormedAddCommGroup F']
[NormedAddCommGroup E'']
{c : ℝ}
{f'' : α → E''}
{l : Filter α}
:
@[simp]
theorem
Asymptotics.isBigO_zero_right_iff
{α : Type u_1}
{F' : Type u_5}
{E'' : Type u_6}
[SeminormedAddCommGroup F']
[NormedAddCommGroup E'']
{f'' : α → E''}
{l : Filter α}
:
@[simp]
theorem
Asymptotics.isLittleO_zero_right_iff
{α : Type u_1}
{F' : Type u_5}
{E'' : Type u_6}
[SeminormedAddCommGroup F']
[NormedAddCommGroup E'']
{f'' : α → E''}
{l : Filter α}
:
theorem
Asymptotics.isBigOWith_const_const
{α : Type u_1}
{E : Type u_2}
{F'' : Type u_7}
[Norm E]
[NormedAddCommGroup F'']
(c : E)
{c' : F''}
(hc' : c' ≠ 0)
(l : Filter α)
:
@[simp]
theorem
Asymptotics.isBigO_const_const_iff
{α : Type u_1}
{E'' : Type u_6}
{F'' : Type u_7}
[NormedAddCommGroup E'']
[NormedAddCommGroup F'']
{c : E''}
{c' : F''}
(l : Filter α)
[l.NeBot]
:
@[simp]
theorem
Asymptotics.isBigO_pure
{α : Type u_1}
{E'' : Type u_6}
{F'' : Type u_7}
[NormedAddCommGroup E'']
[NormedAddCommGroup F'']
{f'' : α → E''}
{g'' : α → F''}
{x : α}
:
Sum #
theorem
Asymptotics.IsBigOWith.sum
{α : Type u_1}
{F : Type u_3}
{E' : Type u_4}
[Norm F]
[SeminormedAddCommGroup E']
{g : α → F}
{l : Filter α}
{ι : Type u_8}
{A : ι → α → E'}
{C : ι → ℝ}
{s : Finset ι}
(h : ∀ i ∈ s, IsBigOWith (C i) l (A i) g)
:
IsBigOWith (∑ i ∈ s, C i) l (∑ i ∈ s, A i) g
theorem
Asymptotics.IsBigOWith.fun_sum
{α : Type u_1}
{F : Type u_3}
{E' : Type u_4}
[Norm F]
[SeminormedAddCommGroup E']
{g : α → F}
{l : Filter α}
{ι : Type u_8}
{A : ι → α → E'}
{C : ι → ℝ}
{s : Finset ι}
(h : ∀ i ∈ s, IsBigOWith (C i) l (A i) g)
:
IsBigOWith (∑ i ∈ s, C i) l (fun (a : α) => ∑ c ∈ s, A c a) g
Eta-expanded form of Asymptotics.IsBigOWith.sum
theorem
Asymptotics.IsBigO.fun_sum
{α : Type u_1}
{F : Type u_3}
{E' : Type u_4}
[Norm F]
[SeminormedAddCommGroup E']
{g : α → F}
{l : Filter α}
{ι : Type u_8}
{A : ι → α → E'}
{s : Finset ι}
(h : ∀ i ∈ s, A i =O[l] g)
:
Eta-expanded form of Asymptotics.IsBigO.sum
theorem
Asymptotics.IsLittleO.sum
{α : Type u_1}
{E' : Type u_4}
{F' : Type u_5}
[SeminormedAddCommGroup E']
[SeminormedAddCommGroup F']
{g' : α → F'}
{l : Filter α}
{ι : Type u_8}
{A : ι → α → E'}
{s : Finset ι}
(h : ∀ i ∈ s, A i =o[l] g')
:
theorem
Asymptotics.IsLittleO.fun_sum
{α : Type u_1}
{E' : Type u_4}
{F' : Type u_5}
[SeminormedAddCommGroup E']
[SeminormedAddCommGroup F']
{g' : α → F'}
{l : Filter α}
{ι : Type u_8}
{A : ι → α → E'}
{s : Finset ι}
(h : ∀ i ∈ s, A i =o[l] g')
:
Eta-expanded form of Asymptotics.IsLittleO.sum
theorem
Asymptotics.IsBigOWith.sum_congr
{α : Type u_1}
{E' : Type u_4}
[SeminormedAddCommGroup E']
{l : Filter α}
{ι : Type u_8}
{A : ι → α → E'}
{C : ι → ℝ}
{s : Finset ι}
{B : ι → α → ℝ}
(hAB : ∀ i ∈ s, IsBigOWith (C i) l (A i) (B i))
:
IsBigOWith (sSup (C '' ↑s)) l (fun (H : α) => ∑ i ∈ s, A i H) fun (H : α) => ∑ i ∈ s, ‖B i H‖
If each term A i of a sum IsBigO of B i, then the sum of the A i IsBigO of the sum
of the norms of the B i.
theorem
Asymptotics.IsBigOWith.sum_congr'
{α : Type u_1}
{E' : Type u_4}
[SeminormedAddCommGroup E']
{l : Filter α}
{ι : Type u_8}
{A : ι → α → E'}
{B : ι → α → ℝ}
{C : ℝ}
{i : α → Finset ι}
(hAB : IsBigOWith C (⊤ ×ˢ l) (Function.uncurry A) (Function.uncurry B))
:
IsBigOWith C l (fun (H : α) => ∑ j ∈ i H, A j H) fun (H : α) => ∑ j ∈ i H, ‖B j H‖
Similar to IsBigOWith.sum_congr except the index set can change in the sum. This requires the
constant in hAB to be independent of the index i and also the big-O relationship to "kick in"
at the same point along the running variable. Hence the ⊤ in ⊤ ×ˢ l.
theorem
Asymptotics.IsBigO.sum_congr'
{α : Type u_1}
{E' : Type u_4}
[SeminormedAddCommGroup E']
{l : Filter α}
{ι : Type u_8}
{A : ι → α → E'}
{B : ι → α → ℝ}
{i : α → Finset ι}
(hAB : Function.uncurry A =O[⊤ ×ˢ l] Function.uncurry B)
:
theorem
Asymptotics.IsLittleO.sum_congr'
{α : Type u_1}
{E' : Type u_4}
[SeminormedAddCommGroup E']
{l : Filter α}
{ι : Type u_8}
{A : ι → α → E'}
{B : ι → α → ℝ}
{i : α → Finset ι}
(hAB : Function.uncurry A =o[⊤ ×ˢ l] Function.uncurry B)
: