OAI/Analysis/FiniteFactor/OrbitSampling/TorusLimitMarginals.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteFactor.sourceSamplingLambdaTorus_marginal_le line 14

   Source documentation

   The actual compact-torus limiting marginals are dominated by product Haar, the exact absolute continuity premise needed in the Lusin transfer.

   theorem sourceSamplingLambdaTorus_marginal_le (I : Finset SourceCoordinate) (r : Bool) :
       (sourceSamplingLambdaTorus I : Measure SourceSamplingTorus).map (sourceTorusEndpoint r) ≤ sourceTorusHaar := by
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceSamplingLambdaTorus, OAI.FiniteFactor.SourceSamplingTorus, OAI.FiniteFactor.sourceTorusEndpoint, OAI.FiniteFactor.sourceTorusHaar

2. theorem OAI.FiniteFactor.sourceSamplingLambdaTorus_marginal_ac line 25
3. theorem OAI.FiniteFactor.sourceSamplingLambda_representatives line 29
4. theorem OAI.FiniteFactor.sourceSamplingLambdaTorus_ordered line 47

   Source documentation

   The actual limiting torus measure has the same representative order as the trimmed measures. No closure of the order set in torus topology is assumed.

   theorem sourceSamplingLambdaTorus_ordered (I : Finset SourceCoordinate) :
       ∀ᵐ p ∂(sourceSamplingLambdaTorus I : Measure SourceSamplingTorus),
         ∀ i, sourceTorusRepresentative p.1 i ≤ sourceTorusRepresentative p.2 i := by
   …

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