Endpoint tail identities for the local transfer step

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

theorem Feige.Lemma43Endpoints.expMeasure_one_Iic (t : ℝ) : (ProbabilityTheory.expMeasure 1) (Set.Iic t) = ENNReal.ofReal (if 0 ≤ t then 1 - Real.exp (-t) else 0)

theorem Feige.Lemma43Endpoints.F_zMinusLaw_eq_A (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure μ] {b : ℝ} (hb : 0 < b) : Lemma43.F (TransferStein.zMinusLaw μ b) = Lemma43.A μ b

Subtracting bE and taking the nonnegative tail applies the φ_b endpoint transform to the original law.

theorem Feige.Lemma43Endpoints.expMeasure_one_Ici_all (t : ℝ) : (ProbabilityTheory.expMeasure 1) (Set.Ici t) = ENNReal.ofReal (if t < 0 then 1 else Real.exp (-t))

theorem Feige.Lemma43Endpoints.F_zPlusLaw_eq_B (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure μ] {a : ℝ} (ha : 0 < a) : Lemma43.F (TransferStein.zPlusLaw μ a) = Lemma43.B μ a

Adding aE and taking the nonnegative tail applies the ψ_a endpoint transform to the original law.