PairIdentity.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.FiniteFactor.sourceProjection_biased_prefix_pairs line 11
theorem OAI.FiniteFactor.sourceProjection_biased_pairs line 29
Source documentation
Weak transfer to the actual full biased law. Uniform absolute continuity and the common compact zero sets have all been proved for these actual laws.
```
theorem sourceProjection_biased_pairs (θ : 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 : ℕ) :
    ∀ᵐ z ∂(sourceBiasedTorusMeasure j (fun _ => true) : Measure SourceSamplingTorus),
      z ∈ sourceCappedPairZeroSet θ p := 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.sourceBiasedTorusMeasure, OAI.FiniteFactor.SourceSamplingTorus, OAI.FiniteFactor.sourceCappedPairZeroSet
theorem OAI.FiniteFactor.sourceBiased_endpoints_finiteFloor line 60
Source documentation
Both endpoints of every actual biased law have finite floor support.
```
theorem sourceBiased_endpoints_finiteFloor (θ : SourceCoordinate → ℝ) (hθ : SourceAngles θ)
    (j : ℕ) :
    ∀ᵐ z ∂(sourceBiasedTorusMeasure j (fun _ => true) : Measure SourceSamplingTorus),
      finiteFloorSupport θ (sourceTorusRepresentative z.1) ∧
      finiteFloorSupport θ (sourceTorusRepresentative z.2) := by
…
```
Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceAngles, OAI.FiniteFactor.sourceBiasedTorusMeasure, OAI.FiniteFactor.SourceSamplingTorus, OAI.FiniteFactor.finiteFloorSupport, OAI.FiniteFactor.sourceTorusRepresentative

theorem OAI.FiniteFactor.sourceProjection_biased_ratio_identity line 71

Source documentation

The full uncapped invariant-projection identity under the constructed nu_j. The bounded diagonal acts by the original cocycle ratio on every l2 vector.

theorem sourceProjection_biased_ratio_identity (θ : 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 : ℕ) :
    ∀ᵐ z ∂(sourceBiasedTorusMeasure j (fun _ => true) : Measure SourceSamplingTorus),
      ∃ D : SourceFiberHilbert →L[ℂ] SourceFiberHilbert,
        ‖D‖ ≤ 1 ∧
        (∀ (v : SourceFiberHilbert) (k : ℤ), D v k =
          (sourceCocycle θ sourceLogWeight k (sourceTorusRepresentative z.2) /
            sourceCocycle θ sourceLogWeight k (sourceTorusRepresentative z.1) : ℂ) * v 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.sourceBiasedTorusMeasure, OAI.FiniteFactor.SourceSamplingTorus, OAI.FiniteFactor.SourceFiberHilbert, OAI.FiniteFactor.sourceCocycle, OAI.FiniteFactor.sourceTorusRepresentative