Measure-level transfer Stein identities

This file lifts the fixed-y identities to an arbitrary law for Y. The outer integrability assumptions are stated explicitly, making the result usable independently of how the law of Y is presented.

noncomputable def Feige.TransferStein.uTailIntegrand (d z : ℝ) : ℝ

Real-valued conditional lower-tail transfer integrand u.

Equations

• Feige.TransferStein.uTailIntegrand d z = if 0 ≤ z then Real.exp (-z / d) else 0

noncomputable def Feige.TransferStein.vTailIntegrand (c z : ℝ) : ℝ

Real-valued conditional upper-tail transfer integrand v.

Equations

• Feige.TransferStein.vTailIntegrand c z = if z < 0 then Real.exp (z / c) else 0

theorem Feige.TransferStein.d_mul_transferPhiDeriv {d z : ℝ} (hd : 0 < d) (hz : z ≠ 0) : d * TransferTestFunctions.transferPhiDeriv d z = uTailIntegrand d z

The formal derivative of φ, multiplied by d, is the conditional u integrand away from the sole boundary point zero.

theorem Feige.TransferStein.c_mul_transferPsiDeriv {c z : ℝ} (hc : 0 < c) : c * TransferTestFunctions.transferPsiDeriv c z = vTailIntegrand c z

The ψ derivative identity has no boundary discrepancy.

theorem Feige.TransferStein.d_mul_integral_transferPhiDeriv (ν : MeasureTheory.Measure ℝ) {d : ℝ} (hd : 0 < d) (hzero : ν {0} = 0) : d * ∫ (z : ℝ), TransferTestFunctions.transferPhiDeriv d z ∂ν = ∫ (z : ℝ), uTailIntegrand d z ∂ν

Integral bridge from the analytic φ' quantity to the conditional tail formula. Atomlessness at zero is precisely the boundary condition needed to pass between z ≥ 0 in the tail event and z > 0 in the a.e. derivative.

theorem Feige.TransferStein.c_mul_integral_transferPsiDeriv (ν : MeasureTheory.Measure ℝ) {c : ℝ} (hc : 0 < c) : c * ∫ (z : ℝ), TransferTestFunctions.transferPsiDeriv c z ∂ν = ∫ (z : ℝ), vTailIntegrand c z ∂ν

Integral bridge from the analytic ψ' quantity to the conditional left-tail formula.

noncomputable def Feige.TransferStein.phiPlus (d a y : ℝ) : ℝ

The positive φ expectation conditional on Y = y.

Equations

• Feige.TransferStein.phiPlus d a y = ∫ (e : ℝ) in Set.Ioi 0, Feige.TransferTestFunctions.transferPhi d (y + a * e) * Real.exp (-e)

noncomputable def Feige.TransferStein.phiMinus (d b y : ℝ) : ℝ

The negative φ expectation conditional on Y = y.

Equations

• Feige.TransferStein.phiMinus d b y = ∫ (e : ℝ) in Set.Ioi 0, Feige.TransferTestFunctions.transferPhi d (y - b * e) * Real.exp (-e)

noncomputable def Feige.TransferStein.phiDerivPlus (d a y : ℝ) : ℝ

The positive derivative expectation conditional on Y = y.

Equations

• Feige.TransferStein.phiDerivPlus d a y = ∫ (e : ℝ) in Set.Ioi 0, a * Feige.TransferTestFunctions.transferPhiDeriv d (y + a * e) * Real.exp (-e)

noncomputable def Feige.TransferStein.phiDerivMinus (d b y : ℝ) : ℝ

The negative derivative expectation conditional on Y = y.

Equations

• Feige.TransferStein.phiDerivMinus d b y = ∫ (e : ℝ) in Set.Ioi 0, b * Feige.TransferTestFunctions.transferPhiDeriv d (y - b * e) * Real.exp (-e)

theorem Feige.TransferStein.integral_phi_two_sided (μ : MeasureTheory.Measure ℝ) {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) μ) : ∫ (y : ℝ), phiPlus d a y ∂μ - ∫ (y : ℝ), phiMinus d b y ∂μ = ∫ (y : ℝ), phiDerivPlus d a y ∂μ + ∫ (y : ℝ), phiDerivMinus d b y ∂μ

The two-sided exponential Stein identity for φ, averaged over an arbitrary measure μ.

The four hypotheses are exactly those needed to distribute the outer Bochner integral over subtraction and addition.

