OAI/Analysis/FiniteFactor/CrossedProduct/MaskedSquareMass.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteFactor.sourceOmitted_masked_square line 13

   Source documentation

   The actual source columns and deterministic omitted-index masks satisfy the infinite conditional square estimate in both orientations.

   theorem sourceOmitted_masked_square (θ : SourceCoordinate → ℝ) (hθ : SourceAngles θ)
       {p : SourceHilbert SourceCoordinate →L[ℂ] SourceHilbert SourceCoordinate}
       (hp : p ∈ sourceAlgebra θ) (hproj : IsStarProjection p)
       (j : ℕ) (hphase : SourceSecondPhasesFrom θ j) (n r : ℤ) (b : Bool) :
       (∫ ω, (∑' k : ℤ, (sourceOmittedBadEvent θ hθ j hphase n k b).indicator
         (fun ω => ‖sourceColumn p b (sourceBiasedEndpoint (fun _ => b) ω) (r+k)‖^2) ω)
         ∂sourceBiasedLaw j) ≤ Real.exp (-(sourceStage j).L/400) := by
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceAngles, OAI.FiniteFactor.SourceHilbert, OAI.FiniteFactor.sourceAlgebra, OAI.FiniteFactor.SourceSecondPhasesFrom, OAI.FiniteFactor.sourceOmittedBadEvent, OAI.FiniteFactor.sourceColumn, OAI.FiniteFactor.sourceBiasedEndpoint, OAI.FiniteFactor.sourceBiasedLaw, OAI.FiniteFactor.sourceStage