← Mathematical handbook

noncomputable def Verification.realSampleRankCopula {Ω : Type u_1} (X : ℕ → Ω → Fin 2 → ℝ) (n : ℕ) (ω : Ω) : ProbabilityTheory.Copula 2

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Verification.realSampleCheckerboardEstimator {Ω : Type u_1} (X : ℕ → Ω → Fin 2 → ℝ) (κ : ℝ) (n : ℕ) (ω : Ω) : ℝ

Equations

• One or more equations did not get rendered due to their size.

theorem Verification.realSampleRankCopula_transform {Ω : Type u_1} (ν : MeasureTheory.ProbabilityMeasure (Fin 2 → ℝ)) (X : ℕ → Ω → Fin 2 → ℝ) (n : ℕ) (ω : Ω) (hi : ∀ (d : Fin 2), Function.Injective fun (i : Fin (n + 1)) => ProbabilityTheory.Copula.marginalTransform ν (X (↑i) ω) d) : realSampleRankCopula X n ω = sampleRankCopula (fun (i : ℕ) (ω : Ω) => ProbabilityTheory.Copula.marginalTransform ν (X i ω)) n ω

The probability integral transform leaves sample ranks unchanged, including continuous marginal CDFs with flat intervals.

theorem Verification.realSampleCheckerboardEstimator_ae_tendsto {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (ν : MeasureTheory.ProbabilityMeasure (Fin 2 → ℝ)) (hc : ∀ (d : Fin 2), Continuous ↑(ProbabilityTheory.cdf (ProbabilityTheory.Copula.marginal ν d))) (X : ℕ → Ω → Fin 2 → ℝ) (hX : ∀ (i : ℕ), Measurable (X i)) (hI : ProbabilityTheory.iIndepFun X μ) (hlaw : ∀ (i : ℕ), MeasureTheory.Measure.map (X i) μ = ↑ν) (κ : ℝ) (hκ : 0 < κ) (hκ' : κ ≤ 1 / 3) : ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => realSampleCheckerboardEstimator X κ n ω) Filter.atTop (nhds (ProbabilityTheory.Copula.ofContinuousMarginals ν hc).chatterjeeXi)

Theorem 4.5 statistical conclusion for real observations with continuous marginal CDFs. The estimator uses the original data ranks.