Asymptotic relations and product types

This file contains lemmas about asymptotic relations for product-valued functions and product filters.

Product of functions (right)

theorem Asymptotics.isBigOWith_fst_prod {α : Type u_1} {E' : Type u_5} {F' : Type u_6} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] {f' : α → E'} {g' : α → F'} {l : Filter α} : IsBigOWith 1 l f' fun (x : α) => (f' x, g' x)

theorem Asymptotics.isBigOWith_snd_prod {α : Type u_1} {E' : Type u_5} {F' : Type u_6} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] {f' : α → E'} {g' : α → F'} {l : Filter α} : IsBigOWith 1 l g' fun (x : α) => (f' x, g' x)

theorem Asymptotics.isBigO_fst_prod {α : Type u_1} {E' : Type u_5} {F' : Type u_6} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] {f' : α → E'} {g' : α → F'} {l : Filter α} : f' =O[l] fun (x : α) => (f' x, g' x)

theorem Asymptotics.isBigO_snd_prod {α : Type u_1} {E' : Type u_5} {F' : Type u_6} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] {f' : α → E'} {g' : α → F'} {l : Filter α} : g' =O[l] fun (x : α) => (f' x, g' x)

theorem Asymptotics.isBigO_fst_prod' {α : Type u_1} {E' : Type u_5} {F' : Type u_6} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] {l : Filter α} {f' : α → E' × F'} : (fun (x : α) => (f' x).1) =O[l] f'

theorem Asymptotics.isBigO_snd_prod' {α : Type u_1} {E' : Type u_5} {F' : Type u_6} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] {l : Filter α} {f' : α → E' × F'} : (fun (x : α) => (f' x).2) =O[l] f'

theorem Asymptotics.IsBigOWith.prod_rightl {α : Type u_1} {E : Type u_3} {F' : Type u_6} {G' : Type u_7} [Norm E] [SeminormedAddCommGroup F'] [SeminormedAddCommGroup G'] {c : ℝ} {f : α → E} {g' : α → F'} (k' : α → G') {l : Filter α} (h : IsBigOWith c l f g') (hc : 0 ≤ c) : IsBigOWith c l f fun (x : α) => (g' x, k' x)

theorem Asymptotics.IsBigO.prod_rightl {α : Type u_1} {E : Type u_3} {F' : Type u_6} {G' : Type u_7} [Norm E] [SeminormedAddCommGroup F'] [SeminormedAddCommGroup G'] {f : α → E} {g' : α → F'} (k' : α → G') {l : Filter α} (h : f =O[l] g') : f =O[l] fun (x : α) => (g' x, k' x)

theorem Asymptotics.IsLittleO.prod_rightl {α : Type u_1} {E : Type u_3} {F' : Type u_6} {G' : Type u_7} [Norm E] [SeminormedAddCommGroup F'] [SeminormedAddCommGroup G'] {f : α → E} {g' : α → F'} (k' : α → G') {l : Filter α} (h : f =o[l] g') : f =o[l] fun (x : α) => (g' x, k' x)

theorem Asymptotics.IsBigOWith.prod_rightr {α : Type u_1} {E : Type u_3} {E' : Type u_5} {F' : Type u_6} [Norm E] [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] {c : ℝ} {f : α → E} (f' : α → E') {g' : α → F'} {l : Filter α} (h : IsBigOWith c l f g') (hc : 0 ≤ c) : IsBigOWith c l f fun (x : α) => (f' x, g' x)

theorem Asymptotics.IsBigO.prod_rightr {α : Type u_1} {E : Type u_3} {E' : Type u_5} {F' : Type u_6} [Norm E] [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] {f : α → E} (f' : α → E') {g' : α → F'} {l : Filter α} (h : f =O[l] g') : f =O[l] fun (x : α) => (f' x, g' x)

theorem Asymptotics.IsLittleO.prod_rightr {α : Type u_1} {E : Type u_3} {E' : Type u_5} {F' : Type u_6} [Norm E] [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] {f : α → E} (f' : α → E') {g' : α → F'} {l : Filter α} (h : f =o[l] g') : f =o[l] fun (x : α) => (f' x, g' x)

theorem Asymptotics.IsBigO.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 =O[l ×ˢ l'] g → ∀ᶠ (a : α) in l, (fun (x : β) => f (a, x)) =O[l'] fun (x : β) => g (a, x)

theorem Asymptotics.IsBigO.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 =O[l ×ˢ l'] g → ∀ᶠ (b : β) in l', (fun (x : α) => f (x, b)) =O[l] fun (x : α) => g (x, b)

theorem Asymptotics.IsBigO.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 =O[l] g → (f ∘ Prod.fst) =O[l ×ˢ l'] (g ∘ Prod.fst)

theorem Asymptotics.IsBigO.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 =O[l] g → (f ∘ Prod.snd) =O[l' ×ˢ l] (g ∘ Prod.snd)

theorem Asymptotics.IsLittleO.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 =o[l] g → (f ∘ Prod.fst) =o[l ×ˢ l'] (g ∘ Prod.fst)

theorem Asymptotics.IsLittleO.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 =o[l] g → (f ∘ Prod.snd) =o[l' ×ˢ l] (g ∘ Prod.snd)

theorem Asymptotics.IsBigOWith.prod_left_same {α : Type u_1} {E' : Type u_5} {F' : Type u_6} {G' : Type u_7} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] [SeminormedAddCommGroup G'] {c : ℝ} {f' : α → E'} {g' : α → F'} {k' : α → G'} {l : Filter α} (hf : IsBigOWith c l f' k') (hg : IsBigOWith c l g' k') : IsBigOWith c l (fun (x : α) => (f' x, g' x)) k'

theorem Asymptotics.IsBigOWith.prod_left {α : Type u_1} {E' : Type u_5} {F' : Type u_6} {G' : Type u_7} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] [SeminormedAddCommGroup G'] {c c' : ℝ} {f' : α → E'} {g' : α → F'} {k' : α → G'} {l : Filter α} (hf : IsBigOWith c l f' k') (hg : IsBigOWith c' l g' k') : IsBigOWith (max c c') l (fun (x : α) => (f' x, g' x)) k'

theorem Asymptotics.IsBigOWith.prod_left_fst {α : Type u_1} {E' : Type u_5} {F' : Type u_6} {G' : Type u_7} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] [SeminormedAddCommGroup G'] {c : ℝ} {f' : α → E'} {g' : α → F'} {k' : α → G'} {l : Filter α} (h : IsBigOWith c l (fun (x : α) => (f' x, g' x)) k') : IsBigOWith c l f' k'

theorem Asymptotics.IsBigOWith.prod_left_snd {α : Type u_1} {E' : Type u_5} {F' : Type u_6} {G' : Type u_7} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] [SeminormedAddCommGroup G'] {c : ℝ} {f' : α → E'} {g' : α → F'} {k' : α → G'} {l : Filter α} (h : IsBigOWith c l (fun (x : α) => (f' x, g' x)) k') : IsBigOWith c l g' k'

theorem Asymptotics.isBigOWith_prod_left {α : Type u_1} {E' : Type u_5} {F' : Type u_6} {G' : Type u_7} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] [SeminormedAddCommGroup G'] {c : ℝ} {f' : α → E'} {g' : α → F'} {k' : α → G'} {l : Filter α} : IsBigOWith c l (fun (x : α) => (f' x, g' x)) k' ↔ IsBigOWith c l f' k' ∧ IsBigOWith c l g' k'

theorem Asymptotics.IsBigO.prod_left {α : Type u_1} {E' : Type u_5} {F' : Type u_6} {G' : Type u_7} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] [SeminormedAddCommGroup G'] {f' : α → E'} {g' : α → F'} {k' : α → G'} {l : Filter α} (hf : f' =O[l] k') (hg : g' =O[l] k') : (fun (x : α) => (f' x, g' x)) =O[l] k'

theorem Asymptotics.IsBigO.prod_left_fst {α : Type u_1} {E' : Type u_5} {F' : Type u_6} {G' : Type u_7} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] [SeminormedAddCommGroup G'] {f' : α → E'} {g' : α → F'} {k' : α → G'} {l : Filter α} : (fun (x : α) => (f' x, g' x)) =O[l] k' → f' =O[l] k'

theorem Asymptotics.IsBigO.prod_left_snd {α : Type u_1} {E' : Type u_5} {F' : Type u_6} {G' : Type u_7} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] [SeminormedAddCommGroup G'] {f' : α → E'} {g' : α → F'} {k' : α → G'} {l : Filter α} : (fun (x : α) => (f' x, g' x)) =O[l] k' → g' =O[l] k'

@[simp]

theorem Asymptotics.isBigO_prod_left {α : Type u_1} {E' : Type u_5} {F' : Type u_6} {G' : Type u_7} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] [SeminormedAddCommGroup G'] {f' : α → E'} {g' : α → F'} {k' : α → G'} {l : Filter α} : (fun (x : α) => (f' x, g' x)) =O[l] k' ↔ f' =O[l] k' ∧ g' =O[l] k'

theorem Asymptotics.IsLittleO.prod_left {α : Type u_1} {E' : Type u_5} {F' : Type u_6} {G' : Type u_7} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] [SeminormedAddCommGroup G'] {f' : α → E'} {g' : α → F'} {k' : α → G'} {l : Filter α} (hf : f' =o[l] k') (hg : g' =o[l] k') : (fun (x : α) => (f' x, g' x)) =o[l] k'

theorem Asymptotics.IsLittleO.prod_left_fst {α : Type u_1} {E' : Type u_5} {F' : Type u_6} {G' : Type u_7} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] [SeminormedAddCommGroup G'] {f' : α → E'} {g' : α → F'} {k' : α → G'} {l : Filter α} : (fun (x : α) => (f' x, g' x)) =o[l] k' → f' =o[l] k'

theorem Asymptotics.IsLittleO.prod_left_snd {α : Type u_1} {E' : Type u_5} {F' : Type u_6} {G' : Type u_7} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] [SeminormedAddCommGroup G'] {f' : α → E'} {g' : α → F'} {k' : α → G'} {l : Filter α} : (fun (x : α) => (f' x, g' x)) =o[l] k' → g' =o[l] k'

@[simp]

theorem Asymptotics.isLittleO_prod_left {α : Type u_1} {E' : Type u_5} {F' : Type u_6} {G' : Type u_7} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] [SeminormedAddCommGroup G'] {f' : α → E'} {g' : α → F'} {k' : α → G'} {l : Filter α} : (fun (x : α) => (f' x, g' x)) =o[l] k' ↔ f' =o[l] k' ∧ g' =o[l] k'