OAI/Analysis/LipschitzHilbert/Estimates/RelativeExitScales.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Dyadic selection of the relative exit scale for each nonzero interval.

  1. def OAI.LipschitzHilbert.relativeExitScale line 12

    Source documentation

    Relative radii, starting below one half as required by the pathwise argument.

    def relativeExitScale (m : ℕ) : ℝ := (1/4)*(1/2)^m
  2. theorem OAI.LipschitzHilbert.relativeExitScale_pos line 14
  3. theorem OAI.LipschitzHilbert.relativeExitScale_le line 18
  4. theorem OAI.LipschitzHilbert.relativeExitScale_succ line 23
  5. theorem OAI.LipschitzHilbert.exists_relativeExitScale line 28
  6. theorem OAI.LipschitzHilbert.relative_interval_scale line 48