OAI/NumberTheory/Ostmann/Arithmetic/MovingFrequencyBudget.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The actual accumulated gaps and rounded frequency cutoffs of Section 7

  1. def OAI.Ostmann.movingCutoffExponent line 12

    Source documentation

    The square-root reserve agrees with the proved bottom cutoff at 4m.

    noncomputable def movingCutoffExponent (Bs BD Bz z m : ℝ) (n : ℕ) : ℝ :=
…
  2. def OAI.Ostmann.movingNaturalCutoff line 17
  3. def OAI.Ostmann.movingFrequencyRate line 21

    Source documentation

    One unit of reserve is left for the root-frequency count.

    noncomputable def movingFrequencyRate (Bs BD Bz z : ℝ) (n : ℕ) : ℝ :=
…
  4. theorem OAI.Ostmann.movingCutoffExponent_zero line 25
  5. theorem OAI.Ostmann.movingCutoffExponent_succ line 29
  6. theorem OAI.Ostmann.moving_sum_two_pow line 36
  7. theorem OAI.Ostmann.movingCutoffExponent_bound line 44
  8. theorem OAI.Ostmann.movingNaturalCutoff_frequency_bound line 87