ProductLogCells.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The actual logarithmic and residue cells, with partial output

def OAI.JointDickman.logResidueCell line 12
theorem OAI.JointDickman.logResidueCell_eq_some line 21

theorem OAI.JointDickman.high_product_cell_iff line 50

Source documentation

Multiplication by the common product translates the log cell and permutes the unit residue. The high-exclusive cutoff changes only the lower endpoint.

theorem high_product_cell_iff {B c n q : ℕ} (hc : 0 < c) (hn : 0 < n)
    (u r : (ZMod q)ˣ) (hu : (c : ZMod q) = u) (a b θ : ℝ) :
    (θ < Real.log n / B ∧
      Real.log (c * n : ℕ) / B ∈ Set.Ioc a b ∧ ((c * n : ℕ) : ZMod q) = (r : ZMod q)) ↔
    (Real.log n / B ∈ Set.Ioc (max θ (a - Real.log c / B)) (b - Real.log c / B) ∧
      (n : ZMod q) = (u⁻¹ * r : (ZMod q)ˣ)) := by
…

theorem OAI.JointDickman.product_cell_iff line 78

Source documentation

The uncut product cell is a translated log interval with a permuted residue.

theorem product_cell_iff {B c n q : ℕ} (hc : 0 < c) (hn : 0 < n)
    (u r : (ZMod q)ˣ) (hu : (c : ZMod q) = u) (a b : ℝ) :
    (Real.log (c * n : ℕ) / B ∈ Set.Ioc a b ∧ ((c * n : ℕ) : ZMod q) = (r : ZMod q)) ↔
    (Real.log n / B ∈ Set.Ioc (a - Real.log c / B) (b - Real.log c / B) ∧
      (n : ZMod q) = (u⁻¹ * r : (ZMod q)ˣ)) := by
…