Enforce a-related parameters as natural numbers

[Parcly-Taxel]

More specifically a, A = 2 ^ A, D = 2 ^ (100 * a ^ 2) and the constant S in the definition of GridStructure.

The blueprint explicitly states that a is natural, and having this avoids "rounding fudges" in some proofs. Cf. Zulip.

[fpvandoorn]

Looks good to me, thanks! two comments:

• Can you revert the changes to DoublingMeasure? A doubling measure is a concept that I would like to move to Mathlib relatively soon, and there is no reason to restrict the parameter to a natural number abstractly.
• You might want to cast the natural numbers to real numbers as soon as possible, by explicitly writing e.g. (A : ℝ) ^ 2. That might save some exact_mod_casts.

[fpvandoorn]

Thanks!