RectangleApproximation.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.FiniteFactor.sourceSampling_rectangle_approximation_event line 13
Source documentation
Actual rational rectangle masses approach their ideal product integrals on a single conull event. This is the stochastic approximation step; the identification of the ideal limiting law is a separate obligation.
```
theorem sourceSampling_rectangle_approximation_event :
    ∀ᵐ θ ∂sourceAngleLaw, ∀ (I : Finset SourceCoordinate) (T : SourceSamplingRationalTest),
      Tendsto (fun stage =>
        ((sourceSamplingUntrimmed I stage θ)
          (sourceSamplingRectangle (sourceSamplingRationalX T) (sourceSamplingRationalY T))).toReal -
        ∫ x, sourceSamplingIdealDensity stage false (fun i => decide (i ∈ I))
          (sourceSamplingRationalX T) (sourceSamplingRationalY T) x ∂sourceSamplingHaar)
      atTop (𝓝 0) := 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.sourceSamplingIdealDensity, OAI.FiniteFactor.sourceSamplingHaar