Median

Ported from scottnarmstrong/CoarseGraining at c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4. Module imports, support namespace and local option directives adapted for Lean Pool.

Two-function median

A standalone measure-theory prelude. For a finite measure μ on α and two almost-everywhere measurable real functions f g, there is a real level m such that both the total upper mass and the total lower mass of the pair (f, g) across the two copies of α stay below μ univ:

μ {m < f} + μ {m < g} ≤ μ univ and μ {f < m} + μ {g < m} ≤ μ univ.

This is exactly the statement that m is a median of the combined function on the disjoint union of two copies of α, phrased without sum types.

No sorry, no axioms, no heartbeat overrides.

theorem HCPolySupport.exists_two_function_median {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {f g : α → ℝ} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) : ∃ (m : ℝ), μ {x : α | m < f x} + μ {x : α | m < g x} ≤ μ Set.univ ∧ μ {x : α | f x < m} + μ {x : α | g x < m} ≤ μ Set.univ

Two-function median. For a finite measure and two a.e.-measurable real functions, there is a common level m at which the combined upper mass and the combined lower mass are each at most the total mass.