← Mathematical handbook

Beta-boundary equality cases for exact-blest-regions.tex. Fermat's theorem applied to the already checked dual forces the shuffle graph.

noncomputable def Papers.Rockel2026ExactBlest.betaRankReal (q x : ℝ) : ℝ

Equations

• One or more equations did not get rendered due to their size.

theorem Papers.Rockel2026ExactBlest.betaRankReal_mem (q : ℝ) (hq : q ∈ Set.Icc 0 (1 / 2)) (x : ↑unitInterval) : betaRankReal q ↑x ∈ Set.Icc 0 1

noncomputable def Papers.Rockel2026ExactBlest.betaRank (q : ℝ) (hq : q ∈ Set.Icc 0 (1 / 2)) (x : ↑unitInterval) : ↑unitInterval

Equations

• Papers.Rockel2026ExactBlest.betaRank q hq x = ⟨Papers.Rockel2026ExactBlest.betaRankReal q ↑x, ⋯⟩

theorem Papers.Rockel2026ExactBlest.measurable_betaRank (q : ℝ) (hq : q ∈ Set.Icc 0 (1 / 2)) : Measurable (betaRank q hq)

theorem Papers.Rockel2026ExactBlest.hasDerivAt_betaCubic (h c x : ℝ) : HasDerivAt (fun (y : ℝ) => 2 * y ^ 3 / 3 + h * y ^ 2 + c) (2 * x * (x + h)) x

theorem Papers.Rockel2026ExactBlest.hasDerivAt_paramPhi (q x : ℝ) (hxq : x ≠ q) (hxh : x ≠ 1 / 2) (hxr : x ≠ 1 - q) : HasDerivAt (paramPhi q) (2 * x * betaRankReal q x) x

noncomputable def Papers.Rockel2026ExactBlest.betaSlackReal (q x z : ℝ) : ℝ

Equations

• One or more equations did not get rendered due to their size.

theorem Papers.Rockel2026ExactBlest.hasDerivAt_betaIndicator (x z : ℝ) (hxh : x ≠ 1 / 2) : HasDerivAt (fun (y : ℝ) => if 1 / 2 < y ∧ 1 / 2 < z then 1 else 0) 0 x

The median-quadrant indicator is locally constant off its vertical cut.

theorem Papers.Rockel2026ExactBlest.beta_contact (q x z : ℝ) (hq : q ∈ Set.Icc 0 (1 / 2)) (hx : x ∈ Set.Ioo 0 1) (hz : z ∈ Set.Icc 0 1) (hxq : x ≠ q) (hxh : x ≠ 1 / 2) (hxr : x ≠ 1 - q) (heq : betaSlackReal q x z = 0) : z = betaRankReal q x

theorem Papers.Rockel2026ExactBlest.beta_upper_graph (C : ProbabilityTheory.Copula 2) (q : ℝ) (hq : q ∈ Set.Icc 0 (1 / 2)) (hb : C.blomqvistBeta = 4 * q - 1) (hn : Rockel2026XiBlest.blestNu C = betaUpper C.blomqvistBeta) : ∀ᵐ (x : Fin 2 → ↑unitInterval) ∂C.survivalCopula.toMeasure, x 1 = betaRank q hq (x 0)

theorem Papers.Rockel2026ExactBlest.beta_upper_unique (C D : ProbabilityTheory.Copula 2) (hb : C.blomqvistBeta = D.blomqvistBeta) (hc : Rockel2026XiBlest.blestNu C = betaUpper C.blomqvistBeta) (hd : Rockel2026XiBlest.blestNu D = betaUpper D.blomqvistBeta) : C = D

The unique graph is forced at every beta, including both endpoint fibres.

theorem Papers.Rockel2026ExactBlest.beta_lower_unique (C D : ProbabilityTheory.Copula 2) (hb : C.blomqvistBeta = D.blomqvistBeta) (hc : Rockel2026XiBlest.blestNu C = betaLower C.blomqvistBeta) (hd : Rockel2026XiBlest.blestNu D = betaLower D.blomqvistBeta) : C = D

theorem Papers.Rockel2026ExactBlest.beta_upper_exists_unique (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) : ∃! C : ProbabilityTheory.Copula 2, C.blomqvistBeta = b ∧ Rockel2026XiBlest.blestNu C = betaUpper b

theorem Papers.Rockel2026ExactBlest.beta_lower_exists_unique (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) : ∃! C : ProbabilityTheory.Copula 2, C.blomqvistBeta = b ∧ Rockel2026XiBlest.blestNu C = betaLower b

theorem Papers.Rockel2026ExactBlest.nu_beta_upper_parameter (C : ProbabilityTheory.Copula 2) (hc : Rockel2026XiBlest.blestNu C - C.blomqvistBeta = 8 / 9) : C.blomqvistBeta = -1 / 3

