← Mathematical handbook

Sampling a quadratic band from two independent uniforms

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

The second rank is the CDF transform of Z-b*(1-U)^2.

Equations

• Verification.quadraticSample b p = ![p.1, Verification.quadraticMeanUnit b (↑p.2 - b * (1 - ↑p.1) ^ 2)]

theorem Verification.continuous_quadraticSample (b : ℝ) : Continuous (quadraticSample b)

theorem Verification.quadraticSample_intercept_mem {b : ℝ} (hb : 0 ≤ b) (u z : ↑unitInterval) : ↑z - b * (1 - ↑u) ^ 2 ∈ Set.Icc (-b) 1

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

The complete lower-orthant distribution of the sampled vector.

theorem Verification.quadraticBand_toMeasure_sample (b : ℝ) (hb : 0 ≤ b) : (quadraticBand b hb).toMeasure = MeasureTheory.Measure.map (quadraticSample b) MeasureTheory.volume

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

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

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

theorem Verification.quadraticBand_cdf_sample (b : ℝ) (hb : 0 ≤ b) (u z : ↑unitInterval) : (quadraticBand b hb).cdf (quadraticSample b (u, z)) = ∫ (t : ↑unitInterval) in Set.Iic u, unitClamp (↑z - b * (1 - ↑u) ^ 2 + b * (1 - ↑t) ^ 2)

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