ProjectionPairIdentity.lean`

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.FiniteFactor.sourceProjection_ordered_orbits line 13
Source documentation
Every original invariant projection satisfies the normalized equation on all its ordered positive orbit pairs, on one conull set.
```
theorem sourceProjection_ordered_orbits (θ : SourceCoordinate → ℝ) (hθ : SourceAngles θ)
    {p : SourceHilbert SourceCoordinate →L[ℂ] SourceHilbert SourceCoordinate}
    (hp : p ∈ sourceAlgebra θ) (hproj : IsStarProjection p)
    (hinv : (1-p)*sourceOperator θ sourceLogWeight hθ.nonneg sourceLogWeight_nonneg*p = 0) :
    ∀ᵐ z ∂sourceTorusHaar, ∀ n : ℕ,
      (∀ i, sourceTorusRepresentative z i ≤ sourceTorusRepresentative (sourceTorusRotate θ n z) i) →
      (z,sourceTorusRotate θ n z) ∈ sourceCappedPairZeroSet θ p := by
…
```
Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceAngles, OAI.FiniteFactor.SourceHilbert, OAI.FiniteFactor.sourceAlgebra, OAI.FiniteFactor.sourceOperator, OAI.FiniteFactor.sourceLogWeight, OAI.FiniteFactor.sourceLogWeight_nonneg, OAI.FiniteFactor.sourceTorusHaar, OAI.FiniteFactor.sourceTorusRepresentative, OAI.FiniteFactor.sourceTorusRotate, OAI.FiniteFactor.sourceCappedPairZeroSet
theorem OAI.FiniteFactor.sourceProjection_sampling_pairs line 56
Source documentation
The approximant equations follow from the original invariant projection, the actual positive orbit support, and absolute continuity of the first marginal. They are not assumed as a transfer premise.
```
theorem sourceProjection_sampling_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)
    (I : Finset SourceCoordinate) (s : ℕ) :
    ∀ᵐ z ∂(sourceSamplingTrimmedTorus I s θ : 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.sourceSamplingTrimmedTorus, OAI.FiniteFactor.SourceSamplingTorus, OAI.FiniteFactor.sourceCappedPairZeroSet
theorem OAI.FiniteFactor.sourceProjection_lambda_pairs line 82