ErrorEvent.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.FiniteFactor.sourceSamplingCorrelationBudget_summable line 11
Source documentation
The distinct and mixed error budget is summable along the actual stages.
```
theorem sourceSamplingCorrelationBudget_summable : Summable sourceSamplingCorrelationBudget := by
…
```
Mentions: OAI.FiniteFactor.sourceSamplingCorrelationBudget

theorem OAI.FiniteFactor.sourceSamplingSquaredError_summable_integral line 35

Source documentation

Summable expectations for the full empirical sampling error.

theorem sourceSamplingSquaredError_summable_integral (r : Bool) (b : SourceCoordinate → Bool)
    (a c a' c' : SourceCoordinate → ℝ) :
    Summable (fun stage => ∫ θ, sourceSamplingSquaredError stage r b
      (fun i => Set.Icc (a i) (c i)) (fun i => Set.Icc (a' i) (c' i)) θ ∂sourceAngleLaw) := by
…

Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceSamplingSquaredError, OAI.FiniteFactor.sourceAngleLaw

theorem OAI.FiniteFactor.sourceSamplingSquaredError_ae line 50

Source documentation

The full squared sampling error is summable and converges to zero on a conull set of actual source angles. This is not just the self-pair event.

theorem sourceSamplingSquaredError_ae (r : Bool) (b : SourceCoordinate → Bool)
    (a c a' c' : SourceCoordinate → ℝ) :
    ∀ᵐ θ ∂sourceAngleLaw,
      Summable (fun stage => sourceSamplingSquaredError stage r b
        (fun i => Set.Icc (a i) (c i)) (fun i => Set.Icc (a' i) (c' i)) θ) ∧
      Tendsto (fun stage => sourceSamplingSquaredError stage r b
        (fun i => Set.Icc (a i) (c i)) (fun i => Set.Icc (a' i) (c' i)) θ) atTop (𝓝 0) := by
…

Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceAngleLaw, OAI.FiniteFactor.sourceSamplingSquaredError

theorem OAI.FiniteFactor.sourceSamplingSquaredError_countable_event line 67

Source documentation

One source-angle event handles any countable family of interval tests, orientations and triangular-coordinate choices for the full error.

theorem sourceSamplingSquaredError_countable_event {ι : Type*} [Countable ι]
    (r : ι → Bool) (b : ι → SourceCoordinate → Bool)
    (a c a' c' : ι → SourceCoordinate → ℝ) :
    ∀ᵐ θ ∂sourceAngleLaw, ∀ j,
      Summable (fun stage => sourceSamplingSquaredError stage (r j) (b j)
        (fun i => Set.Icc (a j i) (c j i)) (fun i => Set.Icc (a' j i) (c' j i)) θ) ∧
      Tendsto (fun stage => sourceSamplingSquaredError stage (r j) (b j)
        (fun i => Set.Icc (a j i) (c j i)) (fun i => Set.Icc (a' j i) (c' j i)) θ) atTop (𝓝 0) :=
…

Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceAngleLaw, OAI.FiniteFactor.sourceSamplingSquaredError