A measurable kernel of mean-one two-point laws

This file supplies the measurable-kernel interface needed to condition on the latent two-point parameters in the proof of Theorem 2.1.

theorem Feige.measurable_twoPointMeasure_apply {B : Set ℝ} (hB : MeasurableSet B) : Measurable fun (p : ℝ × ℝ) => (twoPointMeasure p.1 p.2) B

Evaluation of the two-point law on a Borel set is measurable in both support points.

def Feige.TwoPointParams : Type

Admissible parameters x ≤ 1 ≤ y, with distinct support points.

Equations

• Feige.TwoPointParams = { p : ℝ × ℝ // p.1 ≤ 1 ∧ 1 ≤ p.2 ∧ p.1 < p.2 }

@[instance_reducible]

instance Feige.instMeasurableSpaceTwoPointParams : MeasurableSpace TwoPointParams

Equations

• Feige.instMeasurableSpaceTwoPointParams = MeasurableSpace.comap Subtype.val inferInstance

noncomputable def Feige.twoPointKernel : ProbabilityTheory.Kernel TwoPointParams ℝ

The Markov kernel sending (x,y) to the mean-one two-point law Q_{x,y}.

Equations

• Feige.twoPointKernel = { toFun := fun (p : Feige.TwoPointParams) => Feige.twoPointMeasure (↑p).1 (↑p).2, measurable' := Feige.twoPointKernel._proof_1 }

@[simp]

theorem Feige.twoPointKernel_apply (p : TwoPointParams) : twoPointKernel p = twoPointMeasure (↑p).1 (↑p).2

instance Feige.instIsMarkovKernelTwoPointParamsRealTwoPointKernel : ProbabilityTheory.IsMarkovKernel twoPointKernel

theorem Feige.twoPointKernel_mean (p : TwoPointParams) : ∫ (z : ℝ), z ∂twoPointKernel p = 1

theorem Feige.twoPointKernel_nonnegative_support (p : TwoPointParams) (hx : 0 ≤ (↑p).1) : (twoPointKernel p) (Set.Iio 0) = 0

noncomputable def Feige.kernelTwoPointMixture (ν : MeasureTheory.Measure TwoPointParams) : MeasureTheory.Measure ℝ

The genuine measure obtained by sampling latent two-point parameters and then sampling from their two-point law.

Equations

• Feige.kernelTwoPointMixture ν = ν.bind ⇑Feige.twoPointKernel

instance Feige.instIsProbabilityMeasureRealKernelTwoPointMixtureOfTwoPointParams (ν : MeasureTheory.Measure TwoPointParams) [MeasureTheory.IsProbabilityMeasure ν] : MeasureTheory.IsProbabilityMeasure (kernelTwoPointMixture ν)

theorem Feige.kernelTwoPointMixture_apply (ν : MeasureTheory.Measure TwoPointParams) {B : Set ℝ} (hB : MeasurableSet B) : (kernelTwoPointMixture ν) B = ∫⁻ (p : TwoPointParams), (twoPointMeasure (↑p).1 (↑p).2) B ∂ν

The Measure.bind formula for the two-point mixture.

theorem Feige.kernelTwoPointMixture_apply_le (ν : MeasureTheory.Measure TwoPointParams) [MeasureTheory.IsProbabilityMeasure ν] {B : Set ℝ} (hB : MeasurableSet B) {c : ENNReal} (hc : ∀ (p : TwoPointParams), (twoPointMeasure (↑p).1 (↑p).2) B ≤ c) : (kernelTwoPointMixture ν) B ≤ c

Averaging a pointwise probability bound over latent parameters.

def Feige.strictPairSet : Set (ℝ × ℝ)

The strict below-above region used for the nondegenerate latent pair.

Equations

• Feige.strictPairSet = {p : ℝ × ℝ | p.1 < 1 ∧ 1 < p.2}

theorem Feige.measurableSet_strictPairSet : MeasurableSet strictPairSet

theorem Feige.strictPairSet_admissible {p : ℝ × ℝ} (hp : p ∈ strictPairSet) : p.1 ≤ 1 ∧ 1 ≤ p.2 ∧ p.1 < p.2

Every strict below-above pair is an admissible two-point parameter.

@[instance_reducible]

noncomputable def Feige.instDecidablePredProdRealMemSetStrictPairSet : DecidablePred fun (x : ℝ × ℝ) => x ∈ strictPairSet

Classical decidability for membership in the strict parameter region.

Equations

• Feige.instDecidablePredProdRealMemSetStrictPairSet = Classical.decPred fun (x : ℝ × ℝ) => x ∈ Feige.strictPairSet

noncomputable def Feige.pairToParams (p : ℝ × ℝ) : TwoPointParams

A total measurable map into TwoPointParams; outside the strict region we use the harmless default pair (0,2). The weighted latent measure below is supported on the strict region.

Equations

• Feige.pairToParams p = if hp : p ∈ Feige.strictPairSet then ⟨p, ⋯⟩ else ⟨(0, 2), Feige.pairToParams._proof_2⟩

theorem Feige.measurable_pairToParams : Measurable pairToParams

noncomputable def Feige.belowAboveProduct (μ : MeasureTheory.Measure ℝ) : MeasureTheory.Measure (ℝ × ℝ)

The unnormalized product law on a strict below point and a strict above point.

Equations

• Feige.belowAboveProduct μ = (μ.restrict (Set.Iio 1)).prod (μ.restrict (Set.Ioi 1))

noncomputable def Feige.latentPairDensity (M : ℝ) (p : ℝ × ℝ) : ENNReal

The density (y-x)/M of the latent below/above pair, written in ℝ≥0∞.

Equations

• Feige.latentPairDensity M p = (ENNReal.ofReal M)⁻¹ * ENNReal.ofReal (p.2 - p.1)

theorem Feige.measurable_latentPairDensity (M : ℝ) : Measurable (latentPairDensity M)

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

The concrete weighted below×above latent measure.

Equations

• Feige.latentPairMeasure μ M = (Feige.belowAboveProduct μ).withDensity (Feige.latentPairDensity M)

theorem Feige.strictPairSet_eq_prod : strictPairSet = Set.Iio 1 ×ˢ Set.Ioi 1

theorem Feige.belowAboveProduct_compl_strictPairSet (μ : MeasureTheory.Measure ℝ) [MeasureTheory.SFinite μ] : (belowAboveProduct μ) strictPairSetᶜ = 0

theorem Feige.latentPairMeasure_compl_strictPairSet (μ : MeasureTheory.Measure ℝ) [MeasureTheory.SFinite μ] (M : ℝ) : (latentPairMeasure μ M) strictPairSetᶜ = 0

The weighted latent pair measure has no mass outside the strict below×above parameter region.

instance Feige.instSFiniteProdRealLatentPairMeasure (μ : MeasureTheory.Measure ℝ) [MeasureTheory.SFinite μ] (M : ℝ) : MeasureTheory.SFinite (latentPairMeasure μ M)

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

The weighted pair measure, transported to the admissible parameter subtype on which twoPointKernel is Markov.

Equations

• Feige.latentParamsMeasure μ M = MeasureTheory.Measure.map Feige.pairToParams (Feige.latentPairMeasure μ M)

theorem Feige.latentParamsMeasure_apply (μ : MeasureTheory.Measure ℝ) (M : ℝ) {A : Set TwoPointParams} (hA : MeasurableSet A) : (latentParamsMeasure μ M) A = (latentPairMeasure μ M) (pairToParams ⁻¹' A)

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

The resulting genuine kernel mixture of the nondegenerate latent component.

Equations

• Feige.nondegenerateKernelMixture μ M = Feige.kernelTwoPointMixture (Feige.latentParamsMeasure μ M)

theorem Feige.belowMoment_eq_integral_Iio (μ : MeasureTheory.Measure ℝ) : belowMoment μ = ∫ (x : ℝ) in Set.Iio 1, 1 - x ∂μ

The absolute-value definition of the lower moment is the usual restricted first moment below one.

theorem Feige.aboveMoment_eq_integral_Ioi (μ : MeasureTheory.Measure ℝ) : aboveMoment μ = ∫ (y : ℝ) in Set.Ioi 1, y - 1 ∂μ

The absolute-value definition of the upper moment is the usual restricted first moment above one.

theorem Feige.ofReal_belowMoment_eq_lintegral_Iio {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsFiniteMeasure μ] (hμ : MeasureTheory.Integrable (fun (x : ℝ) => x) μ) : ENNReal.ofReal (belowMoment μ) = ∫⁻ (x : ℝ) in Set.Iio 1, ENNReal.ofReal (1 - x) ∂μ

theorem Feige.ofReal_aboveMoment_eq_lintegral_Ioi {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsFiniteMeasure μ] (hμ : MeasureTheory.Integrable (fun (x : ℝ) => x) μ) : ENNReal.ofReal (aboveMoment μ) = ∫⁻ (y : ℝ) in Set.Ioi 1, ENNReal.ofReal (y - 1) ∂μ

theorem Feige.latentPairMeasure_univ {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsFiniteMeasure μ] (hμ : MeasureTheory.Integrable (fun (x : ℝ) => x) μ) (M : ℝ) : (latentPairMeasure μ M) Set.univ = (ENNReal.ofReal M)⁻¹ * (μ (Set.Iio 1) * ENNReal.ofReal (aboveMoment μ) + ENNReal.ofReal (belowMoment μ) * μ (Set.Ioi 1))

Tonelli expansion of the total mass of the nondegenerate latent pair measure.

theorem Feige.mass_below_add_above (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure μ] : μ (Set.Iio 1) + μ (Set.Ioi 1) = 1 - μ {1}

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

In the mean-one positive-moment branch, the nondegenerate latent component has precisely the mass outside the atom at one.

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

The full kernel mixture: the atom at one plus the nondegenerate latent two-point component.

Equations

• Feige.fullKernelMixture μ M = μ {1} • MeasureTheory.Measure.dirac 1 + Feige.nondegenerateKernelMixture μ M

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

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

theorem Feige.nondegenerateKernelMixture_apply_pair (μ : MeasureTheory.Measure ℝ) (M : ℝ) {B : Set ℝ} (hB : MeasurableSet B) : (nondegenerateKernelMixture μ M) B = ∫⁻ (p : ℝ × ℝ), (twoPointMeasure (↑(pairToParams p)).1 (↑(pairToParams p)).2) B ∂latentPairMeasure μ M

Pull the nondegenerate kernel mixture back from the parameter subtype to the original weighted pair measure. This is the change-of-variables layer in the Borel-set verification of the two-point mixture formula.

theorem Feige.nondegenerateKernelMixture_apply_strict (μ : MeasureTheory.Measure ℝ) [MeasureTheory.SFinite μ] (M : ℝ) {B : Set ℝ} (hB : MeasurableSet B) : (nondegenerateKernelMixture μ M) B = ∫⁻ (p : ℝ × ℝ), (twoPointMeasure p.1 p.2) B ∂latentPairMeasure μ M

theorem Feige.nondegenerateKernelMixture_apply_expanded {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsFiniteMeasure μ] (hμ : MeasureTheory.Integrable (fun (x : ℝ) => x) μ) (M : ℝ) {B : Set ℝ} (hB : MeasurableSet B) : (nondegenerateKernelMixture μ M) B = (ENNReal.ofReal M)⁻¹ * (ENNReal.ofReal (aboveMoment μ) * (μ.restrict (Set.Iio 1)) B + ENNReal.ofReal (belowMoment μ) * (μ.restrict (Set.Ioi 1)) B)

theorem Feige.fullKernelMixture_eq_expanded {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsFiniteMeasure μ] (hμ : MeasureTheory.Integrable (fun (x : ℝ) => x) μ) (M : ℝ) : fullKernelMixture μ M = expandedTwoPointMixture μ M

The measurable-kernel construction agrees with the direct expansion of the two-point mixture formula.

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

For a mean-one probability law with a nonzero lower moment, sampling the latent pair and then the corresponding two-point law reconstructs the original law.