theorem Papers.Rockel2026ExactBlest.nu_beta_upper_unique (C : ProbabilityTheory.Copula 2) (hc : Rockel2026XiBlest.blestNu C - C.blomqvistBeta = 8 / 9) : C = betaWitness

theorem Papers.Rockel2026ExactBlest.nu_beta_lower_unique (C : ProbabilityTheory.Copula 2) (hc : Rockel2026XiBlest.blestNu C - C.blomqvistBeta = -8 / 9) : C = betaWitness.reflect {1}

theorem Papers.Rockel2026ExactBlest.nu_beta_eq_iff (C : ProbabilityTheory.Copula 2) : |Rockel2026XiBlest.blestNu C - C.blomqvistBeta| = 8 / 9 ↔ C = betaWitness ∨ C = betaWitness.reflect {1}

theorem Papers.Rockel2026ExactBlest.beta_upper_rho_eq (C : ProbabilityTheory.Copula 2) (hc : Rockel2026XiBlest.blestNu C = betaUpper C.blomqvistBeta) : C.spearmanRho = Rockel2026XiBlest.blestNu C

theorem Papers.Rockel2026ExactBlest.beta_lower_rho_eq (C : ProbabilityTheory.Copula 2) (hc : Rockel2026XiBlest.blestNu C = betaLower C.blomqvistBeta) : C.spearmanRho = Rockel2026XiBlest.blestNu C

theorem Papers.Rockel2026ExactBlest.beta_upper_survival (C : ProbabilityTheory.Copula 2) (hc : Rockel2026XiBlest.blestNu C = betaUpper C.blomqvistBeta) : C.survivalCopula = C

theorem Papers.Rockel2026ExactBlest.beta_lower_survival (C : ProbabilityTheory.Copula 2) (hc : Rockel2026XiBlest.blestNu C = betaLower C.blomqvistBeta) : C.survivalCopula = C

theorem Papers.Rockel2026ExactBlest.beta_upper_graph_law (C : ProbabilityTheory.Copula 2) (q : ℝ) (hq : q ∈ Set.Icc 0 (1 / 2)) (hb : C.blomqvistBeta = 4 * q - 1) (hn : Rockel2026XiBlest.blestNu C = betaUpper C.blomqvistBeta) : C.toMeasure = MeasureTheory.Measure.map (fun (x : ↑unitInterval) => ![x, betaRank q hq x]) MeasureTheory.volume

The original and reflected-coordinate upper extremizer is the graph law of P_q. The map representative may differ from the displayed P_q only at its cut points.

noncomputable def Papers.Rockel2026ExactBlest.betaLowerRank (q : ℝ) (hq : q ∈ Set.Icc 0 (1 / 2)) (x : ↑unitInterval) : ↑unitInterval

Equations

• Papers.Rockel2026ExactBlest.betaLowerRank q hq x = unitInterval.symm (Papers.Rockel2026ExactBlest.betaRank (1 / 2 - q) ⋯ x)

theorem Papers.Rockel2026ExactBlest.beta_lower_graph_law (C : ProbabilityTheory.Copula 2) (q : ℝ) (hq : q ∈ Set.Icc 0 (1 / 2)) (hb : C.blomqvistBeta = 4 * q - 1) (hn : Rockel2026XiBlest.blestNu C = betaLower C.blomqvistBeta) : C.toMeasure = MeasureTheory.Measure.map (fun (x : ↑unitInterval) => ![x, betaLowerRank q hq x]) MeasureTheory.volume

The lower shuffle is the second-coordinate reflection of P_(1/2-q).

theorem Papers.Rockel2026ExactBlest.betaRankReal_eq_paper (q x : ℝ) (hxq : x ≠ q) (hxh : x ≠ 1 / 2) : betaRankReal q x = if q ≤ x ∧ x < 1 / 2 then x + 1 / 2 - q else if 1 / 2 ≤ x ∧ x ≤ 1 - q then x - 1 / 2 + q else x

Exact agreement with the paper's P_q off its finitely many breakpoints.

theorem Papers.Rockel2026ExactBlest.betaLowerRank_eq_paper (q : ℝ) (hq : q ∈ Set.Icc 0 (1 / 2)) (x : ↑unitInterval) (hxl : ↑x ≠ 1 / 2 - q) (hxh : ↑x ≠ 1 / 2) : ↑(betaLowerRank q hq x) = if 1 / 2 - q ≤ ↑x ∧ ↑x < 1 / 2 then 1 - ↑x - q else if 1 / 2 ≤ ↑x ∧ ↑x ≤ 1 / 2 + q then 1 - ↑x + q else 1 - ↑x

The reflected shuffle agrees with the displayed N_q off the breakpoints.