← Mathematical handbook

The law of (U, V_b) (Proposition 5.3, first statement)

U ~ U(0,1) and an independent fair coin ε (Bool); V_b = U if U ∉ (b/2, 1 - b/2) and V_b = (2U + b)/4 + ε (1 - b)/2 otherwise. We show that the law of (U, V_b) is the measure of the copula R_b, so that R_b is the copula of (U, V_b).

noncomputable def Papers.OrendayLaresRockel2026XiBeta.bernoulliHalf : MeasureTheory.Measure Bool

The fair coin: P(ε = 0) = P(ε = 1) = 1/2 (false ↦ 0, true ↦ 1).

Equations

• Papers.OrendayLaresRockel2026XiBeta.bernoulliHalf = 2⁻¹ • (MeasureTheory.Measure.dirac false + MeasureTheory.Measure.dirac true)

instance Papers.OrendayLaresRockel2026XiBeta.instIsProbabilityMeasureBoolBernoulliHalf : MeasureTheory.IsProbabilityMeasure bernoulliHalf

theorem Papers.OrendayLaresRockel2026XiBeta.integral_bernoulliHalf (f : Bool → ℝ) : ∫ (e : Bool), f e ∂bernoulliHalf = (f false + f true) / 2

noncomputable def Papers.OrendayLaresRockel2026XiBeta.vbReal (b u : ℝ) (e : Bool) : ℝ

The real-valued formula for V_b as a function of (U, ε).

Equations

• Papers.OrendayLaresRockel2026XiBeta.vbReal b u e = if b / 2 < u ∧ u < 1 - b / 2 then (2 * u + b) / 4 + if e = true then (1 - b) / 2 else 0 else u

theorem Papers.OrendayLaresRockel2026XiBeta.vbReal_mem {b : ℝ} (hb : b ∈ Set.Icc 0 1) {u : ℝ} (hu : u ∈ Set.Icc 0 1) (e : Bool) : vbReal b u e ∈ Set.Icc 0 1

noncomputable def Papers.OrendayLaresRockel2026XiBeta.Vb (b : ℝ) (u : ↑unitInterval) (e : Bool) : ↑unitInterval

V_b as a point of the unit interval.

Equations

• Papers.OrendayLaresRockel2026XiBeta.Vb b u e = Set.projIcc 0 1 Papers.OrendayLaresRockel2026XiBeta.Vb._proof_1 (Papers.OrendayLaresRockel2026XiBeta.vbReal b (↑u) e)

theorem Papers.OrendayLaresRockel2026XiBeta.coe_Vb {b : ℝ} (hb : b ∈ Set.Icc 0 1) (u : ↑unitInterval) (e : Bool) : ↑(Vb b u e) = vbReal b (↑u) e

theorem Papers.OrendayLaresRockel2026XiBeta.measurable_Vb (b : ℝ) : Measurable fun (p : ↑unitInterval × Bool) => Vb b p.1 p.2

noncomputable def Papers.OrendayLaresRockel2026XiBeta.Xb (b : ℝ) (p : ↑unitInterval × Bool) : Fin 2 → ↑unitInterval

The random vector (U, V_b) on I × Bool.

Equations

• Papers.OrendayLaresRockel2026XiBeta.Xb b p = ![p.1, Papers.OrendayLaresRockel2026XiBeta.Vb b p.1 p.2]

theorem Papers.OrendayLaresRockel2026XiBeta.measurable_Xb (b : ℝ) : Measurable (Xb b)

noncomputable def Papers.OrendayLaresRockel2026XiBeta.lawVb (b : ℝ) : MeasureTheory.Measure (Fin 2 → ↑unitInterval)

The law of (U, V_b).

Equations

• Papers.OrendayLaresRockel2026XiBeta.lawVb b = MeasureTheory.Measure.map (Papers.OrendayLaresRockel2026XiBeta.Xb b) (MeasureTheory.volume.prod Papers.OrendayLaresRockel2026XiBeta.bernoulliHalf)

instance Papers.OrendayLaresRockel2026XiBeta.instIsProbabilityMeasureForallFinOfNatNatElemRealUnitIntervalLawVb (b : ℝ) : MeasureTheory.IsProbabilityMeasure (lawVb b)

theorem Papers.OrendayLaresRockel2026XiBeta.rightSection_B {b : ℝ} (hb : b ∈ Set.Icc 0 1) {t : ℝ} (ht : 0 ≤ t) : (rightSection b hb).B t = 1 / 2 + t - rbA b t

theorem Papers.OrendayLaresRockel2026XiBeta.kerR_rightSection {b : ℝ} (hb : b ∈ Set.Icc 0 1) {t v : ℝ} (ht : t ∈ Set.Icc 0 1) (hne : t ≠ 1 - b / 2) : (rightSection b hb).kerR v t = ((if vbReal b t false ≤ v then 1 else 0) + if vbReal b t true ≤ v then 1 else 0) / 2

The kernel of R_b at t ≠ 1 - b/2 is the law of V_b given U = t.

theorem Papers.OrendayLaresRockel2026XiBeta.volume_coe_eq_null (c : ℝ) : MeasureTheory.volume {t : ↑unitInterval | ↑t = c} = 0

theorem Papers.OrendayLaresRockel2026XiBeta.cdf_lawVb {b : ℝ} (hb : b ∈ Set.Icc 0 1) (u v : ↑unitInterval) : (lawVb b).real (Set.Iic ![u, v]) = (Rb b hb).cdf ![u, v]

The distribution function of the law of (U, V_b) is that of R_b.

theorem Papers.OrendayLaresRockel2026XiBeta.measure_eq_of_real_Iic_eq (μ ν : MeasureTheory.Measure (Fin 2 → ↑unitInterval)) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] (h : ∀ (w : Fin 2 → ↑unitInterval), μ.real (Set.Iic w) = ν.real (Set.Iic w)) : μ = ν

Two probability measures on the unit square with equal distribution functions coincide.

theorem Papers.OrendayLaresRockel2026XiBeta.Rb_toMeasure_eq_lawVb {b : ℝ} (hb : b ∈ Set.Icc 0 1) : (Rb b hb).toMeasure = lawVb b

Proposition 5.3, first statement: the measure of R_b is the law of (U, V_b).