RealIdentity.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.FiniteFactor.sourceBiasedEndpoint_ae line 11
Source documentation
Almost-everywhere original-base properties transfer to every actual mixed endpoint.
```
theorem sourceBiasedEndpoint_ae (j : ℕ) (r : SourceCoordinate → Bool)
    {P : (SourceCoordinate → ℝ) → Prop} (hP : ∀ᵐ x ∂sourceBaseMeasure, P x) :
    ∀ᵐ ω ∂sourceBiasedLaw j, P (sourceBiasedEndpoint r ω) := by
…
```
Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceBaseMeasure, OAI.FiniteFactor.sourceBiasedLaw, OAI.FiniteFactor.sourceBiasedEndpoint

theorem OAI.FiniteFactor.sourceProjection_biased_ratio_augmented line 22

Source documentation

The full uncapped pair identity on the actual augmented probability space, with the original real endpoints and original operator fields.

theorem sourceProjection_biased_ratio_augmented (θ : 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 : ℕ) :
    ∀ᵐ ω ∂sourceBiasedLaw j,
      ∃ D : SourceFiberHilbert →L[ℂ] SourceFiberHilbert,
        ‖D‖ ≤ 1 ∧
        (∀ (v : SourceFiberHilbert) (k : ℤ), D v k =
          (sourceCocycle θ sourceLogWeight k (sourceBiasedEndpoint (fun _ => true) ω) /
            sourceCocycle θ sourceLogWeight k (sourceBiasedEndpoint (fun _ => false) ω) : ℂ) * 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.sourceBiasedLaw, OAI.FiniteFactor.SourceFiberHilbert, OAI.FiniteFactor.sourceCocycle, OAI.FiniteFactor.sourceBiasedEndpoint