Convolution.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.FiniteFactor.cocycle_antitone_of_step line 15
Source documentation
Monotonicity follows from the integer cocycle's one-step recurrence; this includes negative integer indices.
```
theorem cocycle_antitone_of_step {F w : ℤ → ℝ}
    (hF : ∀ k, 0 ≤ F k) (hw : ∀ k, w k ≤ 1)
    (hstep : ∀ k, F (k+1) = w k * F k) : Antitone F := by
…
```

theorem OAI.FiniteFactor.cocycle_two_ratio_bounds line 24

Source documentation

Both cocycle ratio bounds, valid at every integer index.

theorem cocycle_two_ratio_bounds {F G : ℤ → ℝ}
    (hF : ∀ k, 0 < F k) (hG : ∀ k, 0 < G k)
    (hFa : Antitone F) (hGa : Antitone G) (hGF : ∀ k, G k ≤ F k)
    {n v : ℤ} (hn : 0 ≤ n) :
    0 < G (n + v) / F v ∧
    G (n + v) / F v ≤ min (G v / F v) (G (n + v) / F (n + v)) ∧
    min (G v / F v) (G (n + v) / F (n + v)) ≤ 1 := by
…

theorem OAI.FiniteFactor.shifted_l2_norm_product line 38

Source documentation

Cauchy--Schwarz with a genuine integer translation of the second vector.

theorem shifted_l2_norm_product (ξ γ : lp (fun _ : ℤ => ℂ) 2) (n : ℤ) :
    Summable (fun v => ‖ξ v‖ * ‖γ (n + v)‖) ∧
    (∑' v, ‖ξ v‖ * ‖γ (n + v)‖) ≤ ‖ξ‖ * ‖γ‖ := by
…

theorem OAI.FiniteFactor.weighted_convolution_summable line 55

Source documentation

The ratio-weighted convolution is absolutely convergent and has the sharp product-of-L²-norms bound.

theorem weighted_convolution_summable (ξ γ : lp (fun _ : ℤ => ℂ) 2)
    (n : ℤ) {r : ℤ → ℝ} (hr0 : ∀ v, 0 ≤ r v) (hr1 : ∀ v, r v ≤ 1) :
    Summable (fun v => ‖(r v : ℂ) * ξ v * conj (γ (n + v))‖) ∧
    (∑' v, ‖(r v : ℂ) * ξ v * conj (γ (n + v))‖) ≤ ‖ξ‖ * ‖γ‖ := by
…

def OAI.FiniteFactor.leftCoefficient line 74
Source documentation
Exact rescaling used in coefficient-sequences; neither sequence is required to belong to ℓ².
```
noncomputable def leftCoefficient (F : ℤ → ℝ) (ξ : ℤ → ℂ) (v : ℤ) : ℂ :=
…
```
def OAI.FiniteFactor.rightCoefficient line 77
theorem OAI.FiniteFactor.cocycle_convolution_term_eq line 80
theorem OAI.FiniteFactor.cocycle_convolution_absolute_convergence line 87

theorem OAI.FiniteFactor.weighted_shift_convolution_eq_inner line 104

Source documentation

Reindexing the Hilbert inner product gives the exact convolution from coordinates of the shifted weighted vector.

theorem weighted_shift_convolution_eq_inner
    (ξ γ η : lp (fun _ : ℤ => ℂ) 2) (r : ℤ → ℝ) (n : ℤ)
    (hη : ∀ v, η (n+v) = (r v : ℂ) * ξ v) :
    (∑' v, (r v : ℂ) * ξ v * conj (γ (n+v))) = inner ℂ γ η := by
…

theorem OAI.FiniteFactor.cocycle_convolution_zero_of_range line 118

Source documentation

Orthogonality of the image vector to the complementary range produces convolution-identity, with its original rescaled coefficients and signs.

theorem cocycle_convolution_zero_of_range
    (ξ γ η : lp (fun _ : ℤ => ℂ) 2) (F G : ℤ → ℝ) (n : ℤ)
    (V : Submodule ℂ (lp (fun _ : ℤ => ℂ) 2))
    (hηV : η ∈ V) (hγV : γ ∈ Vᗮ)
    (hη : ∀ v, η (n+v) = (G (n+v) / F v : ℝ) * ξ v) :
    (∑' v, leftCoefficient F ξ v * rightCoefficient G γ (-n-v)) = 0 := by
…

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

theorem OAI.FiniteFactor.finite_part_eq_neg_tail line 130
Source documentation
Removing any finite part of a zero absolutely convergent series gives its exact complementary tail, before applying the triangle inequality.
```
theorem finite_part_eq_neg_tail {t : ℤ → ℂ} (ht : Summable t)
    (hzero : ∑' v, t v = 0) (W : Finset ℤ) :
    (∑ v ∈ W, t v) = -(∑' v : {v : ℤ // v ∉ W}, t v) := by
…
```
theorem OAI.FiniteFactor.finite_part_norm_le_tail line 137
def OAI.FiniteFactor.omittedIndex line 144
Source documentation
The deterministic omitted-index choice used for both complementary masks.
```
def omittedIndex (K : ℕ) (n v : ℤ) : ℤ :=
…
```
theorem OAI.FiniteFactor.omittedIndex_spec line 147