bigo.txt

Definitions:

```
f(n) = O(g(n)) <==> \exists x_0 \in R, m \in R+, \forall x >= x_0, 0 < g(x) \land |f(x)| <= m * g(x)
```

Let `a(n) = O(b(n))`
Let `c(n) = O(d(n))`

We have:

```
\exists x_0_a \in R, m_a \in R+,
\exists x_0_b \in R, m_b \in R+,
(\forall x >= x_0_a, |a(x)| <= m_a * b(x)) \land
(\forall x >= x_0_b, |c(x)| <= m_b * d(x))
```

By relation of `>=` to `max`:

```
\exists x_0_a \in R, m_a \in R+,
\exists x_0_b \in R, m_b \in R+,
(\forall x >= max(x_0_a, x_0_b), |a(x)| <= m_a * b(x)) \land
(\forall x >= max(x_0_a, x_0_b), |c(x)| <= m_b * d(x))
```

Let `x_0 = max(x_0_a, x_0_b)`, and by existence of `x_0`:

```
\exists x_0 \in R, m_a \in R+, m_b \in R+,
(\forall x >= x_0, |a(x)| <= m_a * b(x)) \land
(\forall x >= x_0, |c(x)| <= m_b * d(x))
```

By relation of `<=` to `max` and `*`:

```
\exists x_0 \in R, m_a \in R+, m_b \in R+,
(\forall x >= x_0, |a(x)| <= max(m_a, m_b) * b(x)) \land
(\forall x >= x_0, |c(x)| <= max(m_a, m_b) * d(x))
```

Let `m = max(m_a, m_b)`, and by existence of `m`:

```
\exists x_0 \in R, m \in R+,
(\forall x >= x_0, |a(x)| <= m * b(x)) \land
(\forall x >= x_0, |c(x)| <= m * d(x))
```

Combine both clauses as both sides of inequality are non-negative:


```
\exists x_0 \in R, m \in R+,
(\forall x >= x_0, |a(x)| * |c(x)| <= m * b(x) * m * d(x))
```

Let `M = m * m`:

```
\exists x_0 \in R, M \in R+,
(\forall x >= x_0, |a(x)| * |c(x)| <= M * b(x) * d(x))
```

By `|ab| = |a||b|`:

```
\exists x_0 \in R, M \in R+,
(\forall x >= x_0, |a(x) * c(x)| <= M * b(x) * d(x))
```

Therefore: `a(n) * c(n) = O(b(n) * d(n))