Complete interface for the local exponential transfer step

This file packages the probability identity and the likelihood-ratio order comparison in forms intended for pointwise use along an insertion chain.

noncomputable def Feige.Lemma43.F (ν : MeasureTheory.Measure ℝ) : ℝ

The probability quantities attached to one law.

Equations

• Feige.Lemma43.F ν = (ν (Set.Ici 0)).toReal

noncomputable def Feige.Lemma43.A (ν : MeasureTheory.Measure ℝ) (d : ℝ) : ℝ

The upper transfer-test expectation for ν.

Equations

• Feige.Lemma43.A ν d = ∫ (z : ℝ), Feige.TransferTestFunctions.transferPhi d z ∂ν

noncomputable def Feige.Lemma43.B (ν : MeasureTheory.Measure ℝ) (c : ℝ) : ℝ

The lower transfer-test expectation for ν.

Equations

• Feige.Lemma43.B ν c = ∫ (z : ℝ), Feige.TransferTestFunctions.transferPsi c z ∂ν

noncomputable def Feige.Lemma43.u (ν : MeasureTheory.Measure ℝ) (d : ℝ) : ℝ

The upper crossing probability for ν.

Equations

• Feige.Lemma43.u ν d = Feige.TransferStein.uProbability ν d

noncomputable def Feige.Lemma43.v (ν : MeasureTheory.Measure ℝ) (c : ℝ) : ℝ

The lower crossing probability for ν.

Equations

• Feige.Lemma43.v ν c = Feige.TransferStein.vProbability ν c

noncomputable def Feige.Lemma43.w (ν : MeasureTheory.Measure ℝ) (c d : ℝ) : ℝ

The sum of the upper and lower crossing probabilities.

Equations

• Feige.Lemma43.w ν c d = Feige.Lemma43.u ν d + Feige.Lemma43.v ν c

noncomputable def Feige.Lemma43.theta (ν : MeasureTheory.Measure ℝ) (c d : ℝ) : ℝ

The upper crossing probability normalized by total crossing mass.

Equations

• Feige.Lemma43.theta ν c d = Feige.Lemma43.u ν d / Feige.Lemma43.w ν c d

theorem Feige.Lemma43.w_pos (ν : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure ν] {c d : ℝ} (hc : 0 < c) (hd : 0 < d) : 0 < w ν c d

def Feige.Lemma43.DensityIdentification (f : ℝ → ENNReal) (νP νM : MeasureTheory.Measure ℝ) (a b c d : ℝ) : Prop

Explicit, auditable identification between the actual tail probabilities of two laws and the four likelihood-ratio integrals.

Equations

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

def Feige.Lemma43.ProbabilityRelations (νP νM : MeasureTheory.Measure ℝ) (c d : ℝ) : Prop

The four elementary relations among A,B,F,u,v,w, kept as an explicit proposition so that no probability identification is hidden.

Equations

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

theorem Feige.Lemma43.transfer_identity (νP νM : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure νP] [MeasureTheory.IsProbabilityMeasure νM] {a b c d : ℝ} (hc : 0 < c) (hd : 0 < d) (hrel : ProbabilityRelations νP νM c d) (hA : d * (A νP d - A νM d) = a * u νP d + b * u νM d) (hB : c * (B νP c - B νM c) = a * v νP c + b * v νM c) : (1 - theta νM c d) * (A νP d - A νM d) - c / (c + d) * (F νP - F νM) = (a - c) / (c + d) * w νP c d * (theta νP c d - theta νM c d)

Identity half of the local transfer step, stated entirely in the actual probability quantities of the two laws.

theorem Feige.Lemma43.theta_plus_ge_theta_minus_of_fourPoint {f : ℝ → ENNReal} (hfmeas : Measurable f) (hflc : LikelihoodRatio.FourPointLogConcave f) {a b c d uP uM vP vM : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (huP0 : 0 ≤ uP) (huM0 : 0 ≤ uM) (hvM0 : 0 ≤ vM) (hwP : 0 < uP + vP) (hwM : 0 < uM + vM) (huP : ENNReal.ofReal uP = LikelihoodRatio.uIntegral (LikelihoodRatio.fPlus f a) d) (huM : ENNReal.ofReal uM = LikelihoodRatio.uIntegral (LikelihoodRatio.fMinus f b) d) (hvP : ENNReal.ofReal vP = LikelihoodRatio.vIntegral (LikelihoodRatio.fPlus f a) c) (hvM : ENNReal.ofReal vM = LikelihoodRatio.vIntegral (LikelihoodRatio.fMinus f b) c) : uM / (uM + vM) ≤ uP / (uP + vP)

Order half of the local transfer step after identifying the four actual tail probabilities with the corresponding convolution-density integrals. The identification hypotheses are the exact interface needed from a density-of-pushforward lemma.

theorem Feige.Lemma43.theta_order {f : ℝ → ENNReal} (hfmeas : Measurable f) (hflc : LikelihoodRatio.FourPointLogConcave f) (νP νM : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure νP] [MeasureTheory.IsProbabilityMeasure νM] {a b c d : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hc : 0 < c) (hd : 0 < d) (hid : DensityIdentification f νP νM a b c d) : theta νM c d ≤ theta νP c d

Order half in the named probability quantities.

theorem Feige.Lemma43.complete {f : ℝ → ENNReal} (hfmeas : Measurable f) (hflc : LikelihoodRatio.FourPointLogConcave f) (νP νM : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure νP] [MeasureTheory.IsProbabilityMeasure νM] {a b c d : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hc : 0 < c) (hd : 0 < d) (hrel : ProbabilityRelations νP νM c d) (hA : d * (A νP d - A νM d) = a * u νP d + b * u νM d) (hB : c * (B νP c - B νM c) = a * v νP c + b * v νM c) (hid : DensityIdentification f νP νM a b c d) : (1 - theta νM c d) * (A νP d - A νM d) - c / (c + d) * (F νP - F νM) = (a - c) / (c + d) * w νP c d * (theta νP c d - theta νM c d) ∧ theta νM c d ≤ theta νP c d ∧ 0 < w νP c d ∧ 0 < w νM c d

Full auditable local-transfer interface for one insertion-chain edge. The analytic/probability identities and the density identifications are separate named hypotheses, and the conclusion exposes the factorized transfer identity, the likelihood-ratio order, and positivity of both denominators.