theorem Feige.TransferStein.integral_phi_two_sided_prod (μ : MeasureTheory.Measure ℝ) [MeasureTheory.SFinite μ] {d a b : ℝ} (hd : 0 < d) (ha : 0 < a) (hb : 0 < b) (hPlus : MeasureTheory.Integrable (fun (p : ℝ × ℝ) => TransferTestFunctions.transferPhi d (p.1 + a * p.2) * Real.exp (-p.2)) (μ.prod (MeasureTheory.volume.restrict (Set.Ioi 0)))) (hMinus : MeasureTheory.Integrable (fun (p : ℝ × ℝ) => TransferTestFunctions.transferPhi d (p.1 - b * p.2) * Real.exp (-p.2)) (μ.prod (MeasureTheory.volume.restrict (Set.Ioi 0)))) (hDerivPlus : MeasureTheory.Integrable (fun (p : ℝ × ℝ) => a * TransferTestFunctions.transferPhiDeriv d (p.1 + a * p.2) * Real.exp (-p.2)) (μ.prod (MeasureTheory.volume.restrict (Set.Ioi 0)))) (hDerivMinus : MeasureTheory.Integrable (fun (p : ℝ × ℝ) => b * TransferTestFunctions.transferPhiDeriv d (p.1 - b * p.2) * Real.exp (-p.2)) (μ.prod (MeasureTheory.volume.restrict (Set.Ioi 0)))) : ∫ (p : ℝ × ℝ), TransferTestFunctions.transferPhi d (p.1 + a * p.2) * Real.exp (-p.2) ∂μ.prod (MeasureTheory.volume.restrict (Set.Ioi 0)) - ∫ (p : ℝ × ℝ), TransferTestFunctions.transferPhi d (p.1 - b * p.2) * Real.exp (-p.2) ∂μ.prod (MeasureTheory.volume.restrict (Set.Ioi 0)) = ∫ (p : ℝ × ℝ), a * TransferTestFunctions.transferPhiDeriv d (p.1 + a * p.2) * Real.exp (-p.2) ∂μ.prod (MeasureTheory.volume.restrict (Set.Ioi 0)) + ∫ (p : ℝ × ℝ), b * TransferTestFunctions.transferPhiDeriv d (p.1 - b * p.2) * Real.exp (-p.2) ∂μ.prod (MeasureTheory.volume.restrict (Set.Ioi 0))

Product-measure/Fubini form of the averaged φ identity.

noncomputable def Feige.TransferStein.psiPlus (c a y : ℝ) : ℝ

The positive ψ expectation conditional on Y = y.

Equations

• Feige.TransferStein.psiPlus c a y = ∫ (e : ℝ) in Set.Ioi 0, Feige.TransferTestFunctions.transferPsi c (y + a * e) * Real.exp (-e)

noncomputable def Feige.TransferStein.psiMinus (c b y : ℝ) : ℝ

The negative ψ expectation conditional on Y = y.

Equations

• Feige.TransferStein.psiMinus c b y = ∫ (e : ℝ) in Set.Ioi 0, Feige.TransferTestFunctions.transferPsi c (y - b * e) * Real.exp (-e)

noncomputable def Feige.TransferStein.psiDerivPlus (c a y : ℝ) : ℝ

The positive derivative expectation conditional on Y = y.

Equations

• Feige.TransferStein.psiDerivPlus c a y = ∫ (e : ℝ) in Set.Ioi 0, a * Feige.TransferTestFunctions.transferPsiDeriv c (y + a * e) * Real.exp (-e)

noncomputable def Feige.TransferStein.psiDerivMinus (c b y : ℝ) : ℝ

The negative derivative expectation conditional on Y = y.

Equations

• Feige.TransferStein.psiDerivMinus c b y = ∫ (e : ℝ) in Set.Ioi 0, b * Feige.TransferTestFunctions.transferPsiDeriv c (y - b * e) * Real.exp (-e)

theorem Feige.TransferStein.integral_psi_two_sided (μ : MeasureTheory.Measure ℝ) {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) μ) : ∫ (y : ℝ), psiPlus c a y ∂μ - ∫ (y : ℝ), psiMinus c b y ∂μ = ∫ (y : ℝ), psiDerivPlus c a y ∂μ + ∫ (y : ℝ), psiDerivMinus c b y ∂μ

The two-sided exponential Stein identity for ψ, averaged over an arbitrary measure μ.

