← Mathematical handbook

Lemma 5.1 (i), (ii): the maximal completion Q_A of a median section

For s : MedianSection (with section A and companion B) the kernel of Q_A puts mass p(u) at A(u) and mass 1 - p(u) at B(u); its distribution function in the response threshold v is kerR. The copula s.completion is built from this kernel (copulaOfConditionalAE), its distribution function is the closed form (5.1) of the source, and it is stochastically increasing with median section A. Part (ii) says that it is the largest copula with median section A.

theorem Papers.OrendayLaresRockel2026XiBeta.intervalIntegrable_mul_ite {x : ℝ → ℝ} {a b : ℝ} (hx : IntervalIntegrable x MeasureTheory.volume a b) (P : ℝ → Prop) [DecidablePred P] (hP : MeasurableSet {t : ℝ | P t}) : IntervalIntegrable (fun (t : ℝ) => x t * if P t then 1 else 0) MeasureTheory.volume a b

A density times the indicator of a measurable set stays interval integrable.

theorem Papers.OrendayLaresRockel2026XiBeta.integral_mul_indicator_primitive {x : ℝ → ℝ} (hxi : ∀ (a b : ℝ), IntervalIntegrable x MeasureTheory.volume a b) {u a v : ℝ} (hu : 0 ≤ u) (hx : ∀ t ∈ Set.Icc 0 u, 0 ≤ x t) (hav : a ≤ v) : (∫ (t : ℝ) in 0..u, x t * if a + ∫ (r : ℝ) in 0..t, x r ≤ v then 1 else 0) = min (a + ∫ (r : ℝ) in 0..u, x r) v - a

The integral of a nonnegative density against the indicator of a sublevel set of its own primitive is min (X u) v - a.

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.half_mul_le_A (s : MedianSection) {u : ℝ} (hu : 0 ≤ u) (hu1 : u ≤ 1) : u / 2 ≤ s.A u

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.B_eq_integral (s : MedianSection) (t : ℝ) : s.B t = 1 / 2 + ∫ (r : ℝ) in 0..t, 1 - s.p r

noncomputable def Papers.OrendayLaresRockel2026XiBeta.MedianSection.kerR (s : MedianSection) (v t : ℝ) : ℝ

The distribution function in the response threshold v of the kernel of Q_A at the conditioning point t: mass p(t) at A(t) and mass 1 - p(t) at B(t).

Equations

