OAI/Analysis/FiniteFactor/OrbitSampling/LambdaRectangles.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteFactor.sourceSamplingLambdaTest line 10
2. theorem OAI.FiniteFactor.sourceSamplingLambdaTest_measurable line 15
3. theorem OAI.FiniteFactor.sourceSamplingLambdaTest_iff line 26

   Source documentation

   The finite coordinate conditions are equivalent to restriction by the triangle and the full cylinder rectangle on the conull Haar cube.

   theorem sourceSamplingLambdaTest_iff (I : Finset SourceCoordinate) (T : SourceSamplingRationalTest)
       (p : SourceCoordinate → ℝ × ℝ)
       (hp : ∀ i, (p i).1 ∈ Set.Ico (0 : ℝ) 1 ∧ (p i).2 ∈ Set.Ico (0 : ℝ) 1) :
       (∀ i ∈ I ∪ T.1, sourceSamplingLambdaTest I T i (p i)) ↔
         sourceSamplingLimitMap I p ∈ sourceSamplingRectangle (sourceSamplingRationalX T) (sourceSamplingRationalY T) ∧
         p ∈ sourceSamplingTriangleSet I := by
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceSamplingRationalTest, OAI.FiniteFactor.sourceSamplingLambdaTest, OAI.FiniteFactor.sourceSamplingLimitMap, OAI.FiniteFactor.sourceSamplingRectangle, OAI.FiniteFactor.sourceSamplingRationalX, OAI.FiniteFactor.sourceSamplingRationalY, OAI.FiniteFactor.sourceSamplingTriangleSet

4. theorem OAI.FiniteFactor.sourceSamplingLambda_rectangle line 59

   Source documentation

   The constructed infinite-coordinate measure has exactly the rectangle values previously obtained as sampling limits.

   theorem sourceSamplingLambda_rectangle (I : Finset SourceCoordinate) (T : SourceSamplingRationalTest) :
       ((sourceSamplingLambda I)
         (sourceSamplingRectangle (sourceSamplingRationalX T) (sourceSamplingRationalY T))).toReal =
         sourceSamplingLimitRectangleMass I T := by
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceSamplingRationalTest, OAI.FiniteFactor.sourceSamplingLambda, OAI.FiniteFactor.sourceSamplingRectangle, OAI.FiniteFactor.sourceSamplingRationalX, OAI.FiniteFactor.sourceSamplingRationalY, OAI.FiniteFactor.sourceSamplingLimitRectangleMass

5. theorem OAI.FiniteFactor.sourceSamplingLambda_rectangle_limit_event line 108

   Source documentation

   Actual untrimmed measures converge to the actual source limiting measure on every rational cylinder rectangle, on a single conull event.

   theorem sourceSamplingLambda_rectangle_limit_event :
       ∀ᵐ θ ∂sourceAngleLaw, ∀ (I : Finset SourceCoordinate) (T : SourceSamplingRationalTest),
         Tendsto (fun stage => ((sourceSamplingUntrimmed I stage θ)
           (sourceSamplingRectangle (sourceSamplingRationalX T) (sourceSamplingRationalY T))).toReal)
           atTop (𝓝 (((sourceSamplingLambda I)
             (sourceSamplingRectangle (sourceSamplingRationalX T) (sourceSamplingRationalY T))).toReal)) := by
   …

   Mentions: OAI.FiniteFactor.sourceAngleLaw, OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceSamplingRationalTest, OAI.FiniteFactor.sourceSamplingUntrimmed, OAI.FiniteFactor.sourceSamplingRectangle, OAI.FiniteFactor.sourceSamplingRationalX, OAI.FiniteFactor.sourceSamplingRationalY, OAI.FiniteFactor.sourceSamplingLambda