TruncatedBound.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.FiniteFactor.sourceTruncatedCoefficient_measurable line 10
theorem OAI.FiniteFactor.sourceTruncatedCoefficient_norm_le_one line 25
Source documentation
Each actual truncated coefficient has norm at most one under the full biased law. This follows from the original absolute convolution bound.
```
theorem sourceTruncatedCoefficient_norm_le_one (θ : 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 n : ℕ) : ∀ᵐ ω ∂sourceBiasedLaw j, ‖sourceTruncatedCoefficient θ p j n ω‖ ≤ 1 := by
…
```
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.sourceTruncatedCoefficient
theorem OAI.FiniteFactor.sourceTruncatedCoefficient_integrable line 38