def median_set (A : Finset ℝ) : Set ℝ

Definition 3.13: median_set A is the set of real numbers β such that at least half of the elements of the finite nonempty set A lie below β and at least half lie above β.

@[simp]

theorem median_set_empty : median_set ∅ = ∅

The median set of the empty finite set is empty.

theorem median_set_eq_inter_of_nonempty {A : Finset ℝ} (hA : A.Nonempty) : median_set A = {β : ℝ | A.card ≤ 2 * {a ∈ A | a ≤ β}.card} ∩ {β : ℝ | A.card ≤ 2 * {a ∈ A | β ≤ a}.card}

For a nonempty finite set, median_set A is exactly the intersection of the two defining counting conditions.

theorem mem_median_set_iff_of_nonempty {A : Finset ℝ} (hA : A.Nonempty) {β : ℝ} : β ∈ median_set A ↔ A.card ≤ 2 * {a ∈ A | a ≤ β}.card ∧ A.card ≤ 2 * {a ∈ A | β ≤ a}.card

For a nonempty finite set, membership in median_set A means satisfying the two median-count inequalities.

@[simp]

theorem mem_median_set_iff {A : Finset ℝ} {β : ℝ} : β ∈ median_set A ↔ A.Nonempty ∧ A.card ≤ 2 * {a ∈ A | a ≤ β}.card ∧ A.card ≤ 2 * {a ∈ A | β ≤ a}.card

Membership in median_set A is equivalent to A being nonempty together with the two median-count inequalities.

theorem median_set_eq_singleton_of_strictMono_odd (m : ℕ) (a : Fin (2 * m + 1) → ℝ) (ha : StrictMono a) : median_set (Finset.image a Finset.univ) = {a (Fin.ofNat (2 * m + 1) m)}

The odd-case characterization from Definition 3.13: for a strictly increasing odd tuple, the median set is the singleton containing the middle entry.

theorem median_set_eq_Icc_of_strictMono_even (m : ℕ) (a : Fin (2 * (m + 1)) → ℝ) (ha : StrictMono a) : median_set (Finset.image a Finset.univ) = Set.Icc (a (Fin.ofNat (2 * (m + 1)) m)) (a (Fin.ofNat (2 * (m + 1)) (m + 1)))

The even-case characterization from Definition 3.13: for a strictly increasing even tuple, the median set is the closed interval between the two middle entries.