BscThesisFormalisation

3 lemma 2.1

3.1 General Idea

What we would like to do is mostly just copy the proof from the thesis, since almost nothing happens in it anyway. For this we need the following definitions:

  1. concave

  2. sublinear

  3. speedup.

Lemma 11
#

For any concave, sublinear speedup function, \(s\) with \(\alpha \in \mathbb {R}^n\), the function \(i\cdot s(\frac{\alpha }{i})\) is increasing in \(i\) for all \(i{\lt}||\alpha ||_1\), and is non-decreasing in \(i\) for all \(i\geq ||\alpha ||_1\).

Proof

We will proof the following two different cases:

  1. \(i {\lt} ||\alpha ||_1\): We need to prove in this case that \(i\cdot s(\frac{\alpha }{i})\) is increasing. We will look at the following difference for any \(\delta {\gt} 0\):

    \[ i (1+\delta ) s \left(\frac{\alpha }{i\cdot (1+\delta )} \right) - i \cdot s (\frac{\alpha }{i}) = i \left((1+\delta ) s \left(\frac{\alpha }{i\cdot (1+\delta )} \right) - s (\frac{\alpha }{i})\right) \]

    Since \(||\frac{\alpha }{i}|| {\gt} 1\), \(s\) increases sublinearly, and \((1+\delta )s\left(\frac{\alpha }{i \cdot (1+\delta )}\right) {\gt} s(\frac{\alpha }{i})\). This yields

    \[ i \cdot (1+\delta )s\left(\frac{\alpha }{i\cdot (1+\delta )} \right) - i \cdot s\left(\frac{\alpha }{i}\right) {\gt} 0 \]

    From which we can conclude that \(i \cdot s(\frac{\alpha }{i})\) is increasing in \(i\).

  2. \(i \geq ||\alpha ||_1\): We need to prove in this case that \(i\cdot s(\frac{\alpha }{i})\) is non-decreasing. This follows directly from the assumption that \(s\left(\frac{\alpha }{i}\right) = \frac{\alpha \cdot \beta }{i}\). From which we conclude that

    \[ i\cdot s \left(\frac{\alpha }{i}\right) = \alpha \cdot \beta \qquad \forall i \geq ||\alpha ||_1 \]

    which is non-decreasing in \(i\).