← Mathematical handbook

Proposition 2: the actual Lebesgue density of the tent copula

Values on the finitely many strip edges are fixed explicitly. At full width the version uses the median sign, which also supports the endpoint TP2 claim.

noncomputable def Papers.OrendayLaresRockel2026XiBeta.tentStart (r : ↑unitInterval) : ↑unitInterval

Equations

• Papers.OrendayLaresRockel2026XiBeta.tentStart r = ⟨(1 - ↑r) / 2, ⋯⟩

noncomputable def Papers.OrendayLaresRockel2026XiBeta.tentEnd (r : ↑unitInterval) : ↑unitInterval

Equations

• Papers.OrendayLaresRockel2026XiBeta.tentEnd r = ⟨(1 + ↑r) / 2, ⋯⟩

noncomputable def Papers.OrendayLaresRockel2026XiBeta.tentSlope (r v : ↑unitInterval) : ℝ

Equations

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

theorem Papers.OrendayLaresRockel2026XiBeta.measurable_tentSlope (r : ↑unitInterval) : Measurable (tentSlope r)

theorem Papers.OrendayLaresRockel2026XiBeta.tentSlope_values (r v : ↑unitInterval) : tentSlope r v = -1 ∨ tentSlope r v = 0 ∨ tentSlope r v = 1

theorem Papers.OrendayLaresRockel2026XiBeta.tentSlope_abs_le (r v : ↑unitInterval) : |tentSlope r v| ≤ 1

theorem Papers.OrendayLaresRockel2026XiBeta.integral_tentSlope (r v : ↑unitInterval) : ∫ (t : ↑unitInterval) in Set.Iic v, tentSlope r t = Verification.medianTent ↑r ↑v

noncomputable def Papers.OrendayLaresRockel2026XiBeta.signedTentSlope (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) (v : ↑unitInterval) : ℝ

Equations

• Papers.OrendayLaresRockel2026XiBeta.signedTentSlope b hb v = if h : 0 ≤ b then Papers.OrendayLaresRockel2026XiBeta.tentSlope ⟨b, ⋯⟩ v else -Papers.OrendayLaresRockel2026XiBeta.tentSlope ⟨-b, ⋯⟩ v

noncomputable def Papers.OrendayLaresRockel2026XiBeta.tentDensity (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) (x : Fin 2 → ↑unitInterval) : ℝ

Equations

• Papers.OrendayLaresRockel2026XiBeta.tentDensity b hb x = 1 + Verification.medianSign (x 0) * Papers.OrendayLaresRockel2026XiBeta.signedTentSlope b hb (x 1)

theorem Papers.OrendayLaresRockel2026XiBeta.signedTentSlope_measurable (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) : Measurable (signedTentSlope b hb)

theorem Papers.OrendayLaresRockel2026XiBeta.signedTentSlope_abs_le (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) (v : ↑unitInterval) : |signedTentSlope b hb v| ≤ 1

theorem Papers.OrendayLaresRockel2026XiBeta.integral_signedTentSlope (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) (v : ↑unitInterval) : ∫ (t : ↑unitInterval) in Set.Iic v, signedTentSlope b hb t = (tentDisplacement b hb).toFun v

theorem Papers.OrendayLaresRockel2026XiBeta.leftBoundary_density (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) : (leftBoundary b hb).toMeasure = MeasureTheory.volume.withDensity fun (x : Fin 2 → ↑unitInterval) => ENNReal.ofReal (tentDensity b hb x)

theorem Papers.OrendayLaresRockel2026XiBeta.leftBoundary_absolutelyContinuous (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) : (leftBoundary b hb).toMeasure.AbsolutelyContinuous MeasureTheory.volume

theorem Papers.OrendayLaresRockel2026XiBeta.tentDensity_values (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) (x : Fin 2 → ↑unitInterval) : tentDensity b hb x = 0 ∨ tentDensity b hb x = 1 ∨ tentDensity b hb x = 2