← Mathematical handbook

Sampling a diagonal band from two independent uniforms

noncomputable def Verification.bandSample (b : ℝ) (p : ↑unitInterval × ↑unitInterval) : Fin 2 → ↑unitInterval

The second rank is the CDF transform of b*U+Z.

Equations

• Verification.bandSample b p = ![p.1, Verification.clampedMeanUnit b (b * ↑p.1 + ↑p.2)]

theorem Verification.continuous_bandSample (b : ℝ) : Continuous (bandSample b)

theorem Verification.bandSample_intercept_mem {b : ℝ} (hb : 0 ≤ b) (u z : ↑unitInterval) : b * ↑u + ↑z ∈ Set.Icc 0 (b + 1)

theorem Verification.integral_unit_le_real (r : ℝ) : (∫ (z : ↑unitInterval), if ↑z ≤ r then 1 else 0) = unitClamp r

theorem Verification.bandSample_orthant (b : ℝ) (hb : 0 ≤ b) (u v : ↑unitInterval) : (∫ (p : ↑unitInterval × ↑unitInterval), if bandSample b p ≤ ![u, v] then 1 else 0) = (diagonalBand b hb).cdf ![u, v]

The complete lower-orthant distribution of the sampled vector.

theorem Verification.diagonalBand_toMeasure_sample (b : ℝ) (hb : 0 ≤ b) : (diagonalBand b hb).toMeasure = MeasureTheory.Measure.map (bandSample b) MeasureTheory.volume

The constructed copula is exactly the law of the sampled vector.

theorem Verification.diagonalBand_integral_sample (b : ℝ) (hb : 0 ≤ b) {f : (Fin 2 → ↑unitInterval) → ℝ} (hf : Continuous f) : ∫ (x : Fin 2 → ↑unitInterval), f x ∂(diagonalBand b hb).toMeasure = ∫ (u : ↑unitInterval) (z : ↑unitInterval), f (bandSample b (u, z))

Integrals under the band can be evaluated on two independent uniforms.

theorem Verification.diagonalBand_cdf_sample (b : ℝ) (hb : 0 ≤ b) (u z : ↑unitInterval) : (diagonalBand b hb).cdf (bandSample b (u, z)) = ∫ (t : ↑unitInterval) in Set.Iic u, unitClamp (b * ↑u + ↑z - b * ↑t)

The CDF at the sampled point has a simple affine clamped integrand.