Proposition 2: exact support and its convexity #
theorem
Papers.AnsariRockel2026XiRho.sourceBand_support_set
(b : ℝ)
(hb : 0 < b)
:
(MeasureTheory.Measure.map (fun (u : Fin 2 → ↑unitInterval) (i : Fin 2) => ↑(u i))
(sourceBand b hb).toMeasure).support = Verification.bandSupport b
The real-coordinate support of the actual source copula is the explicit closed band.
theorem
Papers.AnsariRockel2026XiRho.sourceBand_support_iff
(b : ℝ)
(hb : 0 < b)
(x : Fin 2 → ℝ)
:
x ∈ (MeasureTheory.Measure.map (fun (u : Fin 2 → ↑unitInterval) (i : Fin 2) => ↑(u i))
(sourceBand b hb).toMeasure).support ↔ (∀ (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)
Membership includes the entire boundary of the support.
theorem
Papers.AnsariRockel2026XiRho.sourceBand_support_convex
(b : ℝ)
(hb : 0 < b)
:
Convex ℝ
(MeasureTheory.Measure.map (fun (u : Fin 2 → ↑unitInterval) (i : Fin 2) => ↑(u i))
(sourceBand b hb).toMeasure).support
Convexity is proved for the topological support of the actual probability measure.