Probability-law formulation of the transfer Stein identities

theorem Feige.TransferStein.instIsProbabilityMeasureRealExpMeasureOfNat_leanPool : MeasureTheory.IsProbabilityMeasure (ProbabilityTheory.expMeasure 1)

noncomputable def Feige.TransferStein.zPlusLaw (μ : MeasureTheory.Measure ℝ) (a : ℝ) : MeasureTheory.Measure ℝ

Law of Z₊ = Y + aE, where E is an independent rate-one exponential.

Equations

• Feige.TransferStein.zPlusLaw μ a = MeasureTheory.Measure.map (fun (p : ℝ × ℝ) => p.1 + a * p.2) (μ.prod (ProbabilityTheory.expMeasure 1))

noncomputable def Feige.TransferStein.zMinusLaw (μ : MeasureTheory.Measure ℝ) (b : ℝ) : MeasureTheory.Measure ℝ

Law of Z₋ = Y - bE, where E is an independent rate-one exponential.

Equations

• Feige.TransferStein.zMinusLaw μ b = MeasureTheory.Measure.map (fun (p : ℝ × ℝ) => p.1 - b * p.2) (μ.prod (ProbabilityTheory.expMeasure 1))

theorem Feige.TransferStein.measurable_zPlusMap (a : ℝ) : Measurable fun (p : ℝ × ℝ) => p.1 + a * p.2

theorem Feige.TransferStein.measurable_zMinusMap (b : ℝ) : Measurable fun (p : ℝ × ℝ) => p.1 - b * p.2

instance Feige.TransferStein.zPlusLaw_isFinite (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure μ] (a : ℝ) : MeasureTheory.IsFiniteMeasure (zPlusLaw μ a)

instance Feige.TransferStein.zMinusLaw_isFinite (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure μ] (b : ℝ) : MeasureTheory.IsFiniteMeasure (zMinusLaw μ b)

theorem Feige.TransferStein.integral_zPlusLaw (μ : MeasureTheory.Measure ℝ) (a : ℝ) (f : ℝ → ℝ) (hf : MeasureTheory.AEStronglyMeasurable f (zPlusLaw μ a)) : ∫ (z : ℝ), f z ∂zPlusLaw μ a = ∫ (p : ℝ × ℝ), f (p.1 + a * p.2) ∂μ.prod (ProbabilityTheory.expMeasure 1)

Expectations under the pushforward law reduce to product-space expectations.

theorem Feige.TransferStein.integral_zMinusLaw (μ : MeasureTheory.Measure ℝ) (b : ℝ) (f : ℝ → ℝ) (hf : MeasureTheory.AEStronglyMeasurable f (zMinusLaw μ b)) : ∫ (z : ℝ), f z ∂zMinusLaw μ b = ∫ (p : ℝ × ℝ), f (p.1 - b * p.2) ∂μ.prod (ProbabilityTheory.expMeasure 1)

theorem Feige.TransferStein.zPlusLaw_singleton (μ : MeasureTheory.Measure ℝ) {a x : ℝ} (ha : a ≠ 0) : (zPlusLaw μ a) {x} = 0

Adding a nondegenerate exponential variable removes every atom.

theorem Feige.TransferStein.zMinusLaw_singleton (μ : MeasureTheory.Measure ℝ) {b x : ℝ} (hb : b ≠ 0) : (zMinusLaw μ b) {x} = 0

Subtracting a nondegenerate exponential variable likewise removes every atom.

theorem Feige.TransferStein.measurable_uTailIntegrand (d : ℝ) : Measurable (uTailIntegrand d)

theorem Feige.TransferStein.measurable_vTailIntegrand (c : ℝ) : Measurable (vTailIntegrand c)

theorem Feige.TransferStein.uTailIntegrand_nonneg (d z : ℝ) : 0 ≤ uTailIntegrand d z

theorem Feige.TransferStein.vTailIntegrand_nonneg (c z : ℝ) : 0 ≤ vTailIntegrand c z

theorem Feige.TransferStein.uTailIntegrand_le_one {d : ℝ} (hd : 0 < d) (z : ℝ) : uTailIntegrand d z ≤ 1

