← Mathematical handbook

Complete pointwise contact sets for the eta transport certificates.

theorem Papers.Rockel2026ExactBlest.phiA_upper_closed (w x : ℝ) (hx : w ≤ x) : phiA w x = phiA1 w x

theorem Papers.Rockel2026ExactBlest.psiA_upper_closed (w z : ℝ) (hz : 1 - w ≤ z) : psiA w z = psiA1 w z

def Papers.Rockel2026ExactBlest.contactA (w x z : ℝ) : Prop

Equations

• Papers.Rockel2026ExactBlest.contactA w x z = (x ≤ w ∧ z = 1 - x ∨ w ≤ x ∧ z = x - w ∨ w = 1 / 2 ∧ w ≤ x ∧ z = 1 / 2)

theorem Papers.Rockel2026ExactBlest.graph_contact_complete (w x z : ℝ) (hw0 : 0 < w) (hw1 : w ≤ 1 / 2) (hx : x ∈ Set.Icc 0 1) (hz : z ∈ Set.Icc 0 1) : phiA w x + psiA w z - cost (kA w) x z = 0 ↔ contactA w x z

theorem Papers.Rockel2026ExactBlest.phiB_upper_closed (a x : ℝ) (hx : a ≤ x) : phiB a x = phiB1 a x

theorem Papers.Rockel2026ExactBlest.randomized_contact_complete (a x z : ℝ) (ha : 1 / 2 < a) (ha1 : a < 1) (hx : x ∈ Set.Icc 0 1) (hz : z ∈ Set.Icc 0 1) : phiB a x + psiB a z - cost (kB a) x z = 0 ↔ x = randomRankReal a z