← Mathematical handbook

The signed tent g_b and the factor ℓ (Section 3, version 2)

Real-variable versions of the objects of Section 3:

• tentG b v = sgn(b) (|b|/2 - |v - 1/2|)_+ (equation (3.1)),
• ellFun u = min(u, 1 - u), sigmaFun u = 1 for u < 1/2 and -1 for u ≥ 1/2,
• its properties stated before Proposition 3.1: Lipschitz, support, g_b(1/2) = b/2, symmetry, oddness in b, ∫ g_b = b|b|/4, and the a.e. derivative g_b'.

They are tied to the version-1 tent displacement tentDisplacement.

noncomputable def Papers.OrendayLaresRockel2026XiBeta.sgn (b : ℝ) : ℝ

The sign function with sgn 0 = 0.

Equations

• Papers.OrendayLaresRockel2026XiBeta.sgn b = if 0 < b then 1 else if b < 0 then -1 else 0

theorem Papers.OrendayLaresRockel2026XiBeta.sgn_of_pos {b : ℝ} (h : 0 < b) : sgn b = 1

theorem Papers.OrendayLaresRockel2026XiBeta.sgn_of_neg {b : ℝ} (h : b < 0) : sgn b = -1

theorem Papers.OrendayLaresRockel2026XiBeta.sgn_zero : sgn 0 = 0

theorem Papers.OrendayLaresRockel2026XiBeta.sgn_neg (b : ℝ) : sgn (-b) = -sgn b

theorem Papers.OrendayLaresRockel2026XiBeta.sgn_mul_abs (b : ℝ) : sgn b * |b| = b

noncomputable def Papers.OrendayLaresRockel2026XiBeta.tentG (b v : ℝ) : ℝ

The signed tent g_b(v) = sgn(b) (|b|/2 - |v - 1/2|)_+ on the real line.

Equations

• Papers.OrendayLaresRockel2026XiBeta.tentG b v = Papers.OrendayLaresRockel2026XiBeta.sgn b * Verification.medianTent |b| v

noncomputable def Papers.OrendayLaresRockel2026XiBeta.ellFun (u : ℝ) : ℝ

ℓ(u) = min(u, 1 - u).

Equations

• Papers.OrendayLaresRockel2026XiBeta.ellFun u = min u (1 - u)

noncomputable def Papers.OrendayLaresRockel2026XiBeta.sigmaFun (u : ℝ) : ℝ

σ(u) = 1 for u < 1/2 and σ(u) = -1 for u ≥ 1/2.

Equations

• Papers.OrendayLaresRockel2026XiBeta.sigmaFun u = if u < 1 / 2 then 1 else -1

noncomputable def Papers.OrendayLaresRockel2026XiBeta.tentGDeriv (b v : ℝ) : ℝ

The a.e. derivative of g_b: sgn(b) (1_{(α_b, 1/2)} - 1_{(1/2, 1 - α_b)}), where α_b = (1 - |b|)/2.

Equations

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

theorem Papers.OrendayLaresRockel2026XiBeta.tentDisplacement_eq_tentG (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) (v : ↑unitInterval) : (tentDisplacement b hb).toFun v = tentG b ↑v

theorem Papers.OrendayLaresRockel2026XiBeta.abs_sgn_le (b : ℝ) : |sgn b| ≤ 1

theorem Papers.OrendayLaresRockel2026XiBeta.tentG_lipschitz (b v w : ℝ) : |tentG b v - tentG b w| ≤ |v - w|

theorem Papers.OrendayLaresRockel2026XiBeta.tentG_eq_zero {b v : ℝ} (h : v < (1 - |b|) / 2 ∨ (1 + |b|) / 2 < v) : tentG b v = 0

theorem Papers.OrendayLaresRockel2026XiBeta.tentG_half (b : ℝ) : tentG b (1 / 2) = b / 2

theorem Papers.OrendayLaresRockel2026XiBeta.tentG_one_sub (b v : ℝ) : tentG b (1 - v) = tentG b v

theorem Papers.OrendayLaresRockel2026XiBeta.tentG_neg (b v : ℝ) : tentG (-b) v = -tentG b v

theorem Papers.OrendayLaresRockel2026XiBeta.tentG_zero (v : ℝ) : tentG 0 v = 0

theorem Papers.OrendayLaresRockel2026XiBeta.integral_tentG (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) : ∫ (v : ↑unitInterval), tentG b ↑v = b * |b| / 4

theorem Papers.OrendayLaresRockel2026XiBeta.integral_tentG_sq (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) : ∫ (v : ↑unitInterval), tentG b ↑v ^ 2 = |b| ^ 3 / 12

theorem Papers.OrendayLaresRockel2026XiBeta.hasDerivAt_tentG (b : ℝ) {v : ℝ} (h1 : v ≠ (1 - |b|) / 2) (h2 : v ≠ 1 / 2) (h3 : v ≠ (1 + |b|) / 2) : HasDerivAt (tentG b) (tentGDeriv b v) v

The derivative of g_b away from the three break points α_b, 1/2, 1 - α_b.

theorem Papers.OrendayLaresRockel2026XiBeta.hasDerivAt_ellFun {u : ℝ} (h : u ≠ 1 / 2) : HasDerivAt ellFun (sigmaFun u) u