OAI/Analysis/FiniteFactor/CrossedProduct/UncappedPairIdentity.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteFactor.sourceLambda_endpoints_finiteFloor line 12

   Source documentation

   The limiting endpoints have finite floor support, because both actual lambda_I marginals are Haar-dominated.

   theorem sourceLambda_endpoints_finiteFloor (θ : SourceCoordinate → ℝ) (hθ : SourceAngles θ)
       (I : Finset SourceCoordinate) :
       ∀ᵐ z ∂(sourceSamplingLambdaTorus I : Measure SourceSamplingTorus),
         finiteFloorSupport θ (sourceTorusRepresentative z.1) ∧
         finiteFloorSupport θ (sourceTorusRepresentative z.2) := by
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceAngles, OAI.FiniteFactor.sourceSamplingLambdaTorus, OAI.FiniteFactor.SourceSamplingTorus, OAI.FiniteFactor.finiteFloorSupport, OAI.FiniteFactor.sourceTorusRepresentative

2. theorem OAI.FiniteFactor.sourceCappedRatio_eq_ratio line 25
3. theorem OAI.FiniteFactor.sourceProjection_lambda_ratio_identity line 36