Exponential tail formulas used by the transfer identity

This file supplies the reusable one-dimensional probability calculations behind the local exponential transfer step. They are stated for Mathlib's rate-one exponential measure. In particular, the strict and non-strict tails agree, since this measure has no atoms.

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

theorem Feige.ExponentialTransfer.expMeasure_one_singleton (x : ℝ) : (ProbabilityTheory.expMeasure 1) {x} = 0

The rate-one exponential distribution has no atoms.

theorem Feige.ExponentialTransfer.expMeasure_one_Ioi {x : ℝ} (hx : 0 ≤ x) : (ProbabilityTheory.expMeasure 1) (Set.Ioi x) = ENNReal.ofReal (Real.exp (-x))

The rate-one exponential upper tail, in strict form.

theorem Feige.ExponentialTransfer.expMeasure_one_Ici {x : ℝ} (hx : 0 ≤ x) : (ProbabilityTheory.expMeasure 1) (Set.Ici x) = ENNReal.ofReal (Real.exp (-x))

The rate-one exponential upper tail, in non-strict form.

theorem Feige.ExponentialTransfer.measure_lt_mul_exp {z d : ℝ} (hd : 0 < d) : (ProbabilityTheory.expMeasure 1) {e : ℝ | 0 ≤ z ∧ z < d * e} = ENNReal.ofReal (if 0 ≤ z then Real.exp (-z / d) else 0)

Conditional u-integrand calculation. If d > 0, the exponential probability of z < dE', subject to z ≥ 0, is exp (-z/d).

theorem Feige.ExponentialTransfer.measure_neg_mul_le {z c : ℝ} (hc : 0 < c) : (ProbabilityTheory.expMeasure 1) {e : ℝ | z < 0 ∧ -c * e ≤ z} = ENNReal.ofReal (if z < 0 then Real.exp (z / c) else 0)

Conditional v-integrand calculation. If c > 0, the exponential probability of z ≥ -cE', subject to z < 0, is exp (z/c).

theorem Feige.ExponentialTransfer.prod_measure_u (μ : MeasureTheory.Measure ℝ) (d : ℝ) (hd : 0 < d) : (μ.prod (ProbabilityTheory.expMeasure 1)) {p : ℝ × ℝ | 0 ≤ p.1 ∧ p.1 < d * p.2} = ∫⁻ (z : ℝ), ENNReal.ofReal (if 0 ≤ z then Real.exp (-z / d) else 0) ∂μ

Product-measure/Tonelli form of the lower-tail transfer probability. On the canonical product space, the first coordinate is Z with law μ and the second coordinate is an independent rate-one exponential variable.

theorem Feige.ExponentialTransfer.prod_measure_v (μ : MeasureTheory.Measure ℝ) (c : ℝ) (hc : 0 < c) : (μ.prod (ProbabilityTheory.expMeasure 1)) {p : ℝ × ℝ | p.1 < 0 ∧ -c * p.2 ≤ p.1} = ∫⁻ (z : ℝ), ENNReal.ofReal (if z < 0 then Real.exp (z / c) else 0) ∂μ

Product-measure/Tonelli form of the upper-tail transfer probability. This is the mass between the threshold -cE' and zero.

noncomputable def Feige.ExponentialTransfer.bandIntegrand (c d z : ℝ) : ENNReal

Conditional width of the random interval [-cE', dE'] at a fixed value z; this is the integrand for w = u + v.

Equations

• Feige.ExponentialTransfer.bandIntegrand c d z = ENNReal.ofReal (if 0 ≤ z then Real.exp (-z / d) else Real.exp (z / c))

theorem Feige.ExponentialTransfer.measurable_bandIntegrand (c d : ℝ) : Measurable (bandIntegrand c d)

theorem Feige.ExponentialTransfer.bandIntegrand_pos (c d z : ℝ) : 0 < bandIntegrand c d z

theorem Feige.ExponentialTransfer.lintegral_bandIntegrand_pos (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure μ] (c d : ℝ) : 0 < ∫⁻ (z : ℝ), bandIntegrand c d z ∂μ

The interval width w is strictly positive under every probability law for Z.