OAI/Analysis/FiniteFactor/CrossedProduct/ProjectionConvolution.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteFactor.sourceProjection_convolution line 15

   Source documentation

   The original coefficient sequences satisfy every nonnegative convolution identity under the actual augmented biased law, with absolute sum at most one. This instantiates the range and weight hypotheses from the constructed algebra.

   theorem sourceProjection_convolution (θ : SourceCoordinate → ℝ) (hθ : SourceAngles θ)
       (hs : SourceOrderedTorusSampling θ)
       {p : SourceHilbert SourceCoordinate →L[ℂ] SourceHilbert SourceCoordinate}
       (hp : p ∈ sourceAlgebra θ) (hproj : IsStarProjection p)
       (hinv : (1-p)*sourceOperator θ sourceLogWeight hθ.nonneg sourceLogWeight_nonneg*p = 0)
       (j : ℕ) :
       ∀ᵐ ω ∂sourceBiasedLaw j, ∀ n : ℕ,
         (∑' k : ℤ, sourceProjectionLeftCoefficient θ p (sourceBiasedEndpoint (fun _ => false) ω) k *
           sourceProjectionRightCoefficient θ p (sourceBiasedEndpoint (fun _ => true) ω) (-(n : ℤ)-k)) = 0 ∧
         Summable (fun k : ℤ => ‖sourceProjectionLeftCoefficient θ p (sourceBiasedEndpoint (fun _ => false) ω) k *
           sourceProjectionRightCoefficient θ p (sourceBiasedEndpoint (fun _ => true) ω) (-(n : ℤ)-k)‖) ∧
         (∑' k : ℤ, ‖sourceProjectionLeftCoefficient θ p (sourceBiasedEndpoint (fun _ => false) ω) k *
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceAngles, OAI.FiniteFactor.SourceOrderedTorusSampling, OAI.FiniteFactor.SourceHilbert, OAI.FiniteFactor.sourceAlgebra, OAI.FiniteFactor.sourceOperator, OAI.FiniteFactor.sourceLogWeight, OAI.FiniteFactor.sourceLogWeight_nonneg, OAI.FiniteFactor.sourceBiasedLaw, OAI.FiniteFactor.sourceProjectionLeftCoefficient, OAI.FiniteFactor.sourceBiasedEndpoint, OAI.FiniteFactor.sourceProjectionRightCoefficient