Documentation

Papers.Rockel2026ExactBlest.ExactBlestUniqueness

← Mathematical handbook

Equality cases for exact-blest-regions.tex.

source
theorem Papers.Rockel2026ExactBlest.copula_eq_of_graph (C D : ProbabilityTheory.Copula 2) (f : ↑unitInterval → ↑unitInterval) (hf : Measurable f) (hc : ∀ᵐ (x : Fin 2 → ↑unitInterval) ∂C.toMeasure, x 1 = f (x 0)) (hd : ∀ᵐ (x : Fin 2 → ↑unitInterval) ∂D.toMeasure, x 1 = f (x 0)) :
C = D

A deterministic graph and its uniform first marginal determine the copula.

source
noncomputable def Papers.Rockel2026ExactBlest.rhoRank (t u : ↑unitInterval) :
↑unitInterval
Equations
Instances For
    source
    theorem Papers.Rockel2026ExactBlest.measurable_rhoRank (t : ↑unitInterval) :
    Measurable (rhoRank t)
    source
    theorem Papers.Rockel2026ExactBlest.rho_contact (t x z : ℝ) (ht : 0 ≤ t) (hx : 0 ≤ x) (hz : 0 ≤ z) (heq : rhoParamPhi t x + rhoParamPsi t z - (x ^ 2 - t * x) * z = 0) :
    z = if x ≤ t then 2 * |x - t / 2| else x
    source
    noncomputable def Papers.Rockel2026ExactBlest.rhoSlack (t : ↑unitInterval) (x : Fin 2 → ↑unitInterval) :
    ℝ
    Equations
    Instances For
      source
      theorem Papers.Rockel2026ExactBlest.rho_support_graph (C : ProbabilityTheory.Copula 2) (t : ↑unitInterval) (hbound : Rockel2026XiBlest.blestNu C - ↑t * C.spearmanRho = 1 - ↑t + ↑t ^ 4 / 4) :
      ∀ᵐ (x : Fin 2 → ↑unitInterval) ∂C.survivalCopula.toMeasure, x 1 = rhoRank t (x 0)
      source
      theorem Papers.Rockel2026ExactBlest.rho_upper_graph (C : ProbabilityTheory.Copula 2) (t : ↑unitInterval) (hr : C.spearmanRho = rhoPosR ↑t) (hn : Rockel2026XiBlest.blestNu C = rhoPosN ↑t) :
      ∀ᵐ (x : Fin 2 → ↑unitInterval) ∂C.survivalCopula.toMeasure, x 1 = rhoRank t (x 0)
      source
      theorem Papers.Rockel2026ExactBlest.rho_positive_unique (C D : ProbabilityTheory.Copula 2) (t : ↑unitInterval) (hc : C.spearmanRho = rhoPosR ↑t) (hnc : Rockel2026XiBlest.blestNu C = rhoPosN ↑t) (hd : D.spearmanRho = rhoPosR ↑t) (hnd : Rockel2026XiBlest.blestNu D = rhoPosN ↑t) :
      C = D
      source
      theorem Papers.Rockel2026ExactBlest.rho_support_unique (C D : ProbabilityTheory.Copula 2) (t : ↑unitInterval) (hc : Rockel2026XiBlest.blestNu C - ↑t * C.spearmanRho = 1 - ↑t + ↑t ^ 4 / 4) (hd : Rockel2026XiBlest.blestNu D - ↑t * D.spearmanRho = 1 - ↑t + ↑t ^ 4 / 4) :
      C = D
      source
      theorem Papers.Rockel2026ExactBlest.rho_upper_unique (C D : ProbabilityTheory.Copula 2) (hr : C.spearmanRho = D.spearmanRho) (hc : Rockel2026XiBlest.blestNu C = rhoBoundary C.spearmanRho) (hd : Rockel2026XiBlest.blestNu D = rhoBoundary D.spearmanRho) :
      C = D
      source
      theorem Papers.Rockel2026ExactBlest.rho_lower_unique (C D : ProbabilityTheory.Copula 2) (hr : C.spearmanRho = D.spearmanRho) (hc : Rockel2026XiBlest.blestNu C = 2 * C.spearmanRho - rhoBoundary C.spearmanRho) (hd : Rockel2026XiBlest.blestNu D = 2 * D.spearmanRho - rhoBoundary D.spearmanRho) :
      C = D
      source
      theorem Papers.Rockel2026ExactBlest.rho_upper_exists_unique (r : ℝ) (hr : r ∈ Set.Icc (-1) 1) :
      ∃! C : ProbabilityTheory.Copula 2, C.spearmanRho = r ∧ Rockel2026XiBlest.blestNu C = rhoBoundary r
      source
      theorem Papers.Rockel2026ExactBlest.rho_lower_exists_unique (r : ℝ) (hr : r ∈ Set.Icc (-1) 1) :
      ∃! C : ProbabilityTheory.Copula 2, C.spearmanRho = r ∧ Rockel2026XiBlest.blestNu C = 2 * r - rhoBoundary r
      source
      theorem Papers.Rockel2026ExactBlest.nu_rho_upper_unique (C D : ProbabilityTheory.Copula 2) (hc : Rockel2026XiBlest.blestNu C - C.spearmanRho = 1 / 4) (hd : Rockel2026XiBlest.blestNu D - D.spearmanRho = 1 / 4) :
      C = D
      source
      theorem Papers.Rockel2026ExactBlest.nu_rho_lower_unique (C D : ProbabilityTheory.Copula 2) (hc : Rockel2026XiBlest.blestNu C - C.spearmanRho = -1 / 4) (hd : Rockel2026XiBlest.blestNu D - D.spearmanRho = -1 / 4) :
      C = D