OAI/Analysis/FiniteFactor/OrbitSampling/LambdaMarginals.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteFactor.sourceSamplingLimitCoordinate line 11
2. theorem OAI.FiniteFactor.sourceSamplingLimitCoordinate_preserving line 14
3. theorem OAI.FiniteFactor.sourceSamplingLimitEndpoint_eq line 25
4. theorem OAI.FiniteFactor.sourceSamplingLimitEndpoint_preserving line 33

   Source documentation

   Before the triangular restriction, either selected endpoint is exactly product Haar, including the mixed first/second selection in the second endpoint.

   theorem sourceSamplingLimitEndpoint_preserving (I : Finset SourceCoordinate) (r : Bool) :
       MeasurePreserving (sourceSamplingEndpoint r ∘ sourceSamplingLimitMap I)
         sourceSamplingPairHaar sourceSamplingHaar := by
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceSamplingEndpoint, OAI.FiniteFactor.sourceSamplingLimitMap, OAI.FiniteFactor.sourceSamplingPairHaar, OAI.FiniteFactor.sourceSamplingHaar

5. theorem OAI.FiniteFactor.sourceSamplingLambda_marginal_le line 44

   Source documentation

   Both actual limiting marginals are submeasures of Haar. This proves the absolute continuity needed for the later Lusin transfer without assuming a marginal law.

   theorem sourceSamplingLambda_marginal_le (I : Finset SourceCoordinate) (r : Bool) :
       (sourceSamplingLambda I).map (sourceSamplingEndpoint r) ≤ sourceSamplingHaar := by
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceSamplingLambda, OAI.FiniteFactor.sourceSamplingEndpoint, OAI.FiniteFactor.sourceSamplingHaar

6. theorem OAI.FiniteFactor.sourceSamplingLambda_marginal_density line 52