OAI/Analysis/FiniteFactor/OrbitSampling/Cube.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.FiniteFactor.SourceSamplingPair line 10
2. def OAI.FiniteFactor.sourceSamplingCube line 12
3. theorem OAI.FiniteFactor.sourceSamplingCube_measurable line 15
4. instance OAI.FiniteFactor.sourceSamplingUntrimmed_finite line 18
5. theorem OAI.FiniteFactor.sourceSamplingSummand_cube line 25
6. theorem OAI.FiniteFactor.sourceSamplingUntrimmed_cube line 36
7. theorem OAI.FiniteFactor.sourceSamplingLambda_cube line 45
8. def OAI.FiniteFactor.sourceSamplingEmptyTest line 56
9. theorem OAI.FiniteFactor.sourceSamplingEmptyTest_rectangle line 58
10. theorem OAI.FiniteFactor.sourceSampling_mass_limit_event line 66

    Source documentation

    The empty rational test gives actual total-mass convergence.

    theorem sourceSampling_mass_limit_event : ∀ᵐ θ ∂sourceAngleLaw,
        ∀ I : Finset SourceCoordinate,
          Tendsto (fun s => ((sourceSamplingUntrimmed I s θ) Set.univ).toReal)
            atTop (𝓝 (((sourceSamplingLambda I) Set.univ).toReal)) := by
    …

    Mentions: OAI.FiniteFactor.sourceAngleLaw, OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceSamplingUntrimmed, OAI.FiniteFactor.sourceSamplingLambda