LeastResidueBridge.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.least_remainder_eq_neg_cast_val line 10
Source documentation
The integer remainder in the ceiling descent is exactly the canonical representative of the negative residue, including remainder zero.
```
theorem least_remainder_eq_neg_cast_val {u A z : ℕ} [NeZero u]
    (hlo : A ≤ u * z) (hhi : u * z < A + u) :
    u * z - A = (-(A : ZMod u)).val := by
…
```
theorem OAI.Problem337.ceiling_remainder_eq_neg_cast_val line 21
Source documentation
Natural rational ceiling supplies the exact least-residue integer.
```
theorem ceiling_remainder_eq_neg_cast_val {u A : ℕ} [NeZero u] :
    u * ⌈(A : ℚ) / (u : ℚ)⌉₊ - A = (-(A : ZMod u)).val := by
…
```
theorem OAI.Problem337.ceiling_remainder_lt_iff line 38
Source documentation
Consequently the natural small-remainder condition is literally the initial cyclic interval condition used in Fourier smoothing.
```
theorem ceiling_remainder_lt_iff {u A : ℕ} [NeZero u] (B : ℝ) :
    ((u * ⌈(A : ℚ) / (u : ℚ)⌉₊ - A : ℕ) : ℝ) < B ↔
      (((-(A : ZMod u)).val : ℕ) : ℝ) < B := by
…
```
theorem OAI.Problem337.stdAddChar_nat_phase line 45
Source documentation
Standard additive characters at natural residues are the usual exponential phases without choosing a representative.
```
theorem stdAddChar_nat_phase {u : ℕ} [NeZero u] (A : ℕ) :
    ZMod.stdAddChar (A : ZMod u) =
      Complex.exp (2 * Real.pi * Complex.I * (A : ℂ) / (u : ℂ)) := by
…
```

theorem OAI.Problem337.stdAddChar_nat_product_phase line 52

Source documentation

In particular, the positive Fourier coefficient for natural products is exactly the exponential sum in the residue estimates.

theorem stdAddChar_nat_product_phase {u : ℕ} [NeZero u] (l A : ℕ) :
    ZMod.stdAddChar ((l : ZMod u) * (A : ZMod u)) =
      Complex.exp (2 * Real.pi * Complex.I * (l * A : ℕ) / (u : ℂ)) := by
…

theorem OAI.Problem337.norm_neg_residue_fourier_eq line 59

Source documentation

Passing from positive exponential phases to the negative least-residue phases preserves every Fourier coefficient norm.

theorem norm_neg_residue_fourier_eq {u : ℕ} [NeZero u]
    {I : Type*} [Fintype I] (A : I → ℕ) (l : ℕ) :
    ‖∑ t : I, ZMod.stdAddChar ((l : ZMod u) * (-(A t : ZMod u)))‖ =
      ‖∑ t : I, Complex.exp
        (2 * Real.pi * Complex.I * (l * A t : ℕ) / (u : ℂ))‖ := by
…

theorem OAI.Problem337.norm_neg_residue_fourier_average_eq line 71

Source documentation

The normalized-average version used by the discrepancy estimate.

theorem norm_neg_residue_fourier_average_eq {u : ℕ} [NeZero u]
    {I : Type*} [Fintype I] (A : I → ℕ) (l : ℕ) :
    ‖(∑ t : I, ZMod.stdAddChar ((l : ZMod u) * (-(A t : ZMod u)))) /
        (Fintype.card I : ℂ)‖ =
      ‖(∑ t : I, Complex.exp
        (2 * Real.pi * Complex.I * (l * A t : ℕ) / (u : ℂ))) /
          (Fintype.card I : ℂ)‖ := by
…