Local transfer identity for an arbitrary base law #
theorem
Feige.Lemma43ArbitraryBase.identity_and_w_pos
(μ : MeasureTheory.Measure ℝ)
[MeasureTheory.IsProbabilityMeasure μ]
{a b c d : ℝ}
(ha : 0 < a)
(hb : 0 < b)
(hc : 0 < c)
(hd : 0 < d)
:
have νP := TransferStein.zPlusLaw μ a;
have νM := TransferStein.zMinusLaw μ b;
(1 - Lemma43.theta νM c d) * (Lemma43.A νP d - Lemma43.A νM d) - c / (c + d) * (Lemma43.F νP - Lemma43.F νM) = (a - c) / (c + d) * Lemma43.w νP c d * (Lemma43.theta νP c d - Lemma43.theta νM c d) ∧ 0 < Lemma43.w νP c d ∧ 0 < Lemma43.w νM c d
The factorized transfer identity and denominator positivity require no density or TP2 assumption: they hold for the two exponential shifts of every probability base law.
theorem
Feige.Lemma43ArbitraryBase.terminal_zMinus
(μ : MeasureTheory.Measure ℝ)
[MeasureTheory.IsProbabilityMeasure μ]
(hpos : μ (Set.Ioi 0) = 0)
{b c d : ℝ}
(hb : 0 < b)
:
have νM := TransferStein.zMinusLaw μ b;
Lemma43.F νM = 0 ∧ Lemma43.theta νM c d = 0
At a terminal base law supported on the nonpositive half-line, the negative endpoint has zero nonnegative tail and hence zero transfer parameter.