Documentation

Papers.OrendayLaresRockel2026XiBeta.RBranchSingular

← Mathematical handbook

R_b is the copula of (U, V_b) and is singular (Proposition 5.3 (i)) #

The support of R_b is a finite union of line segments (three graphs of affine maps), a Lebesgue null set carrying all the mass; hence R_b is singular and has no density.

source
noncomputable def Papers.OrendayLaresRockel2026XiBeta.probVb :
MeasureTheory.ProbabilityMeasure (↑unitInterval × Bool)

The underlying probability space I × Bool (uniform U and independent fair coin ε).

Equations
Instances For
    source
    theorem Papers.OrendayLaresRockel2026XiBeta.marginals_Xb {b : ℝ} (hb : b ∈ Set.Icc 0 1) (i : Fin 2) :
    MeasureTheory.Measure.map (fun (ω : ↑unitInterval × Bool) => Xb b ω i) ↑probVb = MeasureTheory.volume
    source
    theorem Papers.OrendayLaresRockel2026XiBeta.Rb_eq_ofMap {b : ℝ} (hb : b ∈ Set.Icc 0 1) :
    Rb b hb = ProbabilityTheory.Copula.ofMap probVb (Xb b) ⋯ ⋯

    Proposition 5.3, first statement: R_b is the copula of the random vector (U, V_b).

    source
    theorem Papers.OrendayLaresRockel2026XiBeta.Vb_uniform {b : ℝ} (hb : b ∈ Set.Icc 0 1) :
    MeasureTheory.Measure.map (fun (ω : ↑unitInterval × Bool) => Vb b ω.1 ω.2) ↑probVb = MeasureTheory.volume

    V_b is uniformly distributed on [0,1].

    source
    theorem Papers.OrendayLaresRockel2026XiBeta.volume_graph_null (f : ↑unitInterval → ℝ) (hf : Measurable f) :
    MeasureTheory.volume {x : Fin 2 → ↑unitInterval | ↑(x 1) = f (x 0)} = 0
    source
    def Papers.OrendayLaresRockel2026XiBeta.supportGraphs (b : ℝ) :
    Set (Fin 2 → ↑unitInterval)

    The support of R_b: three line segments (graphs of v = u, v = (2u + b)/4, v = (2u + b)/4 + (1 - b)/2).

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem Papers.OrendayLaresRockel2026XiBeta.measurableSet_supportGraphs (b : ℝ) :
      MeasurableSet (supportGraphs b)
      source
      theorem Papers.OrendayLaresRockel2026XiBeta.volume_supportGraphs (b : ℝ) :
      MeasureTheory.volume (supportGraphs b) = 0
      source
      theorem Papers.OrendayLaresRockel2026XiBeta.Xb_mem_supportGraphs {b : ℝ} (hb : b ∈ Set.Icc 0 1) (p : ↑unitInterval × Bool) :
      Xb b p ∈ supportGraphs b
      source
      theorem Papers.OrendayLaresRockel2026XiBeta.Rb_singular {b : ℝ} (hb : b ∈ Set.Icc 0 1) :
      (Rb b hb).toMeasure.MutuallySingular MeasureTheory.volume

      Proposition 5.3 (i): R_b is singular: it lives on a finite union of line segments, a Lebesgue null set.

      source
      theorem Papers.OrendayLaresRockel2026XiBeta.Rb_not_absolutelyContinuous {b : ℝ} (hb : b ∈ Set.Icc 0 1) :
      ¬(Rb b hb).toMeasure.AbsolutelyContinuous MeasureTheory.volume

      R_b has no Lebesgue density: it is not absolutely continuous.