← Mathematical handbook

Exact topological support of the sampled diagonal band

noncomputable def Verification.bandLowerEdge (b u : ℝ) : ℝ

Closed-form lower edge of the support, as a convex function on the real line.

Equations

• Verification.bandLowerEdge b u = u - 1 / (2 * b) + max 0 (1 - b * u) ^ 2 / (2 * b)

theorem Verification.bandLowerEdge_eq_mean {b : ℝ} (hb : 0 < b) (u : ↑unitInterval) : bandLowerEdge b ↑u = clampedMean b (b * ↑u)

theorem Verification.bandUpperEdge_eq_mean {b : ℝ} (hb : 0 < b) (u : ↑unitInterval) : 1 - bandLowerEdge b (1 - ↑u) = clampedMean b (1 + b * ↑u)

noncomputable def Verification.bandSupport (b : ℝ) : Set (Fin 2 → ℝ)

Equations

• Verification.bandSupport b = {x : Fin 2 → ℝ | (∀ (i : Fin 2), x i ∈ Set.Icc 0 1) ∧ Verification.bandLowerEdge b (x 0) ≤ x 1 ∧ x 1 ≤ 1 - Verification.bandLowerEdge b (1 - x 0)}

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

Equations

• Verification.bandSampleReal b p i = ↑(Verification.bandSample b p i)

theorem Verification.continuous_bandSampleReal (b : ℝ) : Continuous (bandSampleReal b)

theorem Verification.range_bandSampleReal {b : ℝ} (hb : 0 < b) : Set.range (bandSampleReal b) = bandSupport b

theorem Verification.support_map_uniform (f : ↑unitInterval × ↑unitInterval → Fin 2 → ℝ) (hf : Continuous f) : (MeasureTheory.Measure.map f MeasureTheory.volume).support = Set.range f

theorem Verification.diagonalBand_support_set {b : ℝ} (hb : 0 < b) : (MeasureTheory.Measure.map (fun (u : Fin 2 → ↑unitInterval) (i : Fin 2) => ↑(u i)) (diagonalBand b ⋯).toMeasure).support = bandSupport b

The topological support of the actual copula, embedded in the real square.