Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-bigo Structured version   Visualization version   GIF version

Definition df-bigo 42135
Description: Define the function "big-O", mapping a real function g to the set of real functions "of order g(x)". Definition in section 1.1 of [AhoHopUll] p. 2. This is a generalisation of "big-O of one", see df-o1 14015 and df-lo1 14016. As explained in the comment of df-o1 , any big-O can be represented in terms of 𝑂(1) and division, see elbigolo1 42144. (Contributed by AV, 15-May-2020.)
Assertion
Ref Expression
df-bigo Ο = (𝑔 ∈ (ℝ ↑pm ℝ) ↦ {𝑓 ∈ (ℝ ↑pm ℝ) ∣ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(𝑓𝑦) ≤ (𝑚 · (𝑔𝑦))})
Distinct variable group:   𝑓,𝑔,𝑥,𝑚,𝑦

Detailed syntax breakdown of Definition df-bigo
StepHypRef Expression
1 cbigo 42134 . 2 class Ο
2 vg . . 3 setvar 𝑔
3 cr 9791 . . . 4 class
4 cpm 7722 . . . 4 class pm
53, 3, 4co 6527 . . 3 class (ℝ ↑pm ℝ)
6 vy . . . . . . . . . 10 setvar 𝑦
76cv 1473 . . . . . . . . 9 class 𝑦
8 vf . . . . . . . . . 10 setvar 𝑓
98cv 1473 . . . . . . . . 9 class 𝑓
107, 9cfv 5790 . . . . . . . 8 class (𝑓𝑦)
11 vm . . . . . . . . . 10 setvar 𝑚
1211cv 1473 . . . . . . . . 9 class 𝑚
132cv 1473 . . . . . . . . . 10 class 𝑔
147, 13cfv 5790 . . . . . . . . 9 class (𝑔𝑦)
15 cmul 9797 . . . . . . . . 9 class ·
1612, 14, 15co 6527 . . . . . . . 8 class (𝑚 · (𝑔𝑦))
17 cle 9931 . . . . . . . 8 class
1810, 16, 17wbr 4577 . . . . . . 7 wff (𝑓𝑦) ≤ (𝑚 · (𝑔𝑦))
199cdm 5028 . . . . . . . 8 class dom 𝑓
20 vx . . . . . . . . . 10 setvar 𝑥
2120cv 1473 . . . . . . . . 9 class 𝑥
22 cpnf 9927 . . . . . . . . 9 class +∞
23 cico 12004 . . . . . . . . 9 class [,)
2421, 22, 23co 6527 . . . . . . . 8 class (𝑥[,)+∞)
2519, 24cin 3538 . . . . . . 7 class (dom 𝑓 ∩ (𝑥[,)+∞))
2618, 6, 25wral 2895 . . . . . 6 wff 𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(𝑓𝑦) ≤ (𝑚 · (𝑔𝑦))
2726, 11, 3wrex 2896 . . . . 5 wff 𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(𝑓𝑦) ≤ (𝑚 · (𝑔𝑦))
2827, 20, 3wrex 2896 . . . 4 wff 𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(𝑓𝑦) ≤ (𝑚 · (𝑔𝑦))
2928, 8, 5crab 2899 . . 3 class {𝑓 ∈ (ℝ ↑pm ℝ) ∣ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(𝑓𝑦) ≤ (𝑚 · (𝑔𝑦))}
302, 5, 29cmpt 4637 . 2 class (𝑔 ∈ (ℝ ↑pm ℝ) ↦ {𝑓 ∈ (ℝ ↑pm ℝ) ∣ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(𝑓𝑦) ≤ (𝑚 · (𝑔𝑦))})
311, 30wceq 1474 1 wff Ο = (𝑔 ∈ (ℝ ↑pm ℝ) ↦ {𝑓 ∈ (ℝ ↑pm ℝ) ∣ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(𝑓𝑦) ≤ (𝑚 · (𝑔𝑦))})
Colors of variables: wff setvar class
This definition is referenced by:  bigoval  42136  elbigofrcl  42137
  Copyright terms: Public domain W3C validator