Papers.Rockel2026ExactBlest.ExactBlestEtaUniqueness

← Mathematical handbook

Equality cases for the eta/Blest region in exact-blest-regions.tex.

source

theorem Papers.Rockel2026ExactBlest.ae_coord_ne (C : ProbabilityTheory.Copula 2) (i : Fin 2) (c : ℝ) :

∀ᵐ (x : Fin 2 → ↑unitInterval) ∂C.toMeasure, ↑(x i) ≠ c

Uniform marginals put no mass on a specified coordinate line.

source

noncomputable def Papers.Rockel2026ExactBlest.graphRank (w u : ↑unitInterval) :

↑unitInterval

Equations

Papers.Rockel2026ExactBlest.graphRank w u = ⟨if ↑u ≤ ↑w then 1 - ↑u else ↑u - ↑w, ⋯⟩

Instances For

source

theorem Papers.Rockel2026ExactBlest.measurable_graphRank (w : ↑unitInterval) :

Measurable (graphRank w)

source

theorem Papers.Rockel2026ExactBlest.graph_contact (w x z : ℝ) (hw0 : 0 ≤ w) (hw1 : w ≤ 1 / 2) (hx : x ∈ Set.Icc 0 1) (hz : z ∈ Set.Icc 0 1) (hxc : x ≠ w) (hzc : z ≠ 1 - w) (heq : phiA w x + psiA w z - cost (kA w) x z = 0) :

z = if x ≤ w then 1 - x else x - w

Off the two marginal-null cut lines, zero A-slack forces the graph.

source

theorem Papers.Rockel2026ExactBlest.graph_support_graph (C : ProbabilityTheory.Copula 2) (w : ↑unitInterval) (hw : ↑w ≤ 1 / 2) (hbound : (1 + kA ↑w) * Rockel2026XiBlest.blestNu C - 2 * kA ↑w * eta C = (1 + kA ↑w) * Rockel2026XiBlest.blestNu (familyA w) - 2 * kA ↑w * eta (familyA w)) :

∀ᵐ (x : Fin 2 → ↑unitInterval) ∂C.survivalCopula.toMeasure, x 1 = graphRank w (x 0)

source

theorem Papers.Rockel2026ExactBlest.graph_support_unique (C : ProbabilityTheory.Copula 2) (w : ↑unitInterval) (hw : ↑w ≤ 1 / 2) (hbound : (1 + kA ↑w) * Rockel2026XiBlest.blestNu C - 2 * kA ↑w * eta C = (1 + kA ↑w) * Rockel2026XiBlest.blestNu (familyA w) - 2 * kA ↑w * eta (familyA w)) :

C = familyA w

source

theorem Papers.Rockel2026ExactBlest.graph_upper_unique (C : ProbabilityTheory.Copula 2) (w : ↑unitInterval) (hw : ↑w ≤ 1 / 2) (he : eta C = eta (familyA w)) (hn : Rockel2026XiBlest.blestNu C = Rockel2026XiBlest.blestNu (familyA w)) :

C = familyA w

source

theorem Papers.Rockel2026ExactBlest.graph_lower_unique (C : ProbabilityTheory.Copula 2) (w : ↑unitInterval) (hw : ↑w ≤ 1 / 2) (he : eta C = eta (familyA w)) (hn : Rockel2026XiBlest.blestNu C = 2 * eta (familyA w) - Rockel2026XiBlest.blestNu (familyA w)) :

C = (familyA w).transpose

source

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

C = D

The same graph-law argument with the second marginal as the parameter.

source

noncomputable def Papers.Rockel2026ExactBlest.randomRankReal (a z : ℝ) :

ℝ

Equations

Papers.Rockel2026ExactBlest.randomRankReal a z = if z ≤ Papers.Rockel2026ExactBlest.cutB a then 2 * a * z + a else if z ≤ 1 - a then a * (1 - 2 * z) / (2 * a - 1) else 1 - z

Instances For

source

theorem Papers.Rockel2026ExactBlest.randomRankReal_mem (a z : ℝ) (ha : 1 / 2 < a) (ha1 : a < 1) (hz : z ∈ Set.Icc 0 1) :

randomRankReal a z ∈ Set.Icc 0 1

source

noncomputable def Papers.Rockel2026ExactBlest.randomRank (a : ℝ) (ha : 1 / 2 < a) (ha1 : a < 1) (z : ↑unitInterval) :

↑unitInterval

Equations

Papers.Rockel2026ExactBlest.randomRank a ha ha1 z = ⟨Papers.Rockel2026ExactBlest.randomRankReal a ↑z, ⋯⟩

Instances For

source

theorem Papers.Rockel2026ExactBlest.measurable_randomRank (a : ℝ) (ha : 1 / 2 < a) (ha1 : a < 1) :

Measurable (randomRank a ha ha1)

source

theorem Papers.Rockel2026ExactBlest.randomized_contact (a x z : ℝ) (ha : 1 / 2 < a) (ha1 : a < 1) (hx : x ∈ Set.Icc 0 1) (hz : z ∈ Set.Icc 0 1) (hxc : x ≠ a) (hzc : z ≠ cutB a) (heq : phiB a x + psiB a z - cost (kB a) x z = 0) :

x = randomRankReal a z

Zero B-slack determines X from Z away from marginal-null cut lines.

source