CeilResidue.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.residue_eq_neg_zmod_val line 10
Source documentation
The natural remainder specified by a ceiling step is the canonical representative of the negative residue, including remainder zero.
```
theorem residue_eq_neg_zmod_val {u N z h : ℕ} (hh : h < u)
    (heq : u * z = N + h) : h = (-(N : ZMod u)).val := by
…
```

theorem OAI.Problem337.residue_div_eq_fract_neg line 20

Source documentation

The same remainder normalized by its modulus is the real fractional part.

theorem residue_div_eq_fract_neg {u N z h : ℕ} (hh : h < u)
    (heq : u * z = N + h) :
    (h : ℝ) / u = Int.fract (-(N : ℝ) / u) := by
…

theorem OAI.Problem337.natural_ceil_residue_spec line 34

Source documentation

Arithmetic specifications of the nonnegative ceiling remainder.

theorem natural_ceil_residue_spec (u N : ℕ) (hu : 0 < u) :
    N ≤ u * ⌈(N : ℝ) / u⌉₊ ∧
    u * ⌈(N : ℝ) / u⌉₊ = N + (u * ⌈(N : ℝ) / u⌉₊ - N) ∧
    u * ⌈(N : ℝ) / u⌉₊ - N < u := by
…

theorem OAI.Problem337.natural_ceil_residue_eq_neg_zmod_val line 51
theorem OAI.Problem337.natural_ceil_residue_div_eq_fract_neg line 56

theorem OAI.Problem337.residue_lt_iff_fract_lt line 63

Source documentation

Exact conversion of a real residue cutoff to the fractional-part interval.

theorem residue_lt_iff_fract_lt {u N z h : ℕ} (hh : h < u)
    (heq : u * z = N + h) (δ : ℝ) :
    (h : ℝ) < δ * u ↔ Int.fract (-(N : ℝ) / u) < δ := by
…

theorem OAI.Problem337.residue_lt_iff_neg_zmod_val_lt line 71

Source documentation

Exact conversion to the normalized canonical representative in ZMod.

theorem residue_lt_iff_neg_zmod_val_lt {u N z h : ℕ} (hh : h < u)
    (heq : u * z = N + h) (δ : ℝ) :
    (h : ℝ) < δ * u ↔ ((-(N : ZMod u)).val : ℝ) / u < δ := by
…