Documentation

Papers.AnsariRockel2024.Gaussian

← Mathematical handbook

Gaussian family: admissible parameters, benchmark members and source domain check #

theorem Papers.AnsariRockel2024.gaussian_correlation_admissible (r : ℝ) :

(Verification.bivariateCorrelation r).PosSemidef ↔ r ∈ Set.Icc (-1) 1

theorem Papers.AnsariRockel2024.gaussian_zero :

Verification.gaussianBivariate 0 ⋯ = ProbabilityTheory.Copula.independence 2

theorem Papers.AnsariRockel2024.gaussian_one :

Verification.gaussianBivariate 1 ⋯ = ProbabilityTheory.Copula.comonotonic 2

theorem Papers.AnsariRockel2024.gaussian_symmetric {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) :

(Verification.gaussianBivariate r hr).transpose = Verification.gaussianBivariate r hr

theorem Papers.AnsariRockel2024.gaussian_zero_association :

(Verification.gaussianBivariate 0 ⋯).spearmanRho = 0 ∧ (Verification.gaussianBivariate 0 ⋯).kendallTau = 0 ∧ (Verification.gaussianBivariate 0 ⋯).chatterjeeXi = 0

theorem Papers.AnsariRockel2024.gaussian_one_association :

(Verification.gaussianBivariate 1 ⋯).spearmanRho = 1 ∧ (Verification.gaussianBivariate 1 ⋯).kendallTau = 1 ∧ (Verification.gaussianBivariate 1 ⋯).chatterjeeXi = 1

theorem Papers.AnsariRockel2024.gaussian_printed_xi_argument_outside_domain {r : ℝ} (hr : r ∈ Set.Ioo (-1) (-(1 / 2))) :

1 < Verification.gaussianPrintedXiArgument r

theorem Papers.AnsariRockel2024.gaussian_printed_xi_argument_counterexample :

Verification.gaussianPrintedXiArgument (-(3 / 4)) = 11 / 4 ∧ Verification.gaussianPrintedXiArgument (-(3 / 4)) ∉ Set.Icc (-1) 1

theorem Papers.AnsariRockel2024.gaussian_neg {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) :

Verification.gaussianBivariate (-r) ⋯ = (Verification.gaussianBivariate r hr).reflect {1}

theorem Papers.AnsariRockel2024.gaussian_negative_one :

Verification.gaussianBivariate (-1) ⋯ = ProbabilityTheory.Copula.countermonotonic

theorem Papers.AnsariRockel2024.gaussian_negative_one_association :

(Verification.gaussianBivariate (-1) ⋯).spearmanRho = -1 ∧ (Verification.gaussianBivariate (-1) ⋯).kendallTau = -1 ∧ (Verification.gaussianBivariate (-1) ⋯).chatterjeeXi = 1

theorem Papers.AnsariRockel2024.gaussian_xi_neg {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) :

(Verification.gaussianBivariate (-r) ⋯).chatterjeeXi = (Verification.gaussianBivariate r hr).chatterjeeXi

theorem Papers.AnsariRockel2024.gaussian_rho_neg {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) :

(Verification.gaussianBivariate (-r) ⋯).spearmanRho = -(Verification.gaussianBivariate r hr).spearmanRho

theorem Papers.AnsariRockel2024.gaussian_tau_neg {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) :

(Verification.gaussianBivariate (-r) ⋯).kendallTau = -(Verification.gaussianBivariate r hr).kendallTau

theorem Papers.AnsariRockel2024.gaussian_printed_xi_formula_false :

¬∀ (r : ℝ) (hr : r ∈ Set.Icc (-1) 1), (Verification.gaussianBivariate r hr).chatterjeeXi = Verification.gaussianPrintedXi r

theorem Papers.AnsariRockel2024.gaussian_toMeasure_independent {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) :

(Verification.gaussianBivariate r hr).toMeasure = MeasureTheory.Measure.map (fun (x : Fin 2 → ℝ) => ![ProbabilityTheory.cdfUnit (ProbabilityTheory.gaussianReal 0 1) (x 0), ProbabilityTheory.cdfUnit (ProbabilityTheory.gaussianReal 0 1) (r * x 0 + √(1 - r ^ 2) * x 1)]) (MeasureTheory.Measure.pi fun (x : Fin 2) => ProbabilityTheory.gaussianReal 0 1)

theorem Papers.AnsariRockel2024.gaussian_rho_normal_integral {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) :

(Verification.gaussianBivariate r hr).spearmanRho = (12 * ∫ (x : Fin 2 → ℝ), ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) (x 0) * ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) (r * x 0 + √(1 - r ^ 2) * x 1) ∂MeasureTheory.Measure.pi fun (x : Fin 2) => ProbabilityTheory.gaussianReal 0 1) - 3

theorem Papers.AnsariRockel2024.gaussian_wedge_probability {a : ℝ} (ha : 0 ≤ a) :

