HistogramWindowOverlap.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Bounded overlap of logarithmic windows along a geometric scale

theorem OAI.JointDickman.integer_interval_card_le line 11

Source documentation

The integer lattice has at most length+1 points in any real interval.

theorem integer_interval_card_le (S : Finset ℤ) {a b : ℝ} (hab : a ≤ b)
    (hS : ∀ m ∈ S, a ≤ (m : ℝ) ∧ (m : ℝ) ≤ b) :
    (S.card : ℝ) ≤ b-a+1 := by
…

theorem OAI.JointDickman.histogramWindow_overlap line 38

Source documentation

For X=exp(m*t), the local cell windows have bounded overlap. The constant depends only on their fixed width, with B*mesh displayed.

theorem histogramWindow_overlap {B t L U : ℝ} (hB : 0 < B) (ht : 0 < t)
    (hLU : L ≤ U) {n : ℕ} (hn : 0 < n) (S : Finset ℤ) (i : Fin n) :
    ((S.filter (fun (m : ℤ) => i ∈ histogramWindowCells n
      (((m : ℝ)*t+L)/B) (((m : ℝ)*t+U)/B))).card : ℝ) ≤
        (B*channelMesh n+U-L)/t+1 := by
…

Mentions: OAI.JointDickman.histogramWindowCells, OAI.JointDickman.channelMesh