OAI/Analysis/FiniteFactor/CrossedProduct/FiniteCoefficients.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteFactor.sourceBoundary_cocycle_finite line 14

   Source documentation

   Every signed finite coefficient uses the actual D_j. Positive indices use the exact later-floor exclusions; negative indices use antitonicity.

   theorem sourceBoundary_cocycle_finite (θ : SourceCoordinate → ℝ) (hθ : SourceAngles θ)
       (j : ℕ) (ω : SourceBiasedSample) (he : ω ∈ sourceBoundaryEvent j)
       (hxc : ∀ i, sourceBiasedEndpoint (fun _ => false) ω i ∈ Set.Ico 0 1)
       (hyc : ∀ i, sourceBiasedEndpoint (fun _ => true) ω i ∈ Set.Ico 0 1)
       (hfx : finiteFloorSupport θ (sourceBiasedEndpoint (fun _ => false) ω))
       (hfy : finiteFloorSupport θ (sourceBiasedEndpoint (fun _ => true) ω))
       (k : ℤ) (hk : |(k : ℝ)| ≤ (sourceStageState j).K) :
       1/sourceCocycle θ sourceLogWeight k (sourceBiasedEndpoint (fun _ => false) ω) ≤ (sourceStageState j).D ∧
       sourceCocycle θ sourceLogWeight (-k) (sourceBiasedEndpoint (fun _ => true) ω) ≤ (sourceStageState j).D := by
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceAngles, OAI.FiniteFactor.SourceBiasedSample, OAI.FiniteFactor.sourceBoundaryEvent, OAI.FiniteFactor.sourceBiasedEndpoint, OAI.FiniteFactor.finiteFloorSupport, OAI.FiniteFactor.sourceStageState, OAI.FiniteFactor.sourceCocycle, OAI.FiniteFactor.sourceLogWeight

2. theorem OAI.FiniteFactor.sourceProjection_finite_coefficients line 52

   Source documentation

   Finite coefficient bounds for the arbitrary projection in the original algebra, on the actual source boundary-exclusion event.

   theorem sourceProjection_finite_coefficients (θ : SourceCoordinate → ℝ) (hθ : SourceAngles θ)
       {p : SourceHilbert SourceCoordinate →L[ℂ] SourceHilbert SourceCoordinate}
       (hp : p ∈ sourceAlgebra θ) (hproj : IsStarProjection p) (j : ℕ) :
       ∀ᵐ ω ∂sourceBiasedLaw j, ω ∈ sourceBoundaryEvent j → ∀ k : ℤ,
         |(k : ℝ)| ≤ (sourceStageState j).K →
         ‖sourceProjectionLeftCoefficient θ p (sourceBiasedEndpoint (fun _ => false) ω) k‖ ≤ (sourceStageState j).D ∧
         ‖sourceProjectionRightCoefficient θ p (sourceBiasedEndpoint (fun _ => true) ω) k‖ ≤ (sourceStageState j).D := by
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceAngles, OAI.FiniteFactor.SourceHilbert, OAI.FiniteFactor.sourceAlgebra, OAI.FiniteFactor.sourceBiasedLaw, OAI.FiniteFactor.sourceBoundaryEvent, OAI.FiniteFactor.sourceStageState, OAI.FiniteFactor.sourceProjectionLeftCoefficient, OAI.FiniteFactor.sourceBiasedEndpoint, OAI.FiniteFactor.sourceProjectionRightCoefficient