theorem Feige.TransferStein.vTailIntegrand_le_one {c : ℝ} (hc : 0 < c) (z : ℝ) : vTailIntegrand c z ≤ 1

theorem Feige.TransferStein.integrable_uTailIntegrand (ν : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure ν] {d : ℝ} (hd : 0 < d) : MeasureTheory.Integrable (uTailIntegrand d) ν

theorem Feige.TransferStein.integrable_vTailIntegrand (ν : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure ν] {c : ℝ} (hc : 0 < c) : MeasureTheory.Integrable (vTailIntegrand c) ν

noncomputable def Feige.TransferStein.uProbability (ν : MeasureTheory.Measure ℝ) (d : ℝ) : ℝ

The probability P(0 ≤ Z < dE'), represented on the canonical independent product space.

Equations

• Feige.TransferStein.uProbability ν d = ((ν.prod (ProbabilityTheory.expMeasure 1)) {p : ℝ × ℝ | 0 ≤ p.1 ∧ p.1 < d * p.2}).toReal

noncomputable def Feige.TransferStein.vProbability (ν : MeasureTheory.Measure ℝ) (c : ℝ) : ℝ

The probability P(-cE' ≤ Z < 0).

Equations

• Feige.TransferStein.vProbability ν c = ((ν.prod (ProbabilityTheory.expMeasure 1)) {p : ℝ × ℝ | p.1 < 0 ∧ -c * p.2 ≤ p.1}).toReal

theorem Feige.TransferStein.uProbability_eq_integral (ν : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure ν] {d : ℝ} (hd : 0 < d) : uProbability ν d = ∫ (z : ℝ), uTailIntegrand d z ∂ν

theorem Feige.TransferStein.vProbability_eq_integral (ν : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure ν] {c : ℝ} (hc : 0 < c) : vProbability ν c = ∫ (z : ℝ), vTailIntegrand c z ∂ν

theorem Feige.TransferStein.integral_expMeasure_one (f : ℝ → ℝ) : ∫ (e : ℝ), f e ∂ProbabilityTheory.expMeasure 1 = ∫ (e : ℝ) in Set.Ioi 0, f e * Real.exp (-e)

Rate-one exponential integration is integration against exp (-e) on the positive half-line.

theorem Feige.TransferStein.integral_zPlusLaw_eq_nested (μ : MeasureTheory.Measure ℝ) [MeasureTheory.SFinite μ] (a : ℝ) (f : ℝ → ℝ) (hf : MeasureTheory.AEStronglyMeasurable f (zPlusLaw μ a)) (hprod : MeasureTheory.Integrable (fun (p : ℝ × ℝ) => f (p.1 + a * p.2)) (μ.prod (ProbabilityTheory.expMeasure 1))) : ∫ (z : ℝ), f z ∂zPlusLaw μ a = ∫ (y : ℝ), ∫ (e : ℝ) in Set.Ioi 0, f (y + a * e) * Real.exp (-e) ∂μ

theorem Feige.TransferStein.integral_zMinusLaw_eq_nested (μ : MeasureTheory.Measure ℝ) [MeasureTheory.SFinite μ] (b : ℝ) (f : ℝ → ℝ) (hf : MeasureTheory.AEStronglyMeasurable f (zMinusLaw μ b)) (hprod : MeasureTheory.Integrable (fun (p : ℝ × ℝ) => f (p.1 - b * p.2)) (μ.prod (ProbabilityTheory.expMeasure 1))) : ∫ (z : ℝ), f z ∂zMinusLaw μ b = ∫ (y : ℝ), ∫ (e : ℝ) in Set.Ioi 0, f (y - b * e) * Real.exp (-e) ∂μ

theorem Feige.TransferStein.integrable_transferPhi_zPlus (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure μ] {d : ℝ} (hd : 0 < d) (a : ℝ) : MeasureTheory.Integrable (fun (p : ℝ × ℝ) => TransferTestFunctions.transferPhi d (p.1 + a * p.2)) (μ.prod (ProbabilityTheory.expMeasure 1))

theorem Feige.TransferStein.integrable_transferPhi_zMinus (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure μ] {d : ℝ} (hd : 0 < d) (b : ℝ) : MeasureTheory.Integrable (fun (p : ℝ × ℝ) => TransferTestFunctions.transferPhi d (p.1 - b * p.2)) (μ.prod (ProbabilityTheory.expMeasure 1))

theorem Feige.TransferStein.integrable_transferPsi_zPlus (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure μ] (c a : ℝ) : MeasureTheory.Integrable (fun (p : ℝ × ℝ) => TransferTestFunctions.transferPsi c (p.1 + a * p.2)) (μ.prod (ProbabilityTheory.expMeasure 1))

theorem Feige.TransferStein.integrable_transferPsi_zMinus (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure μ] (c b : ℝ) : MeasureTheory.Integrable (fun (p : ℝ × ℝ) => TransferTestFunctions.transferPsi c (p.1 - b * p.2)) (μ.prod (ProbabilityTheory.expMeasure 1))

theorem Feige.TransferStein.APlus_eq_law (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure μ] {d : ℝ} (hd : 0 < d) (a : ℝ) : APlus μ d a = ∫ (z : ℝ), TransferTestFunctions.transferPhi d z ∂zPlusLaw μ a

theorem Feige.TransferStein.AMinus_eq_law (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure μ] {d : ℝ} (hd : 0 < d) (b : ℝ) : AMinus μ d b = ∫ (z : ℝ), TransferTestFunctions.transferPhi d z ∂zMinusLaw μ b

theorem Feige.TransferStein.BPlus_eq_law (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure μ] (c a : ℝ) : BPlus μ c a = ∫ (z : ℝ), TransferTestFunctions.transferPsi c z ∂zPlusLaw μ a

theorem Feige.TransferStein.BMinus_eq_law (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure μ] (c b : ℝ) : BMinus μ c b = ∫ (z : ℝ), TransferTestFunctions.transferPsi c z ∂zMinusLaw μ b

theorem Feige.TransferStein.uProbability_eq_derivative (ν : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure ν] {d : ℝ} (hd : 0 < d) (hzero : ν {0} = 0) : uProbability ν d = d * ∫ (z : ℝ), TransferTestFunctions.transferPhiDeriv d z ∂ν

On any atomless finite law, the lower-tail transfer probability u is exactly d E[φ'(Z)].

theorem Feige.TransferStein.vProbability_eq_derivative (ν : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure ν] {c : ℝ} (hc : 0 < c) : vProbability ν c = c * ∫ (z : ℝ), TransferTestFunctions.transferPsiDeriv c z ∂ν

The corresponding identity v = c E[ψ'(Z)].

theorem Feige.TransferStein.uProbability_zPlus_eq_derivative (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure μ] {a d : ℝ} (ha : 0 < a) (hd : 0 < d) : uProbability (zPlusLaw μ a) d = d * ∫ (z : ℝ), TransferTestFunctions.transferPhiDeriv d z ∂zPlusLaw μ a

theorem Feige.TransferStein.uProbability_zMinus_eq_derivative (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure μ] {b d : ℝ} (hb : 0 < b) (hd : 0 < d) : uProbability (zMinusLaw μ b) d = d * ∫ (z : ℝ), TransferTestFunctions.transferPhiDeriv d z ∂zMinusLaw μ b

theorem Feige.TransferStein.vProbability_zPlus_eq_derivative (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure μ] {a c : ℝ} (hc : 0 < c) : vProbability (zPlusLaw μ a) c = c * ∫ (z : ℝ), TransferTestFunctions.transferPsiDeriv c z ∂zPlusLaw μ a

theorem Feige.TransferStein.vProbability_zMinus_eq_derivative (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure μ] {b c : ℝ} (hc : 0 < c) : vProbability (zMinusLaw μ b) c = c * ∫ (z : ℝ), TransferTestFunctions.transferPsiDeriv c z ∂zMinusLaw μ b

theorem Feige.TransferStein.uPlus_eq_probability (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure μ] {a d : ℝ} (ha : 0 < a) (hd : 0 < d) (hprod : MeasureTheory.Integrable (fun (p : ℝ × ℝ) => TransferTestFunctions.transferPhiDeriv d (p.1 + a * p.2)) (μ.prod (ProbabilityTheory.expMeasure 1))) : uPlus μ d a = uProbability (zPlusLaw μ a) d

theorem Feige.TransferStein.uMinus_eq_probability (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure μ] {b d : ℝ} (hb : 0 < b) (hd : 0 < d) (hprod : MeasureTheory.Integrable (fun (p : ℝ × ℝ) => TransferTestFunctions.transferPhiDeriv d (p.1 - b * p.2)) (μ.prod (ProbabilityTheory.expMeasure 1))) : uMinus μ d b = uProbability (zMinusLaw μ b) d

theorem Feige.TransferStein.vPlus_eq_probability (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure μ] {a c : ℝ} (ha : 0 < a) (hc : 0 < c) (hprod : MeasureTheory.Integrable (fun (p : ℝ × ℝ) => TransferTestFunctions.transferPsiDeriv c (p.1 + a * p.2)) (μ.prod (ProbabilityTheory.expMeasure 1))) : vPlus μ c a = vProbability (zPlusLaw μ a) c

theorem Feige.TransferStein.vMinus_eq_probability (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure μ] {b c : ℝ} (hb : 0 < b) (hc : 0 < c) (hprod : MeasureTheory.Integrable (fun (p : ℝ × ℝ) => TransferTestFunctions.transferPsiDeriv c (p.1 - b * p.2)) (μ.prod (ProbabilityTheory.expMeasure 1))) : vMinus μ c b = vProbability (zMinusLaw μ b) c

theorem Feige.TransferStein.equation23_A_probability (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure μ] {d a b : ℝ} (hd : 0 < d) (ha : 0 < a) (hb : 0 < b) (hPlus : MeasureTheory.Integrable (phiPlus d a) μ) (hMinus : MeasureTheory.Integrable (phiMinus d b) μ) (hDerivPlus : MeasureTheory.Integrable (phiDerivPlus d a) μ) (hDerivMinus : MeasureTheory.Integrable (phiDerivMinus d b) μ) (hLawDerivPlus : MeasureTheory.Integrable (fun (p : ℝ × ℝ) => TransferTestFunctions.transferPhiDeriv d (p.1 + a * p.2)) (μ.prod (ProbabilityTheory.expMeasure 1))) (hLawDerivMinus : MeasureTheory.Integrable (fun (p : ℝ × ℝ) => TransferTestFunctions.transferPhiDeriv d (p.1 - b * p.2)) (μ.prod (ProbabilityTheory.expMeasure 1))) : d * (∫ (z : ℝ), TransferTestFunctions.transferPhi d z ∂zPlusLaw μ a - ∫ (z : ℝ), TransferTestFunctions.transferPhi d z ∂zMinusLaw μ b) = a * uProbability (zPlusLaw μ a) d + b * uProbability (zMinusLaw μ b) d

The lower-test identity with A± expressed as expectations under the actual laws of Z± and u± as event probabilities.

theorem Feige.TransferStein.equation23_B_probability (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure μ] {c a b : ℝ} (hc : 0 < c) (ha : 0 < a) (hb : 0 < b) (hPlus : MeasureTheory.Integrable (psiPlus c a) μ) (hMinus : MeasureTheory.Integrable (psiMinus c b) μ) (hDerivPlus : MeasureTheory.Integrable (psiDerivPlus c a) μ) (hDerivMinus : MeasureTheory.Integrable (psiDerivMinus c b) μ) (hLawDerivPlus : MeasureTheory.Integrable (fun (p : ℝ × ℝ) => TransferTestFunctions.transferPsiDeriv c (p.1 + a * p.2)) (μ.prod (ProbabilityTheory.expMeasure 1))) (hLawDerivMinus : MeasureTheory.Integrable (fun (p : ℝ × ℝ) => TransferTestFunctions.transferPsiDeriv c (p.1 - b * p.2)) (μ.prod (ProbabilityTheory.expMeasure 1))) : c * (∫ (z : ℝ), TransferTestFunctions.transferPsi c z ∂zPlusLaw μ a - ∫ (z : ℝ), TransferTestFunctions.transferPsi c z ∂zMinusLaw μ b) = a * vProbability (zPlusLaw μ a) c + b * vProbability (zMinusLaw μ b) c

The corresponding upper-test probability identity.