TransferFrequencyRange.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The actual finite range of a transferred frequency

def OAI.Ostmann.transferFrequencyRange line 18
Source documentation
A fixed covering range for the signed output frequency. Zero is excluded in the summand, so the same interval also works when the range is empty.
```
def transferFrequencyRange (V : ℕ) : Finset ℤ := Finset.Icc (-(V : ℤ)) V
```
theorem OAI.Ostmann.mem_transferFrequencyRange line 20

theorem OAI.Ostmann.transferred_frequency_bound line 28

Source documentation

The product ranges supply the frequency cutoff without rounding a quotient or introducing an independent frequency assumption.

theorem transferred_frequency_bound (M L R B H V : ℕ) (s v w : ℤ)
    (hM : 0 < M) (hv : v.natAbs ≤ B) (hw : w.natAbs ≤ B)
    (hL : L ≤ H) (hR : R ≤ H)
    (hscale : 2 * B * H ≤ V * M)
    (hrel : v * R - w * L = s * M) : s.natAbs ≤ V := by
…

theorem OAI.Ostmann.transferred_frequency_sum line 45

Source documentation

One integer quotient contributes once, including its sign.

theorem transferred_frequency_sum (M : ℕ) (hM : 0 < M) (N : ℤ)
    (S : Finset ℤ) (hS : ∀ s : ℤ, s ≠ 0 → N = s * M → s ∈ S) (z : ℂ) :
    (if N ≠ 0 ∧ (M : ℤ) ∣ N then z else 0) =
      ∑ s ∈ S, if s ≠ 0 ∧ N = s * M then z else 0 := by
…

theorem OAI.Ostmann.transferred_frequency_sum_bounded line 74

Source documentation

A prime-product range is enough to cover every off-diagonal term by its actual new root frequency.

theorem transferred_frequency_sum_bounded (M L R B H V : ℕ)
    (hM : 0 < M) (v w : ℤ) (hv : v.natAbs ≤ B) (hw : w.natAbs ≤ B)
    (hL : L ≤ H) (hR : R ≤ H) (hscale : 2 * B * H ≤ V * M) (z : ℂ) :
    (if v * R - w * L ≠ 0 ∧ (M : ℤ) ∣ v * R - w * L then z else 0) =
      ∑ s ∈ transferFrequencyRange V,
        if s ≠ 0 ∧ v * R - w * L = s * M then z else 0 := by
…

Mentions: OAI.Ostmann.transferFrequencyRange