← Mathematical handbook

The scalar relaxation for the xi-footrule lower bound

The two values minimize a strictly convex weighted quadratic under a uniform-mean constraint. The proof uses an exact quadratic remainder.

noncomputable def Verification.jensenLow (μ : ℝ) (v : ↑unitInterval) : ℝ

Equations

• Verification.jensenLow μ v = if ↑v * (2 + μ) ≤ μ then 0 else if ↑v * (2 + μ) ≤ 2 then ↑v - μ / 2 * (1 - ↑v) else 2 - 1 / ↑v

noncomputable def Verification.jensenHigh (μ : ℝ) (v : ↑unitInterval) : ℝ

Equations

• Verification.jensenHigh μ v = if ↑v * (2 + μ) ≤ μ then ↑v / (1 - ↑v) else if ↑v * (2 + μ) ≤ 2 then ↑v + μ / 2 * ↑v else 1

def Verification.splitObjective (μ v a b : ℝ) : ℝ

Equations

• Verification.splitObjective μ v a b = μ * v * a + v * a ^ 2 + (1 - v) * b ^ 2

theorem Verification.jensen_feasible (μ : ℝ) (hμ : μ ∈ Set.Icc 0 2) (v : ↑unitInterval) : jensenLow μ v ∈ Set.Icc 0 1 ∧ jensenHigh μ v ∈ Set.Icc 0 1 ∧ ↑v * jensenLow μ v + (1 - ↑v) * jensenHigh μ v = ↑v

theorem Verification.jensen_certificate (μ : ℝ) (hμ : μ ∈ Set.Icc 0 2) (v : ↑unitInterval) (a b : ℝ) (ha : a ∈ Set.Icc 0 1) (hb : b ∈ Set.Icc 0 1) (hm : ↑v * a + (1 - ↑v) * b = ↑v) : 0 ≤ (μ + 2 * jensenLow μ v - 2 * jensenHigh μ v) * (a - jensenLow μ v)

theorem Verification.splitObjective_remainder (μ v a b x y : ℝ) (hm : v * a + (1 - v) * b = v) (ho : v * x + (1 - v) * y = v) : splitObjective μ v a b - splitObjective μ v x y = v * (a - x) ^ 2 + (1 - v) * (b - y) ^ 2 + v * (μ + 2 * x - 2 * y) * (a - x)

theorem Verification.jensen_optimal_gap (μ : ℝ) (hμ : μ ∈ Set.Icc 0 2) (v : ↑unitInterval) (a b : ℝ) (ha : a ∈ Set.Icc 0 1) (hb : b ∈ Set.Icc 0 1) (hm : ↑v * a + (1 - ↑v) * b = ↑v) : ↑v * (a - jensenLow μ v) ^ 2 + (1 - ↑v) * (b - jensenHigh μ v) ^ 2 ≤ splitObjective μ (↑v) a b - splitObjective μ (↑v) (jensenLow μ v) (jensenHigh μ v)

theorem Verification.jensen_optimal (μ : ℝ) (hμ : μ ∈ Set.Icc 0 2) (v : ↑unitInterval) (a b : ℝ) (ha : a ∈ Set.Icc 0 1) (hb : b ∈ Set.Icc 0 1) (hm : ↑v * a + (1 - ↑v) * b = ↑v) : splitObjective μ (↑v) (jensenLow μ v) (jensenHigh μ v) ≤ splitObjective μ (↑v) a b

theorem Verification.jensen_optimal_eq_iff (μ : ℝ) (hμ : μ ∈ Set.Icc 0 2) (v : ↑unitInterval) (hv : 0 < ↑v ∧ ↑v < 1) (a b : ℝ) (ha : a ∈ Set.Icc 0 1) (hb : b ∈ Set.Icc 0 1) (hm : ↑v * a + (1 - ↑v) * b = ↑v) : splitObjective μ (↑v) a b = splitObjective μ (↑v) (jensenLow μ v) (jensenHigh μ v) ↔ a = jensenLow μ v ∧ b = jensenHigh μ v

theorem Verification.measurable_jensenLow (μ : ℝ) : Measurable (jensenLow μ)

theorem Verification.measurable_jensenHigh (μ : ℝ) : Measurable (jensenHigh μ)