Papers.AnsariRockel2024.Raftery

theorem Papers.AnsariRockel2024.raftery_printed_cdf_not_copula :

¬∃ (C : ProbabilityTheory.Copula 2), ∀ (u v : ↑unitInterval), C.cdf ![u, v] = Verification.rafteryPrintedCDF (1 / 2) ↑u ↑v

The literal arXiv v3 Table 1 formula fails a necessary copula bound.

source

theorem Papers.AnsariRockel2024.raftery_zero_density {C : ProbabilityTheory.Copula 2} (hC : C = ProbabilityTheory.Copula.independence 2) :

C.HasMTP2Density

Endpoint consequence of Table 4's independence identity; no interior constructor is assumed.

source

theorem Papers.AnsariRockel2024.raftery_one_upperTail {C : ProbabilityTheory.Copula 2} (hC : C = ProbabilityTheory.Copula.comonotonic 2) :

C.HasUpperTailDependence 1 ∧ ¬C.HasUpperTailDependence 0

Endpoint consequence of Table 4's comonotonic identity; the zero upper tail excludes it.

source

theorem Papers.AnsariRockel2024.raftery_cdf (δ : ↑unitInterval) (h1 : δ ≠ 1) (u v : ↑unitInterval) :

(Verification.raftery δ).cdf ![u, v] = min ↑u ↑v + (1 - ↑δ) / (1 + ↑δ) * (↑u * ↑v) ^ (1 / (1 - ↑δ)) * (1 - max ↑u ↑v ^ (-(1 + ↑δ) / (1 - ↑δ)))

Actual copula CDF, with the missing factor 1/(1+delta) restored.

source

theorem Papers.AnsariRockel2024.raftery_zero :

Verification.raftery 0 = ProbabilityTheory.Copula.independence 2

source

theorem Papers.AnsariRockel2024.raftery_one :

Verification.raftery 1 = ProbabilityTheory.Copula.comonotonic 2

source

theorem Papers.AnsariRockel2024.raftery_tails_lt_one (δ : ↑unitInterval) (h1 : δ ≠ 1) :

(Verification.raftery δ).HasLowerTailDependence (2 * ↑δ / (1 + ↑δ)) ∧ (Verification.raftery δ).HasUpperTailDependence 0

source

theorem Papers.AnsariRockel2024.raftery_tails_one :

(Verification.raftery 1).HasLowerTailDependence 1 ∧ (Verification.raftery 1).HasUpperTailDependence 1

source

theorem Papers.AnsariRockel2024.raftery_comonotonic_bounds (δ u v : ↑unitInterval) :

min ↑u ↑v - (1 - ↑δ) ≤ (Verification.raftery δ).cdf ![u, v] ∧ (Verification.raftery δ).cdf ![u, v] ≤ min ↑u ↑v

source

theorem Papers.AnsariRockel2024.raftery_tendsto_parameter {A : Type u_1} {l : Filter A} (δ : A → ↑unitInterval) (η : ↑unitInterval) (hδ : Filter.Tendsto (fun (x : A) => ↑(δ x)) l (nhds ↑η)) (u v : ↑unitInterval) :

Filter.Tendsto (fun (x : A) => (Verification.raftery (δ x)).cdf ![u, v]) l (nhds ((Verification.raftery η).cdf ![u, v]))

source

theorem Papers.AnsariRockel2024.raftery_tendsto_zero {A : Type u_1} {l : Filter A} (δ : A → ↑unitInterval) (hδ : Filter.Tendsto (fun (x : A) => ↑(δ x)) l (nhds 0)) (u v : ↑unitInterval) :

Filter.Tendsto (fun (x : A) => (Verification.raftery (δ x)).cdf ![u, v]) l (nhds ((ProbabilityTheory.Copula.independence 2).cdf ![u, v]))

source

theorem Papers.AnsariRockel2024.raftery_tendsto_one {A : Type u_1} {l : Filter A} (δ : A → ↑unitInterval) (hδ : Filter.Tendsto (fun (x : A) => ↑(δ x)) l (nhds 1)) (u v : ↑unitInterval) :

Filter.Tendsto (fun (x : A) => (Verification.raftery (δ x)).cdf ![u, v]) l (nhds ((ProbabilityTheory.Copula.comonotonic 2).cdf ![u, v]))

source

theorem Papers.AnsariRockel2024.raftery_spearmanRho (δ : ↑unitInterval) :

(Verification.raftery δ).spearmanRho = ↑δ * (4 - 3 * ↑δ) / (2 - ↑δ) ^ 2

source

theorem Papers.AnsariRockel2024.raftery_density (δ : ↑unitInterval) (h1 : δ ≠ 1) :

(Verification.raftery δ).toMeasure = MeasureTheory.volume.withDensity fun (x : Fin 2 → ↑unitInterval) => ENNReal.ofReal (Verification.rafteryDensity (1 / (1 - ↑δ)) ↑(x 0) ↑(x 1))

source

theorem Papers.AnsariRockel2024.raftery_absolutelyContinuous_iff (δ : ↑unitInterval) :

(Verification.raftery δ).toMeasure.AbsolutelyContinuous MeasureTheory.volume ↔ δ ≠ 1

source

theorem Papers.AnsariRockel2024.raftery_density_tp2_iff (δ : ↑unitInterval) :

(Verification.raftery δ).HasMTP2Density ↔ δ ≠ 1

source

theorem Papers.AnsariRockel2024.raftery_ci (δ : ↑unitInterval) :

(Verification.raftery δ).IsCI

source

theorem Papers.AnsariRockel2024.raftery_pqd (δ : ↑unitInterval) :

(Verification.raftery δ).IsPQD

source

theorem Papers.AnsariRockel2024.raftery_nqd_iff (δ : ↑unitInterval) :

(Verification.raftery δ).IsNQD ↔ δ = 0

source

theorem Papers.AnsariRockel2024.raftery_cd_iff (δ : ↑unitInterval) :

(Verification.raftery δ).IsCD ↔ δ = 0

source

theorem Papers.AnsariRockel2024.raftery_printed_tp2_exclusion_false :

¬∀ (δ : ↑unitInterval), Verification.raftery δ ≠ ProbabilityTheory.Copula.independence 2 → ¬(Verification.raftery δ).HasMTP2Density

source

theorem Papers.AnsariRockel2024.raftery_lowerOrthant_monotone {δ η : ↑unitInterval} (hδη : δ ≤ η) :

(Verification.raftery δ).LowerOrthantLE (Verification.raftery η)

source

theorem Papers.AnsariRockel2024.raftery_schur_monotone {δ η : ↑unitInterval} (hδη : δ ≤ η) :

(Verification.raftery δ).SchurBothLE (Verification.raftery η)

source

theorem Papers.AnsariRockel2024.raftery_kendallTau (δ : ↑unitInterval) :

(Verification.raftery δ).kendallTau = 2 * ↑δ / (3 - ↑δ)