← Copula mathematical handbook

Constructed clamped extremizers and their unique optimality

noncomputable def ProbabilityTheory.Copula.RankRegion.XiBlest.extremalCopula (b : ℝ) (hb : 0 ≤ b) : Copula 2

Equations

• ProbabilityTheory.Copula.RankRegion.XiBlest.extremalCopula b hb = ProbabilityTheory.Copula.RankRegion.XiBlest.Support.quadraticBand b hb

noncomputable def ProbabilityTheory.Copula.RankRegion.XiBlest.extremalQ (b : ℝ) (hb : 0 < b) (v : ↑unitInterval) : ℝ

The source's normalization parameter, including response thresholds 0 and 1.

Equations

• ProbabilityTheory.Copula.RankRegion.XiBlest.extremalQ b hb v = -ProbabilityTheory.Copula.RankRegion.XiBlest.Support.quadraticIntercept b ⋯ v / b

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.extremal_normalization (b : ℝ) (hb : 0 < b) (v : ↑unitInterval) : ∃! q : ℝ, q ∈ Set.Icc (-1 / b) 1 ∧ ∫ (t : ↑unitInterval), Common.unitClamp (b * ((1 - ↑t) ^ 2 - q)) = ↑v

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.extremalQ_antitone (b : ℝ) (hb : 0 < b) : Antitone (extremalQ b hb)

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.extremal_kernel_measurable (b : ℝ) (hb : 0 ≤ b) : Measurable fun (p : ↑unitInterval × ↑unitInterval) => Support.quadraticKernel b hb p.2 p.1

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.extremal_cdf (b : ℝ) (hb : 0 < b) (u v : ↑unitInterval) : (extremalCopula b ⋯).cdf ![u, v] = ∫ (t : ↑unitInterval) in Set.Iic u, Common.unitClamp (b * ((1 - ↑t) ^ 2 - extremalQ b hb v))

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.extremal_conditionalCDF (b : ℝ) (hb : 0 < b) (v : ↑unitInterval) : (fun (u : ↑unitInterval) => (extremalCopula b ⋯).conditionalCDF u v) =ᵐ[MeasureTheory.volume] fun (u : ↑unitInterval) => Common.unitClamp (b * ((1 - ↑u) ^ 2 - extremalQ b hb v))

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.extremal_isSI (b : ℝ) (hb : 0 ≤ b) : (extremalCopula b hb).IsSI

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.extremal_support (C : Copula 2) (b : ℝ) (hb : 0 ≤ b) : b * blestNu C - C.chatterjeeXi ≤ b * blestNu (extremalCopula b hb) - (extremalCopula b hb).chatterjeeXi

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.extremal_support_eq_iff (C : Copula 2) (b : ℝ) (hb : 0 ≤ b) : b * blestNu C - C.chatterjeeXi = b * blestNu (extremalCopula b hb) - (extremalCopula b hb).chatterjeeXi ↔ C = extremalCopula b hb

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.extremal_maximal_blest (C : Copula 2) (b : ℝ) (hb : 0 < b) (hx : C.chatterjeeXi ≤ (extremalCopula b ⋯).chatterjeeXi) : blestNu C ≤ blestNu (extremalCopula b ⋯)

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.extremal_maximal_blest_eq_iff (C : Copula 2) (b : ℝ) (hb : 0 < b) (hx : C.chatterjeeXi = (extremalCopula b ⋯).chatterjeeXi) : blestNu C = blestNu (extremalCopula b ⋯) ↔ C = extremalCopula b ⋯

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.extremal_zero : extremalCopula 0 ⋯ = independence 2