noncomputable def
Verification.sampleCheckerboardEstimator
{Ω : Type u_1}
(X : ℕ → Ω → Fin 2 → ↑unitInterval)
(κ : ℝ)
(n : ℕ)
(ω : Ω)
:
The sample size is n+1; the grid order is exactly floor((n+1)^κ).
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Verification.sampleCheckerboardEstimator_ae_tendsto
{Ω : Type u_1}
[MeasurableSpace Ω]
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsProbabilityMeasure μ]
(C : ProbabilityTheory.Copula 2)
(X : ℕ → Ω → Fin 2 → ↑unitInterval)
(hX : ∀ (i : ℕ), Measurable (X i))
(hI : ProbabilityTheory.iIndepFun X μ)
(hlaw : ∀ (i : ℕ), MeasureTheory.Measure.map (X i) μ = C.toMeasure)
(κ : ℝ)
(hκ : 0 < κ)
(hκ' : κ ≤ 1 / 3)
:
∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => sampleCheckerboardEstimator X κ n ω) Filter.atTop (nhds C.chatterjeeXi)
Almost-sure consistency of the rank-based checkerboard estimator, proved from independence and the actual sampling law.