OAI/NumberTheory/Ostmann/Construction/InitialWordRanges.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Exact closed integer ranges for the original logarithmic word bins

  1. theorem OAI.Ostmann.floor_log_eq_iff_integer_range line 13

    Source documentation

    Integer endpoints express the half-open logarithmic bin exactly.

    theorem floor_log_eq_iff_integer_range (M j : ℕ) (hM : 0 < M) :
    ⌊Real.log (M : ℝ)⌋₊ = j ↔
      (M : ℝ) ∈ Set.Icc (⌈Real.exp (j : ℝ)⌉₊ : ℝ)
        (⌈Real.exp ((j : ℝ) + 1)⌉₊ - 1 : ℕ) := by
…
  2. def OAI.Ostmann.initialWordBinRange line 31
  3. theorem OAI.Ostmann.initialWordBinRange_holds line 37
  4. theorem OAI.Ostmann.wordLogBin_eq_iff_integer_range line 50