OAI/Analysis/FiniteFactor/OrbitSampling/WeakLimit.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteFactor.sourceSamplingUntrimmedFinite line 11
2. def OAI.FiniteFactor.sourceSamplingLambdaFinite line 15
3. theorem OAI.FiniteFactor.sourceSamplingCylinder_mass_eq line 18
4. theorem OAI.FiniteFactor.sourceSamplingUntrimmed_weak_event line 29

   Source documentation

   Actual finite measures converge weakly on the full real product. The normalization and total-mass obligations are discharged by the empty test; the original full sampling error is retained through the rectangle event.

   theorem sourceSamplingUntrimmed_weak_event : ∀ᵐ θ ∂sourceAngleLaw,
       ∀ I : Finset SourceCoordinate,
         Tendsto (fun s => sourceSamplingUntrimmedFinite I s θ) atTop
           (𝓝 (sourceSamplingLambdaFinite I)) := by
   …

   Mentions: OAI.FiniteFactor.sourceAngleLaw, OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceSamplingUntrimmedFinite, OAI.FiniteFactor.sourceSamplingLambdaFinite