Algebraic core of the two-point mixture lemma

This file develops the two-point mixture decomposition used in the proof of Theorem 2.1. It isolates the equality of the lower and upper first moments and constructs the mean-one two-point law Q_{x,y}.

noncomputable def Feige.belowMoment (μ : MeasureTheory.Measure ℝ) : ℝ

The lower absolute first moment around one.

Equations

• Feige.belowMoment μ = ∫ (x : ℝ), (|x - 1| - (x - 1)) / 2 ∂μ

noncomputable def Feige.aboveMoment (μ : MeasureTheory.Measure ℝ) : ℝ

The upper absolute first moment around one.

Equations

• Feige.aboveMoment μ = ∫ (x : ℝ), (|x - 1| + (x - 1)) / 2 ∂μ

theorem Feige.integrable_sub_one {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsFiniteMeasure μ] (hμ : MeasureTheory.Integrable (fun (x : ℝ) => x) μ) : MeasureTheory.Integrable (fun (x : ℝ) => x - 1) μ

theorem Feige.integrable_abs_sub_one {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsFiniteMeasure μ] (hμ : MeasureTheory.Integrable (fun (x : ℝ) => x) μ) : MeasureTheory.Integrable (fun (x : ℝ) => |x - 1|) μ

theorem Feige.belowMoment_eq_aboveMoment {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsProbabilityMeasure μ] (hμ : MeasureTheory.Integrable (fun (x : ℝ) => x) μ) (hmean : ∫ (x : ℝ), x ∂μ = 1) : belowMoment μ = aboveMoment μ

The two expressions for M agree whenever the law has mean one. No support assumption is needed for this algebraic identity.

noncomputable def Feige.twoPointLowerWeight (x y : ℝ) : ℝ

Lower weight in the mean-one law supported on x < 1 < y.

Equations

• Feige.twoPointLowerWeight x y = (y - 1) / (y - x)

noncomputable def Feige.twoPointUpperWeight (x y : ℝ) : ℝ

Upper weight in the mean-one law supported on x < 1 < y.

Equations

• Feige.twoPointUpperWeight x y = (1 - x) / (y - x)

theorem Feige.twoPointWeights_nonneg {x y : ℝ} (hxy : x < y) (hx : x ≤ 1) (hy : 1 ≤ y) : 0 ≤ twoPointLowerWeight x y ∧ 0 ≤ twoPointUpperWeight x y

theorem Feige.twoPointWeights_add {x y : ℝ} (hxy : x ≠ y) : twoPointLowerWeight x y + twoPointUpperWeight x y = 1

noncomputable def Feige.twoPointMeasure (x y : ℝ) : MeasureTheory.Measure ℝ

The mean-one two-point law, expressed as a genuine nonnegative measure.

Equations

• Feige.twoPointMeasure x y = ENNReal.ofReal (Feige.twoPointLowerWeight x y) • MeasureTheory.Measure.dirac x + ENNReal.ofReal (Feige.twoPointUpperWeight x y) • MeasureTheory.Measure.dirac y

theorem Feige.twoPointMeasure_isProbability {x y : ℝ} (hx : x ≤ 1) (hy : 1 ≤ y) (hxy : x < y) : MeasureTheory.IsProbabilityMeasure (twoPointMeasure x y)

theorem Feige.twoPointMeasure_mean {x y : ℝ} (hx : x ≤ 1) (hy : 1 ≤ y) (hxy : x < y) : ∫ (z : ℝ), z ∂twoPointMeasure x y = 1

theorem Feige.twoPointMeasure_scaled_apply {x y : ℝ} (hx : x ≤ 1) (hy : 1 ≤ y) (hxy : x < y) (B : Set ℝ) : ENNReal.ofReal (y - x) * (twoPointMeasure x y) B = ENNReal.ofReal (y - 1) * (MeasureTheory.Measure.dirac x) B + ENNReal.ofReal (1 - x) * (MeasureTheory.Measure.dirac y) B

Pointwise algebra behind the two-point mixture formula.

noncomputable def Feige.expandedTwoPointMixture (μ : MeasureTheory.Measure ℝ) (M : ℝ) : MeasureTheory.Measure ℝ

The measure obtained after expanding the double integral in the two-point mixture formula.

The first restricted measure is multiplied by the upper moment (integration in y), and the second by the lower moment (integration in x).

Equations

• One or more equations did not get rendered due to their size.

theorem Feige.restrict_below_add_atom_add_above (μ : MeasureTheory.Measure ℝ) : μ.restrict (Set.Iio 1) + μ {1} • MeasureTheory.Measure.dirac 1 + μ.restrict (Set.Ioi 1) = μ

Splitting a measure at one into its below, atom, and above pieces.

theorem Feige.expandedTwoPointMixture_eq {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsProbabilityMeasure μ] (hμ : MeasureTheory.Integrable (fun (x : ℝ) => x) μ) (hmean : ∫ (x : ℝ), x ∂μ = 1) (hM : 0 < belowMoment μ) : expandedTwoPointMixture μ (belowMoment μ) = μ

The two-point mixture formula after evaluating its two product integrals. The support assumption is not needed for this final algebraic identity; it is needed only to ensure that the sampled lower point is nonnegative.

theorem Feige.twoPointMixture_formula42 {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsProbabilityMeasure μ] (hμ : MeasureTheory.Integrable (fun (x : ℝ) => x) μ) (hmean : ∫ (x : ℝ), x ∂μ = 1) (hM : 0 < belowMoment μ) : expandedTwoPointMixture μ (belowMoment μ) = μ

The two-point mixture formula at the canonical lower moment.

theorem Feige.belowMoment_nonneg {μ : MeasureTheory.Measure ℝ} : 0 ≤ belowMoment μ

The lower moment is nonnegative.

theorem Feige.eq_dirac_one_of_belowMoment_eq_zero {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsProbabilityMeasure μ] (hμ : MeasureTheory.Integrable (fun (x : ℝ) => x) μ) (hmean : ∫ (x : ℝ), x ∂μ = 1) (hM : belowMoment μ = 0) : μ = MeasureTheory.Measure.dirac 1

The degenerate branch of the mixture decomposition: if M = 0, a mean-one probability law is concentrated at one.

theorem Feige.twoPointMixture_dichotomy {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsProbabilityMeasure μ] (hμ : MeasureTheory.Integrable (fun (x : ℝ) => x) μ) (hmean : ∫ (x : ℝ), x ∂μ = 1) : μ = MeasureTheory.Measure.dirac 1 ∨ 0 < belowMoment μ ∧ expandedTwoPointMixture μ (belowMoment μ) = μ

Full mixture dichotomy: either the law is the degenerate law at one, or its positive lower moment gives the two-point mixture formula.