CyclicInterval.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.cyclic_sub_val_margin line 10

Source documentation

A point to the right of an inner interval is separated from that interval in both directions around the cyclic group.

theorem cyclic_sub_val_margin {q : ℕ} [NeZero q]
    (x y : ZMod q) (d : ℕ) (hy : d ≤ y.val)
    (hgap : y.val + d ≤ x.val) :
    d ≤ (x - y).val ∧ (x - y).val + d ≤ q := by
…

theorem OAI.Problem337.cyclic_sub_phase_margin line 19

Source documentation

Normalized version of the cyclic separation estimate.

theorem cyclic_sub_phase_margin {q : ℕ} [NeZero q]
    (x y : ZMod q) (d : ℕ) (hy : d ≤ y.val)
    (hgap : y.val + d ≤ x.val) :
    (d : ℝ) / q ≤ ((x - y).val : ℝ) / q ∧
    ((x - y).val : ℝ) / q ≤ 1 - (d : ℝ) / q := by
…

theorem OAI.Problem337.cyclic_initial_interval_phase_margin line 36

Source documentation

An inner initial interval with margin d lies away from every point outside the initial target interval ending at B+d.

theorem cyclic_initial_interval_phase_margin {q : ℕ} [NeZero q]
    (x y : ZMod q) (d B : ℕ)
    (hx : B + d ≤ x.val) (hy : d ≤ y.val ∧ y.val ≤ B) :
    (d : ℝ) / q ≤ ((x - y).val : ℝ) / q ∧
    ((x - y).val : ℝ) / q ≤ 1 - (d : ℝ) / q :=
…

theorem OAI.Problem337.cyclic_interval_eq_image line 44

Source documentation

A cyclic interval is the image of its ordinary representatives.

theorem cyclic_interval_eq_image {q : ℕ} [NeZero q] (a b : ℕ) (hb : b < q) :
    (Finset.univ.filter (fun x : ZMod q => a ≤ x.val ∧ x.val ≤ b)) =
      (Finset.Icc a b).image (fun n : ℕ => (n : ZMod q)) := by
…

theorem OAI.Problem337.cyclic_interval_card line 58

Source documentation

Exact cardinality of a cyclic interval which does not cross zero.

theorem cyclic_interval_card {q : ℕ} [NeZero q] (a b : ℕ) (hb : b < q) :
    (Finset.univ.filter (fun x : ZMod q => a ≤ x.val ∧ x.val ≤ b)).card =
      b + 1 - a := by
…