theorem Feige.TransferStein.integral_psi_two_sided_prod (μ : MeasureTheory.Measure ℝ) [MeasureTheory.SFinite μ] {c a b : ℝ} (hc : 0 < c) (ha : 0 < a) (hb : 0 < b) (hPlus : MeasureTheory.Integrable (fun (p : ℝ × ℝ) => TransferTestFunctions.transferPsi c (p.1 + a * p.2) * Real.exp (-p.2)) (μ.prod (MeasureTheory.volume.restrict (Set.Ioi 0)))) (hMinus : MeasureTheory.Integrable (fun (p : ℝ × ℝ) => TransferTestFunctions.transferPsi c (p.1 - b * p.2) * Real.exp (-p.2)) (μ.prod (MeasureTheory.volume.restrict (Set.Ioi 0)))) (hDerivPlus : MeasureTheory.Integrable (fun (p : ℝ × ℝ) => a * TransferTestFunctions.transferPsiDeriv c (p.1 + a * p.2) * Real.exp (-p.2)) (μ.prod (MeasureTheory.volume.restrict (Set.Ioi 0)))) (hDerivMinus : MeasureTheory.Integrable (fun (p : ℝ × ℝ) => b * TransferTestFunctions.transferPsiDeriv c (p.1 - b * p.2) * Real.exp (-p.2)) (μ.prod (MeasureTheory.volume.restrict (Set.Ioi 0)))) : ∫ (p : ℝ × ℝ), TransferTestFunctions.transferPsi c (p.1 + a * p.2) * Real.exp (-p.2) ∂μ.prod (MeasureTheory.volume.restrict (Set.Ioi 0)) - ∫ (p : ℝ × ℝ), TransferTestFunctions.transferPsi c (p.1 - b * p.2) * Real.exp (-p.2) ∂μ.prod (MeasureTheory.volume.restrict (Set.Ioi 0)) = ∫ (p : ℝ × ℝ), a * TransferTestFunctions.transferPsiDeriv c (p.1 + a * p.2) * Real.exp (-p.2) ∂μ.prod (MeasureTheory.volume.restrict (Set.Ioi 0)) + ∫ (p : ℝ × ℝ), b * TransferTestFunctions.transferPsiDeriv c (p.1 - b * p.2) * Real.exp (-p.2) ∂μ.prod (MeasureTheory.volume.restrict (Set.Ioi 0))

Product-measure/Fubini form of the averaged ψ identity.

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

Analytic A₊ = E φ(Z₊).

Equations

• Feige.TransferStein.APlus μ d a = ∫ (y : ℝ), Feige.TransferStein.phiPlus d a y ∂μ

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

Analytic A₋ = E φ(Z₋).

Equations

• Feige.TransferStein.AMinus μ d b = ∫ (y : ℝ), Feige.TransferStein.phiMinus d b y ∂μ

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

Analytic B₊ = E ψ(Z₊).

Equations

• Feige.TransferStein.BPlus μ c a = ∫ (y : ℝ), Feige.TransferStein.psiPlus c a y ∂μ

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

Analytic B₋ = E ψ(Z₋).

Equations

• Feige.TransferStein.BMinus μ c b = ∫ (y : ℝ), Feige.TransferStein.psiMinus c b y ∂μ

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

u₊, normalized as d times the φ' expectation. Since phiDerivPlus includes the affine chain-rule factor a, it is divided out here.

Equations

• Feige.TransferStein.uPlus μ d a = d / a * ∫ (y : ℝ), Feige.TransferStein.phiDerivPlus d a y ∂μ

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

Analytic u₋.

Equations

• Feige.TransferStein.uMinus μ d b = d / b * ∫ (y : ℝ), Feige.TransferStein.phiDerivMinus d b y ∂μ

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

v₊, normalized as c times the ψ' expectation.

Equations

• Feige.TransferStein.vPlus μ c a = c / a * ∫ (y : ℝ), Feige.TransferStein.psiDerivPlus c a y ∂μ

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

Analytic v₋.

Equations

• Feige.TransferStein.vMinus μ c b = c / b * ∫ (y : ℝ), Feige.TransferStein.psiDerivMinus c b y ∂μ

theorem Feige.TransferStein.equation23_A (μ : MeasureTheory.Measure ℝ) {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) μ) : d * (APlus μ d a - AMinus μ d b) = a * uPlus μ d a + b * uMinus μ d b

The lower-test Stein identity for the analytic quantities above.

theorem Feige.TransferStein.equation23_B (μ : MeasureTheory.Measure ℝ) {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) μ) : c * (BPlus μ c a - BMinus μ c b) = a * vPlus μ c a + b * vMinus μ c b

The upper-test Stein identity for the analytic quantities above.