← Mathematical handbook

The tent is the unique minimizer (introduction and Remark 3.3)

Among all 1-Lipschitz functions g : [0,1] → ℝ with g(1/2) = b/2, the signed tent g_b is pointwise smallest in absolute value and is the unique minimizer of ∫ g², with minimal value |b|³/12. This is the variational statement behind (1.4).

theorem Papers.OrendayLaresRockel2026XiBeta.continuous_tentG (b : ℝ) : Continuous (tentG b)

theorem Papers.OrendayLaresRockel2026XiBeta.abs_tentG_le_abs {b : ℝ} (g : ↑unitInterval → ℝ) (hg : ∀ (v w : ↑unitInterval), |g v - g w| ≤ |↑v - ↑w|) (h2 : g ProbabilityTheory.Copula.unitHalf = b / 2) (v : ↑unitInterval) : |tentG b ↑v| ≤ |g v|

Pointwise: |g_b(v)| ≤ |g(v)| for every 1-Lipschitz g with g(1/2) = b/2.

theorem Papers.OrendayLaresRockel2026XiBeta.tentG_sq_le {b : ℝ} (g : ↑unitInterval → ℝ) (hg : ∀ (v w : ↑unitInterval), |g v - g w| ≤ |↑v - ↑w|) (h2 : g ProbabilityTheory.Copula.unitHalf = b / 2) (v : ↑unitInterval) : tentG b ↑v ^ 2 ≤ g v ^ 2

theorem Papers.OrendayLaresRockel2026XiBeta.tent_minimizes {b : ℝ} (hb : b ∈ Set.Icc (-1) 1) (g : ↑unitInterval → ℝ) (hg : ∀ (v w : ↑unitInterval), |g v - g w| ≤ |↑v - ↑w|) (h2 : g ProbabilityTheory.Copula.unitHalf = b / 2) : |b| ^ 3 / 12 ≤ ∫ (v : ↑unitInterval), g v ^ 2

The signed tent minimizes ∫ g² among 1-Lipschitz functions with g(1/2) = b/2, and the minimal value is |b|³/12.

theorem Papers.OrendayLaresRockel2026XiBeta.continuous_of_lipschitz_unit (g : ↑unitInterval → ℝ) (hg : ∀ (v w : ↑unitInterval), |g v - g w| ≤ |↑v - ↑w|) : Continuous g

theorem Papers.OrendayLaresRockel2026XiBeta.tent_minimizer_unique {b : ℝ} (hb : b ∈ Set.Icc (-1) 1) (g : ↑unitInterval → ℝ) (hg : ∀ (v w : ↑unitInterval), |g v - g w| ≤ |↑v - ↑w|) (h2 : g ProbabilityTheory.Copula.unitHalf = b / 2) (heq : ∫ (v : ↑unitInterval), g v ^ 2 = |b| ^ 3 / 12) (v : ↑unitInterval) : g v = tentG b ↑v

Uniqueness of the minimizer: equality forces g = g_b on [0,1].