IdealRectangleLimit.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

def OAI.FiniteFactor.sourceSamplingLimitRectangleMass line 13
Source documentation
Explicit finite-coordinate rectangle mass of the triangular/diagonal model. The triangular term retains the actual source weight integral.
```
def sourceSamplingLimitRectangleMass (I : Finset SourceCoordinate) (T : SourceSamplingRationalTest) : ℝ :=
…
```
Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceSamplingRationalTest

theorem OAI.FiniteFactor.sourceSamplingIdealDensity_integral line 21

Source documentation

Exact finite-coordinate factorization of the first ideal integral.

theorem sourceSamplingIdealDensity_integral (I : Finset SourceCoordinate) (stage : ℕ)
    (E G : SourceCoordinate → Set ℝ) (hE : ∀ i, MeasurableSet (E i)) (hG : ∀ i, MeasurableSet (G i)) :
    (∫ x, sourceSamplingIdealDensity stage false (fun i => decide (i ∈ I)) E G x ∂sourceSamplingHaar) =
      ∏ i ∈ sourceSamplingPrefix stage, ∫ s,
        samplingTestedFirstDensity (decide (i ∈ I)) (sourceSamplingWidth stage) (sourceSamplingCutoff stage)
          (E i) (G i) s ∂unitIntervalMeasure := by
…

Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceSamplingIdealDensity, OAI.FiniteFactor.sourceSamplingHaar, OAI.FiniteFactor.sourceSamplingPrefix, OAI.FiniteFactor.samplingTestedFirstDensity, OAI.FiniteFactor.sourceSamplingWidth, OAI.FiniteFactor.sourceSamplingCutoff, OAI.FiniteFactor.unitIntervalMeasure

theorem OAI.FiniteFactor.sourceSamplingIdeal_rectangle_split line 32

Source documentation

Tests and triangular coordinates occupy a fixed finite set. Every other prefix coordinate contributes its exact retained mass, 1-2α.

theorem sourceSamplingIdeal_rectangle_split (I : Finset SourceCoordinate) (T : SourceSamplingRationalTest)
    (stage : ℕ) (hK : I ∪ T.1 ⊆ sourceSamplingPrefix stage) :
    (∫ x, sourceSamplingIdealDensity stage false (fun i => decide (i ∈ I))
      (sourceSamplingRationalX T) (sourceSamplingRationalY T) x ∂sourceSamplingHaar) =
    (∏ i ∈ I ∪ T.1, ∫ s,
      samplingTestedFirstDensity (decide (i ∈ I)) (sourceSamplingWidth stage) (sourceSamplingCutoff stage)
        (sourceSamplingRationalX T i) (sourceSamplingRationalY T i) s ∂unitIntervalMeasure) *
    (1-2*sourceSamplingCutoff stage)^((sourceSamplingPrefix stage \ (I ∪ T.1)).card) := by
…

Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceSamplingRationalTest, OAI.FiniteFactor.sourceSamplingPrefix, OAI.FiniteFactor.sourceSamplingIdealDensity, OAI.FiniteFactor.sourceSamplingRationalX, OAI.FiniteFactor.sourceSamplingRationalY, OAI.FiniteFactor.sourceSamplingHaar, OAI.FiniteFactor.samplingTestedFirstDensity, OAI.FiniteFactor.sourceSamplingWidth, OAI.FiniteFactor.sourceSamplingCutoff, OAI.FiniteFactor.unitIntervalMeasure

theorem OAI.FiniteFactor.sourceSamplingIdeal_rectangle_tendsto line 58
Source documentation
The deterministic ideal product limit includes all growing-prefix cutoff losses and has exactly the tested diagonal-coordinate limits.
```
theorem sourceSamplingIdeal_rectangle_tendsto (I : Finset SourceCoordinate) (T : SourceSamplingRationalTest) :
    Tendsto (fun stage => ∫ x, sourceSamplingIdealDensity stage false (fun i => decide (i ∈ I))
      (sourceSamplingRationalX T) (sourceSamplingRationalY T) x ∂sourceSamplingHaar)
      atTop (𝓝 (sourceSamplingLimitRectangleMass I T)) := by
…
```
Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceSamplingRationalTest, OAI.FiniteFactor.sourceSamplingIdealDensity, OAI.FiniteFactor.sourceSamplingRationalX, OAI.FiniteFactor.sourceSamplingRationalY, OAI.FiniteFactor.sourceSamplingHaar, OAI.FiniteFactor.sourceSamplingLimitRectangleMass
theorem OAI.FiniteFactor.sourceSampling_rectangle_limit_event line 92
Source documentation
Actual untrimmed rational rectangle masses converge to the explicit triangular/diagonal product value on one conull event for all I and tests.
```
theorem sourceSampling_rectangle_limit_event :
    ∀ᵐ θ ∂sourceAngleLaw, ∀ (I : Finset SourceCoordinate) (T : SourceSamplingRationalTest),
      Tendsto (fun stage => ((sourceSamplingUntrimmed I stage θ)
        (sourceSamplingRectangle (sourceSamplingRationalX T) (sourceSamplingRationalY T))).toReal)
        atTop (𝓝 (sourceSamplingLimitRectangleMass I T)) := 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.sourceSamplingLimitRectangleMass