Bounded mean

[silviacasac]

First pull request for the Bounded mean transformation, which corresponds to this GitHub permalink.

Files:

• mean.tex -- the LaTeX document with the proof.
• mean.pdf -- the PDF generated from the TeX document.

Note: this transformation is very similar to the Bounded sum with known n one (except for handling the floating point issues when dividing by n) and so any comments which are added to the Bounded sum with known n pull request are very likely to be applicable here too, and viceversa.

[silviacasac]

Remaining things to check:

• Whether it is OK that the castings to not appear in the proof.
• Important. Floating point issues both in the addition of the elements and in the division. We are working on it.