← Mathematical handbook

Optimization over the full relaxed class of measurable kernels

structure Papers.Rockel2026XiBlest.AdmissibleKernel (h : ↑unitInterval × ↑unitInterval → ℝ) : Prop

Coordinates are (response threshold, conditioning rank); no monotonicity is assumed.

• measurable : MeasureTheory.AEStronglyMeasurable h MeasureTheory.volume
• box : ∀ᵐ (p : ↑unitInterval × ↑unitInterval), h p ∈ Set.Icc 0 1
• marginal : ∀ᵐ (v : ↑unitInterval), ∫ (u : ↑unitInterval), h (v, u) = ↑v

noncomputable def Papers.Rockel2026XiBlest.kernelXi (h : ↑unitInterval × ↑unitInterval → ℝ) : ℝ

Equations

• Papers.Rockel2026XiBlest.kernelXi h = (6 * ∫ (p : ↑unitInterval × ↑unitInterval), h p ^ 2) - 2

noncomputable def Papers.Rockel2026XiBlest.kernelNu (h : ↑unitInterval × ↑unitInterval → ℝ) : ℝ

Equations

• Papers.Rockel2026XiBlest.kernelNu h = (12 * ∫ (p : ↑unitInterval × ↑unitInterval), (1 - ↑p.2) ^ 2 * h p) - 2

noncomputable def Papers.Rockel2026XiBlest.extremalKernel (b : ℝ) (hb : 0 ≤ b) (p : ↑unitInterval × ↑unitInterval) : ℝ

Equations

• Papers.Rockel2026XiBlest.extremalKernel b hb p = Verification.quadraticKernel b hb p.1 p.2

theorem Papers.Rockel2026XiBlest.AdmissibleKernel.memLp {h : ↑unitInterval × ↑unitInterval → ℝ} (hh : AdmissibleKernel h) : MeasureTheory.MemLp h 2 MeasureTheory.volume

theorem Papers.Rockel2026XiBlest.extremalKernel_admissible (b : ℝ) (hb : 0 ≤ b) : AdmissibleKernel (extremalKernel b hb)

theorem Papers.Rockel2026XiBlest.relaxed_distance_bound (h : ↑unitInterval × ↑unitInterval → ℝ) (hh : AdmissibleKernel h) (b : ℝ) (hb : 0 ≤ b) : 6 * ∫ (p : ↑unitInterval × ↑unitInterval), (h p - extremalKernel b hb p) ^ 2 ≤ kernelXi h - kernelXi (extremalKernel b hb) - b * (kernelNu h - kernelNu (extremalKernel b hb))

theorem Papers.Rockel2026XiBlest.relaxed_maximal (h : ↑unitInterval × ↑unitInterval → ℝ) (hh : AdmissibleKernel h) (b : ℝ) (hb : 0 < b) (hx : kernelXi h ≤ kernelXi (extremalKernel b ⋯)) : kernelNu h ≤ kernelNu (extremalKernel b ⋯)

theorem Papers.Rockel2026XiBlest.relaxed_maximal_eq_iff (h : ↑unitInterval × ↑unitInterval → ℝ) (hh : AdmissibleKernel h) (b : ℝ) (hb : 0 < b) (hx : kernelXi h ≤ kernelXi (extremalKernel b ⋯)) : kernelNu h = kernelNu (extremalKernel b ⋯) ↔ h =ᵐ[MeasureTheory.volume] extremalKernel b ⋯

theorem Papers.Rockel2026XiBlest.extremalKernel_coefficients (b : ℝ) (hb : 0 ≤ b) : kernelXi (extremalKernel b hb) = (extremalCopula b hb).chatterjeeXi ∧ kernelNu (extremalKernel b hb) = blestNu (extremalCopula b hb)

theorem Papers.Rockel2026XiBlest.relaxed_solution (c : ℝ) (hc : c ∈ Set.Ioo 0 1) : ∃! b : ↑(Set.Ioi 0), kernelXi (extremalKernel ↑b ⋯) = c ∧ ∀ (h : ↑unitInterval × ↑unitInterval → ℝ), AdmissibleKernel h → kernelXi h ≤ c → kernelNu h ≤ kernelNu (extremalKernel ↑b ⋯) ∧ (kernelNu h = kernelNu (extremalKernel ↑b ⋯) ↔ h =ᵐ[MeasureTheory.volume] extremalKernel ↑b ⋯)

Theorem 3.4 for arbitrary admissible L2 representatives, with uniqueness almost everywhere.