Documentation

Papers.OrendayLaresRockel2026XiBeta.MedianSection

← Mathematical handbook

Section 5: median sections and the gap function #

The set S of median sections of the source is encoded through the slope p of the section: a nonincreasing function with values in [0,1] on [0,1] and ∫₀¹ p = 1/2. The section itself is A(u) = ∫₀ᵘ p, the companion is B(u) = 1/2 + u - A(u), and the gap function of equation (5.2) is w = B - A. Only the values of p on [0,1] matter; the global monotonicity is a harmless normalization (every nonincreasing p on [0,1] has such an extension) that makes interval-integral calculus and the countability of discontinuities available without side conditions.

structure Papers.OrendayLaresRockel2026XiBeta.MedianSection :

An element of the set S of Section 5: a median section A(u) = ∫₀ᵘ p, with p nonincreasing, 0 ≤ p ≤ 1 on [0,1] and ∫₀¹ p = 1/2.

p : ℝ → ℝ
the slope of the median section
antitone : Antitone self.p
nonneg : 0 ≤ self.p 1
le_one : self.p 0 ≤ 1
integral_eq : ∫ (t : ℝ) in 0..1, self.p t = 1 / 2

Instances For

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.p_nonneg (s : MedianSection) {u : ℝ} (hu : u ≤ 1) :

0 ≤ s.p u

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.p_le_one (s : MedianSection) {u : ℝ} (hu : 0 ≤ u) :

s.p u ≤ 1

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.intervalIntegrable_p (s : MedianSection) (a b : ℝ) :

IntervalIntegrable s.p MeasureTheory.volume a b

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

The median section A(u) = ∫₀ᵘ p.

Equations

s.A u = ∫ (t : ℝ) in 0..u, s.p t

Instances For

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

The companion B(u) = 1/2 + u - A(u) of the median section.

Equations

s.B u = 1 / 2 + u - s.A u

Instances For

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

The gap function w = B - A of equation (5.2).

Equations

s.gap u = s.B u - s.A u

Instances For

@[simp]

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.A_zero (s : MedianSection) :

s.A 0 = 0

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.A_one (s : MedianSection) :

s.A 1 = 1 / 2

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.A_sub (s : MedianSection) {a b : ℝ} :

s.A b - s.A a = ∫ (t : ℝ) in a..b, s.p t

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.gap_eq (s : MedianSection) (u : ℝ) :

s.gap u = 1 / 2 + u - 2 * s.A u

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.B_zero (s : MedianSection) :

s.B 0 = 1 / 2

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.B_one (s : MedianSection) :

s.B 1 = 1

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.gap_zero (s : MedianSection) :

s.gap 0 = 1 / 2

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.gap_one (s : MedianSection) :

s.gap 1 = 1 / 2

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.A_mono (s : MedianSection) {a b : ℝ} (hab : a ≤ b) (hb : b ≤ 1) :

s.A a ≤ s.A b

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.A_sub_le (s : MedianSection) {a b : ℝ} (ha : 0 ≤ a) (hab : a ≤ b) :

s.A b - s.A a ≤ b - a

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.abs_A_sub_le (s : MedianSection) {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (ha1 : a ≤ 1) (hb1 : b ≤ 1) :

|s.A b - s.A a| ≤ |b - a|

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.continuous_A (s : MedianSection) :

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.continuous_B (s : MedianSection) :

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.continuous_gap (s : MedianSection) :

Continuous s.gap

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.A_nonneg (s : MedianSection) {u : ℝ} (hu : 0 ≤ u) (hu1 : u ≤ 1) :

0 ≤ s.A u

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.A_le_half (s : MedianSection) {u : ℝ} (hu1 : u ≤ 1) :

s.A u ≤ 1 / 2

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.A_le_self (s : MedianSection) {u : ℝ} (hu : 0 ≤ u) :

s.A u ≤ u

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.A_ge (s : MedianSection) {u : ℝ} (hu : 0 ≤ u) (hu1 : u ≤ 1) :

u - 1 / 2 ≤ s.A u

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.half_le_B (s : MedianSection) {u : ℝ} (hu : 0 ≤ u) :

1 / 2 ≤ s.B u

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.B_le_one (s : MedianSection) {u : ℝ} (hu : 0 ≤ u) (hu1 : u ≤ 1) :

s.B u ≤ 1

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.B_mono (s : MedianSection) {a b : ℝ} (ha : 0 ≤ a) (hab : a ≤ b) :

s.B a ≤ s.B b

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.A_le_B (s : MedianSection) {u : ℝ} (hu : 0 ≤ u) (hu1 : u ≤ 1) :

s.A u ≤ s.B u

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.abs_le_gap (s : MedianSection) {u : ℝ} (hu : 0 ≤ u) (hu1 : u ≤ 1) :

|u - 1 / 2| ≤ s.gap u

The gap function lies above the tent |u - 1/2| (source, after (5.2)).

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.gap_nonneg (s : MedianSection) {u : ℝ} (hu : 0 ≤ u) (hu1 : u ≤ 1) :

0 ≤ s.gap u

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.gap_half (s : MedianSection) :

s.gap (1 / 2) = 1 - 2 * s.A (1 / 2)

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.gap_eq_integral (s : MedianSection) (u : ℝ) :

s.gap u = 1 / 2 + ∫ (t : ℝ) in 0..u, 1 - 2 * s.p t

The gap function is 1/2 + ∫₀ᵘ (1 - 2p), i.e. w' = 1 - 2p.

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.concaveOn_A (s : MedianSection) :

ConcaveOn ℝ (Set.Icc 0 1) s.A

A is concave on [0,1].

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.convexOn_gap (s : MedianSection) :

ConvexOn ℝ (Set.Icc 0 1) s.gap

The gap function is convex on [0,1] (source, after (5.2)).

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.abs_gap_sub_le (s : MedianSection) {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (ha1 : a ≤ 1) (hb1 : b ≤ 1) :

|s.gap b - s.gap a| ≤ |b - a|

The gap function is 1-Lipschitz on [0,1].

theorem Papers.OrendayLaresRockel2026XiBeta.exists_medianSection_of_isSI (C : ProbabilityTheory.Copula 2) (hC : C.IsSI) :

∃ (s : MedianSection), ∀ (u : ↑unitInterval), s.A ↑u = C.cdf ![u, ProbabilityTheory.Copula.unitHalf ]

The median section A = C(·, 1/2) of an SI copula belongs to S (source, paragraph before Lemma 5.1): p is a nonincreasing version of ∂₁C(·, 1/2).