• s.kerR v t = (s.p t * if s.A t ≤ v then 1 else 0) + (1 - s.p t) * if s.B t ≤ v then 1 else 0

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.kerR_of_lt (s : MedianSection) {v t : ℝ} (hv : v < 1 / 2) (ht : 0 ≤ t) : s.kerR v t = s.p t * if s.A t ≤ v then 1 else 0

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.kerR_of_ge (s : MedianSection) {v t : ℝ} (hv : 1 / 2 ≤ v) (ht : t ≤ 1) : s.kerR v t = s.p t + (1 - s.p t) * if s.B t ≤ v then 1 else 0

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.kerR_nonneg (s : MedianSection) {v t : ℝ} (ht0 : 0 ≤ t) (ht1 : t ≤ 1) : 0 ≤ s.kerR v t

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.kerR_le_one (s : MedianSection) {v t : ℝ} (ht0 : 0 ≤ t) (ht1 : t ≤ 1) : s.kerR v t ≤ 1

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.kerR_mono (s : MedianSection) {v v' t : ℝ} (hv : v ≤ v') (ht0 : 0 ≤ t) (ht1 : t ≤ 1) : s.kerR v t ≤ s.kerR v' t

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.kerR_anti (s : MedianSection) {v t t' : ℝ} (ht0 : 0 ≤ t) (htt : t ≤ t') (ht1 : t' ≤ 1) : s.kerR v t' ≤ s.kerR v t

noncomputable def Papers.OrendayLaresRockel2026XiBeta.MedianSection.Qfun (s : MedianSection) (u v : ℝ) : ℝ

The closed form (5.1) of the maximal completion Q_A.

Equations

• s.Qfun u v = if v ≤ 1 / 2 then min (s.A u) v else min u (s.A u + v - 1 / 2)

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.measurableSet_A_le (s : MedianSection) (v : ℝ) : MeasurableSet {t : ℝ | s.A t ≤ v}

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.measurableSet_B_le (s : MedianSection) (v : ℝ) : MeasurableSet {t : ℝ | s.B t ≤ v}

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.integral_kerR (s : MedianSection) {u v : ℝ} (hu : 0 ≤ u) (hu1 : u ≤ 1) (hv : 0 ≤ v) : ∫ (t : ℝ) in 0..u, s.kerR v t = s.Qfun u v

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.measurable_kerR (s : MedianSection) (v : ℝ) : Measurable (s.kerR v)

noncomputable def Papers.OrendayLaresRockel2026XiBeta.MedianSection.kernelCDF (s : MedianSection) (v u : ↑unitInterval) : ℝ

The conditional distribution function v ↦ P(V ≤ v | U = u) of Q_A on the unit interval.

Equations

• s.kernelCDF v u = s.kerR ↑v ↑u

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.measurable_kernelCDF (s : MedianSection) (v : ↑unitInterval) : Measurable (s.kernelCDF v)

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.kernelCDF_mem (s : MedianSection) (v u : ↑unitInterval) : s.kernelCDF v u ∈ Set.Icc 0 1

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.integrable_kernelCDF (s : MedianSection) (v : ↑unitInterval) : MeasureTheory.Integrable (s.kernelCDF v) MeasureTheory.volume

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.monotone_kernelCDF (s : MedianSection) (u : ↑unitInterval) : Monotone fun (v : ↑unitInterval) => s.kernelCDF v u

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.antitone_kernelCDF (s : MedianSection) (v : ↑unitInterval) : Antitone (s.kernelCDF v)

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.kernelCDF_one (s : MedianSection) (u : ↑unitInterval) : s.kernelCDF 1 u = 1

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.kernelCDF_zero (s : MedianSection) (u : ↑unitInterval) (hu : u ≠ 0) : s.kernelCDF 0 u = 0

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.kernelCDF_zero_ae (s : MedianSection) : s.kernelCDF 0 =ᵐ[MeasureTheory.volume] fun (x : ↑unitInterval) => 0

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.integral_kernelCDF_Iic (s : MedianSection) (u v : ↑unitInterval) : ∫ (t : ↑unitInterval) in Set.Iic u, s.kernelCDF v t = s.Qfun ↑u ↑v

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.Qfun_one (s : MedianSection) {v : ℝ} (hv1 : v ≤ 1) : s.Qfun 1 v = v

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.integral_kernelCDF (s : MedianSection) (v : ↑unitInterval) : ∫ (t : ↑unitInterval), s.kernelCDF v t = ↑v

noncomputable def Papers.OrendayLaresRockel2026XiBeta.MedianSection.completion (s : MedianSection) : ProbabilityTheory.Copula 2

The maximal completion Q_A of the median section (Lemma 5.1), a genuine bivariate copula whose Markov kernel has distribution function kernelCDF (mass p(u) at A(u), mass 1 - p(u) at B(u)).

Equations

• s.completion = Verification.copulaOfConditionalAE s.kernelCDF ⋯ ⋯ ⋯ ⋯ ⋯

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.cdf_completion (s : MedianSection) (u v : ↑unitInterval) : s.completion.cdf ![u, v] = s.Qfun ↑u ↑v

Equation (5.1): the distribution function of Q_A.

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.conditionalCDF_completion (s : MedianSection) (v : ↑unitInterval) : (fun (u : ↑unitInterval) => s.completion.conditionalCDF u v) =ᵐ[MeasureTheory.volume] s.kernelCDF v

The Markov kernel of Q_A: for a.e. u the conditional distribution function of V given U = u is p(u) 1{A(u) ≤ v} + (1 - p(u)) 1{B(u) ≤ v}.

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.cdf_completion_eq_integral (s : MedianSection) (u v : ↑unitInterval) : s.completion.cdf ![u, v] = ∫ (t : ↑unitInterval) in Set.Iic u, s.kernelCDF v t

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.cdf_completion_of_le_half (s : MedianSection) (u v : ↑unitInterval) (hv : ↑v ≤ 1 / 2) : s.completion.cdf ![u, v] = min (s.A ↑u) ↑v

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.cdf_completion_of_half_le (s : MedianSection) (u v : ↑unitInterval) (hv : 1 / 2 ≤ ↑v) : s.completion.cdf ![u, v] = min (↑u) (s.A ↑u + ↑v - 1 / 2)

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.completion_isSI (s : MedianSection) : s.completion.IsSI

Lemma 5.1 (i): Q_A is stochastically increasing.

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.cdf_completion_half (s : MedianSection) (u : ↑unitInterval) : s.completion.cdf ![u, ProbabilityTheory.Copula.unitHalf] = s.A ↑u

Lemma 5.1 (i): the median section of Q_A is A.

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.cdf_le_completion (s : MedianSection) (C : ProbabilityTheory.Copula 2) (hC : ∀ (u : ↑unitInterval), C.cdf ![u, ProbabilityTheory.Copula.unitHalf] = s.A ↑u) (u v : ↑unitInterval) : C.cdf ![u, v] ≤ s.completion.cdf ![u, v]

Lemma 5.1 (ii): every copula with median section A lies below Q_A.

noncomputable def Papers.OrendayLaresRockel2026XiBeta.MedianSection.atomA (s : MedianSection) (u : ↑unitInterval) : ↑unitInterval

The atom A(u) of the kernel of Q_A, as a point of the unit interval.

Equations

• s.atomA u = ⟨s.A ↑u, ⋯⟩

noncomputable def Papers.OrendayLaresRockel2026XiBeta.MedianSection.atomB (s : MedianSection) (u : ↑unitInterval) : ↑unitInterval

The atom B(u) of the kernel of Q_A, as a point of the unit interval.

Equations

• s.atomB u = ⟨s.B ↑u, ⋯⟩

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.atomA_le_iff (s : MedianSection) (u v : ↑unitInterval) : s.atomA u ≤ v ↔ s.A ↑u ≤ ↑v

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.atomB_le_iff (s : MedianSection) (u v : ↑unitInterval) : s.atomB u ≤ v ↔ s.B ↑u ≤ ↑v

noncomputable def Papers.OrendayLaresRockel2026XiBeta.MedianSection.kernelMeasure (s : MedianSection) (u : ↑unitInterval) : MeasureTheory.Measure ↑unitInterval

The Markov kernel of Q_A: mass p(u) at A(u) and mass 1 - p(u) at B(u).

Equations

• s.kernelMeasure u = ENNReal.ofReal (s.p ↑u) • MeasureTheory.Measure.dirac (s.atomA u) + ENNReal.ofReal (1 - s.p ↑u) • MeasureTheory.Measure.dirac (s.atomB u)

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.kernelMeasure_real_Iic (s : MedianSection) (v u : ↑unitInterval) : (s.kernelMeasure u).real (Set.Iic v) = s.kernelCDF v u

The distribution function of kernelMeasure is kernelCDF.

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.completion_congr (s t : MedianSection) (h : ∀ u ∈ Set.Icc 0 1, s.A u = t.A u) : s.completion = t.completion

The maximal completion depends only on the section A (on [0,1]).