OAI/NumberTheory/JointDickman/Counting/HistogramWindows.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Local collections of fine cells for an endpoint box

  1. def OAI.JointDickman.histogramWindowCells line 12
  2. theorem OAI.JointDickman.mem_histogramWindowCells line 15
  3. theorem OAI.JointDickman.histogramWindowCells_length line 21
  4. theorem OAI.JointDickman.endpoint_support_log_bounds line 56

    Source documentation

    Every retained integer in a fixed endpoint support lies in the interior of the manuscript's logarithmic interval for sufficiently large B.

    theorem endpoint_support_log_bounds {a b : ℝ} (ha : 0 < a) (hab : a ≤ b) :
    ∀ᶠ B : ℕ in atTop, ∀ N : ℝ, 0 < N →
      Real.log N ∈ Set.Icc ((9/10 : ℝ)*B) ((5/2 : ℝ)*B) →
      ∀ k : ℕ, a < (k : ℝ)/N → (k : ℝ)/N ≤ b →
        Real.log k/B ∈ Set.Ioc (1/2 : ℝ) 3 := by
…