∫ (x : ℝ) in Set.Ioi 0, ∫ (y : ℝ) in Set.Ioi 0, if y ≤ a * x then 1 else 0 ∂ProbabilityTheory.gaussianReal 0 1 ∂ProbabilityTheory.gaussianReal 0 1 = Real.arctan a / (2 * Real.pi)

theorem Papers.AnsariRockel2024.gaussian_halfline_cdf_integral (a : ℝ) :

∫ (x : ℝ) in Set.Ioi 0, ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) (a * x) ∂ProbabilityTheory.gaussianReal 0 1 = 1 / 4 + Real.arctan a / (2 * Real.pi)

theorem Papers.AnsariRockel2024.gaussian_kendallTau {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) :

(Verification.gaussianBivariate r hr).kendallTau = 2 / Real.pi * Real.arcsin r

theorem Papers.AnsariRockel2024.gaussian_spearmanRho {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) :

(Verification.gaussianBivariate r hr).spearmanRho = 6 / Real.pi * Real.arcsin (r / 2)

theorem Papers.AnsariRockel2024.gaussian_cdf_normal {r : ℝ} (hr : r ∈ Set.Ioo (-1) 1) (a b : ℝ) :

(Verification.gaussianBivariate r ⋯).cdf ![ProbabilityTheory.cdfUnit (ProbabilityTheory.gaussianReal 0 1) a, ProbabilityTheory.cdfUnit (ProbabilityTheory.gaussianReal 0 1) b] = ∫ (x : ℝ) in Set.Iic a, ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) ((b - r * x) / √(1 - r ^ 2)) ∂ProbabilityTheory.gaussianReal 0 1

theorem Papers.AnsariRockel2024.gaussian_conditionalCDF_normal {r : ℝ} (hr : r ∈ Set.Ioo (-1) 1) (b : ℝ) :

(fun (x : ℝ) => (Verification.gaussianBivariate r ⋯).conditionalCDF (ProbabilityTheory.cdfUnit (ProbabilityTheory.gaussianReal 0 1) x) (ProbabilityTheory.cdfUnit (ProbabilityTheory.gaussianReal 0 1) b)) =ᵐ[ProbabilityTheory.gaussianReal 0 1] fun (x : ℝ) => ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) ((b - r * x) / √(1 - r ^ 2))

theorem Papers.AnsariRockel2024.gaussian_xi_normal_integral {r : ℝ} (hr : r ∈ Set.Ioo (-1) 1) :

(Verification.gaussianBivariate r ⋯).chatterjeeXi = 6 * ∫ (b : ℝ), ∫ (x : ℝ), ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) ((b - r * x) / √(1 - r ^ 2)) ^ 2 ∂ProbabilityTheory.gaussianReal 0 1 ∂ProbabilityTheory.gaussianReal 0 1 - 2

theorem Papers.AnsariRockel2024.gaussian_chatterjeeXi {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) :

(Verification.gaussianBivariate r hr).chatterjeeXi = 3 / Real.pi * Real.arcsin ((1 + r ^ 2) / 2) - 1 / 2

theorem Papers.AnsariRockel2024.gaussian_conditionalCDF_quantile {r : ℝ} (hr : r ∈ Set.Ioo (-1) 1) {v : ↑unitInterval} (hv : ↑v ∈ Set.Ioo 0 1) :

(fun (u : ↑unitInterval) => (Verification.gaussianBivariate r ⋯).conditionalCDF u v) =ᵐ[MeasureTheory.volume] Verification.gaussianQuantileConditional r v

theorem Papers.AnsariRockel2024.gaussian_conditional_antitoneOn {r : ℝ} (hr : 0 ≤ r) (v : ↑unitInterval) :

AntitoneOn (Verification.gaussianQuantileConditional r v) {u : ↑unitInterval | ↑u ∈ Set.Ioo 0 1}

theorem Papers.AnsariRockel2024.gaussian_conditional_monotoneOn {r : ℝ} (hr : r ≤ 0) (v : ↑unitInterval) :

MonotoneOn (Verification.gaussianQuantileConditional r v) {u : ↑unitInterval | ↑u ∈ Set.Ioo 0 1}

theorem Papers.AnsariRockel2024.gaussian_isCI_iff {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) :

(Verification.gaussianBivariate r hr).IsCI ↔ 0 ≤ r

theorem Papers.AnsariRockel2024.gaussian_isCD_iff {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) :

(Verification.gaussianBivariate r hr).IsCD ↔ r ≤ 0

theorem Papers.AnsariRockel2024.gaussian_isPQD_iff {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) :

(Verification.gaussianBivariate r hr).IsPQD ↔ 0 ≤ r

theorem Papers.AnsariRockel2024.gaussian_isNQD_iff {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) :

(Verification.gaussianBivariate r hr).IsNQD ↔ r ≤ 0

theorem Papers.AnsariRockel2024.gaussian_absolutelyContinuous_iff {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) :

