Truncation.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.FiniteFactor.laurent_row_eq line 12

Source documentation

Sum a row of the Laurent coefficient double sum using its unique possible second exponent.

theorem laurent_row_eq (K : ℕ) (A B : ℤ → ℂ) (r v : ℤ) :
    (∑ j : Fin (2*K+1), if v + ((j.val : ℤ)-K) = r then
      A v * B ((j.val : ℤ)-K) else 0) =
    if -(K : ℤ) ≤ r-v ∧ r-v ≤ K then A v * B (r-v) else 0 := by
…

def OAI.FiniteFactor.convolutionWindow line 41
Source documentation
A finite subset of ℤ, exactly the two simultaneous coefficient cutoffs.
```
noncomputable def convolutionWindow (K : ℕ) (n : ℤ) : Finset ℤ :=
…
```
theorem OAI.FiniteFactor.mem_convolutionWindow line 44
theorem OAI.FiniteFactor.not_mem_convolutionWindow line 49
theorem OAI.FiniteFactor.laurent_coefficient_eq_finite_convolution line 54

theorem OAI.FiniteFactor.laurent_coefficient_eq_neg_tail line 78

Source documentation

A zero absolutely convergent convolution forces the exact finite Laurent coefficient to be the negative complementary tail.

theorem laurent_coefficient_eq_neg_tail (K : ℕ) (A B : ℤ → ℂ) (n : ℤ)
    (hs : Summable (fun v => A v * B (-n-v)))
    (hz : ∑' v, A v * B (-n-v) = 0) :
    laurentProductCoefficient K A B (-n) =
      -(∑' v : {v : ℤ // v ∉ convolutionWindow K n}, A v * B (-n-v)) := by
…

Mentions: OAI.FiniteFactor.laurentProductCoefficient, OAI.FiniteFactor.convolutionWindow

theorem OAI.FiniteFactor.laurent_coefficient_norm_le_tail line 87

Source documentation

The corresponding absolute tail bound used in error-pointwise.

theorem laurent_coefficient_norm_le_tail (K : ℕ) (A B : ℤ → ℂ) (n : ℤ)
    (hs : Summable (fun v => ‖A v * B (-n-v)‖))
    (hz : ∑' v, A v * B (-n-v) = 0) :
    ‖laurentProductCoefficient K A B (-n)‖ ≤
      ∑' v : {v : ℤ // v ∉ convolutionWindow K n}, ‖A v * B (-n-v)‖ := by
…

Mentions: OAI.FiniteFactor.laurentProductCoefficient, OAI.FiniteFactor.convolutionWindow

theorem OAI.FiniteFactor.laurent_error_pointwise line 97

Source documentation

The full pointwise error estimate. The two exceptional masks remain separate and each is summed over all of ℤ; no union bound is introduced.

theorem laurent_error_pointwise (K : ℕ) (n : ℤ)
    (ξ γ : lp (fun _ : ℤ => ℂ) 2) {F G : ℤ → ℝ}
    (hF : ∀ k, 0 < F k) (hG : ∀ k, 0 < G k)
    (hFa : Antitone F) (hGa : Antitone G) (hGF : ∀ k, G k ≤ F k)
    (hn : 0 ≤ n) {H₁ H₂ : Set ℤ} {ε : ℝ} (hε : 0 ≤ ε)
    (hz : ∑' v, leftCoefficient F ξ v * rightCoefficient G γ (-n-v) = 0)
    (hR : ∀ v, v ∉ convolutionWindow K n →
      G (n+v) / F v ≤ ε + H₁.indicator (fun _ => 1) v +
        H₂.indicator (fun _ => 1) v) :
    ‖laurentProductCoefficient K (leftCoefficient F ξ) (rightCoefficient G γ) (-n)‖ ≤
      ε * (‖ξ‖ * ‖γ‖) +
      (∑' v, H₁.indicator (fun v => ‖ξ v‖ * ‖γ (n+v)‖) v) +
…

Mentions: OAI.FiniteFactor.leftCoefficient, OAI.FiniteFactor.rightCoefficient, OAI.FiniteFactor.convolutionWindow, OAI.FiniteFactor.laurentProductCoefficient