TransportConvolution.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.FiniteFactor.invariant_transport_composition line 11
Source documentation
Composition of the two genuine range inclusions used in the convolution.
```
theorem invariant_transport_composition {R : Type*} [Ring R] (P Q D W : R)
    (hD : (1-Q)*D*P = 0) (hW : (1-Q)*W*Q = 0) :
    (1-Q)*W*D*P = 0 := by
…
```
theorem OAI.FiniteFactor.fiber_complement_inner_zero line 23

theorem OAI.FiniteFactor.fiber_transport_convolution_zero line 32

Source documentation

The source convolution vanishes whenever the actual transport and weighted power identities hold. No square summability of rescaled coefficients is assumed.

theorem fiber_transport_convolution_zero
    (P Q D W : SourceFiberHilbert →L[ℂ] SourceFiberHilbert)
    (hQ : IsStarProjection Q) (F G : ℤ → ℝ) (hG : ∀ k, G k ≠ 0) (n : ℤ)
    (hD : (1-Q)*D*P = 0) (hW : (1-Q)*W*Q = 0)
    (hDa : ∀ (v : SourceFiberHilbert) (k : ℤ), D v k = (G k / F k : ℂ) * v k)
    (hWa : ∀ (v : SourceFiberHilbert) (k : ℤ), W v (n+k) = (G (n+k) / G k : ℂ) * v k) :
    (∑' k, leftCoefficient F (P (lp.single 2 0 (1 : ℂ))) k *
      rightCoefficient G ((1-Q) (lp.single 2 0 (1 : ℂ))) (-n-k)) = 0 := by
…

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