(Verification.gaussianBivariate r hr).toMeasure.AbsolutelyContinuous MeasureTheory.volume ↔ r ∈ Set.Ioo (-1) 1

theorem Papers.AnsariRockel2024.gaussian_toMeasure_normal_density {r : ℝ} (hr : r ∈ Set.Ioo (-1) 1) :

(Verification.gaussianBivariate r ⋯).toMeasure = MeasureTheory.Measure.map (fun (p : ℝ × ℝ) => ![ProbabilityTheory.cdfUnit (ProbabilityTheory.gaussianReal 0 1) p.1, ProbabilityTheory.cdfUnit (ProbabilityTheory.gaussianReal 0 1) p.2]) (MeasureTheory.volume.withDensity fun (p : ℝ × ℝ) => ProbabilityTheory.gaussianPDF 0 1 p.1 * ProbabilityTheory.gaussianPDF (r * p.1) (1 - r ^ 2).toNNReal p.2)

theorem Papers.AnsariRockel2024.gaussian_density {r : ℝ} (hr : r ∈ Set.Ioo (-1) 1) :

(Verification.gaussianBivariate r ⋯).toMeasure = MeasureTheory.volume.withDensity fun (u : Fin 2 → ↑unitInterval) => ENNReal.ofReal (Verification.gaussianCopulaDensity r u)

theorem Papers.AnsariRockel2024.gaussian_hasMTP2Density_iff {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) :

(Verification.gaussianBivariate r hr).HasMTP2Density ↔ 0 ≤ r ∧ r < 1

theorem Papers.AnsariRockel2024.gaussian_radiallySymmetric {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) :

(Verification.gaussianBivariate r hr).IsRadiallySymmetric

theorem Papers.AnsariRockel2024.gaussian_lowerTail {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) :

(Verification.gaussianBivariate r hr).HasLowerTailDependence (if r = 1 then 1 else 0)

theorem Papers.AnsariRockel2024.gaussian_upperTail {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) :

(Verification.gaussianBivariate r hr).HasUpperTailDependence (if r = 1 then 1 else 0)

theorem Papers.AnsariRockel2024.gaussian_lowerOrthant_iff {r s : ℝ} (hr : r ∈ Set.Icc (-1) 1) (hs : s ∈ Set.Icc (-1) 1) :

(Verification.gaussianBivariate r hr).LowerOrthantLE (Verification.gaussianBivariate s hs) ↔ r ≤ s

theorem Papers.AnsariRockel2024.gaussian_schur_iff {r s : ℝ} (hr : r ∈ Set.Icc (-1) 1) (hs : s ∈ Set.Icc (-1) 1) :

(Verification.gaussianBivariate r hr).SchurLE (Verification.gaussianBivariate s hs) ↔ |r| ≤ |s|

theorem Papers.AnsariRockel2024.gaussian_schurBoth_iff {r s : ℝ} (hr : r ∈ Set.Icc (-1) 1) (hs : s ∈ Set.Icc (-1) 1) :

(Verification.gaussianBivariate r hr).SchurBothLE (Verification.gaussianBivariate s hs) ↔ |r| ≤ |s|

theorem Papers.AnsariRockel2024.gaussian_cdf_continuous (u : Fin 2 → ↑unitInterval) :

Continuous fun (r : ↑(Set.Icc (-1) 1)) => (Verification.gaussianBivariate ↑r ⋯).cdf u

theorem Papers.AnsariRockel2024.gaussian_cdf_tendsto_zero (u : Fin 2 → ↑unitInterval) :

Filter.Tendsto (fun (r : ↑(Set.Icc (-1) 1)) => (Verification.gaussianBivariate ↑r ⋯).cdf u) (nhds ⟨0, ⋯⟩) (nhds ((ProbabilityTheory.Copula.independence 2).cdf u))

theorem Papers.AnsariRockel2024.gaussian_cdf_tendsto_one (u : Fin 2 → ↑unitInterval) :

Filter.Tendsto (fun (r : ↑(Set.Icc (-1) 1)) => (Verification.gaussianBivariate ↑r ⋯).cdf u) (nhds ⟨1, ⋯⟩) (nhds ((ProbabilityTheory.Copula.comonotonic 2).cdf u))

theorem Papers.AnsariRockel2024.gaussian_cdf_tendsto_negative_one (u : Fin 2 → ↑unitInterval) :

Filter.Tendsto (fun (r : ↑(Set.Icc (-1) 1)) => (Verification.gaussianBivariate ↑r ⋯).cdf u) (nhds ⟨-1, ⋯⟩) (nhds (ProbabilityTheory.Copula.countermonotonic.cdf u))

theorem Papers.AnsariRockel2024.gaussian_negative_one_not_lowerTail_one :

¬(Verification.gaussianBivariate (-1) ⋯).HasLowerTailDependence 1

theorem Papers.AnsariRockel2024.gaussian_negative_one_not_upperTail_one :

¬(Verification.gaussianBivariate (-1) ⋯).HasUpperTailDependence 1