OAI/NumberTheory/JointDickman/Counting/HistogramWindowBounds.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.endpoint_histogram_window_length line 10
2. theorem OAI.JointDickman.endpoint_histogram_window_scale line 36

   Source documentation

   The enlarged cell window changes the upper physical scale by at most exp(1).

   theorem endpoint_histogram_window_scale {m B : ℕ} (hm : 0 < m) (hB : 1 ≤ B)
       {a b N : ℝ} (hb : 0 < b) (hN : 0 < N)
       {i : Fin (channelFineCount m B)}
       (hi : i ∈ histogramWindowCells (channelFineCount m B)
         (Real.log (a*N)/B) (Real.log (b*N)/B))
       {x : ℝ} (hx : x ∈ Set.Icc (channelLower (channelFineCount m B) i)
         (channelUpper (channelFineCount m B) i)) :
       Real.exp ((B : ℝ)*x)/N ≤ b*Real.exp 1 := by
   …

   Mentions: OAI.JointDickman.channelFineCount, OAI.JointDickman.histogramWindowCells, OAI.JointDickman.channelLower, OAI.JointDickman.channelUpper