Automatic elementary relations for the local transfer step

The relations B = A + u + v and F = B - v are pointwise identities between the two transfer test functions and their upper/lower exponential tails. Consequently the ProbabilityRelations input of Lemma43.complete holds for every finite law and need not remain an external hypothesis.

theorem Feige.Lemma43.transferPsi_eq_transferPhi_add_tails {c d : ℝ} (hc : 0 < c) (hd : 0 < d) (z : ℝ) : TransferTestFunctions.transferPsi c z = TransferTestFunctions.transferPhi d z + TransferStein.uTailIntegrand d z + TransferStein.vTailIntegrand c z

theorem Feige.Lemma43.indicator_Ici_eq_transferPsi_sub_vTail {c : ℝ} (hc : 0 < c) (z : ℝ) : (Set.Ici 0).indicator (fun (x : ℝ) => 1) z = TransferTestFunctions.transferPsi c z - TransferStein.vTailIntegrand c z

theorem Feige.Lemma43.integrable_transferPhi (ν : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure ν] {d : ℝ} (hd : 0 < d) : MeasureTheory.Integrable (TransferTestFunctions.transferPhi d) ν

theorem Feige.Lemma43.integrable_transferPsi (ν : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure ν] (c : ℝ) : MeasureTheory.Integrable (TransferTestFunctions.transferPsi c) ν

theorem Feige.Lemma43.B_eq_A_add_w (ν : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure ν] {c d : ℝ} (hc : 0 < c) (hd : 0 < d) : B ν c = A ν d + w ν c d

B = A + w for every finite law.

theorem Feige.Lemma43.F_eq_B_sub_v (ν : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure ν] {c : ℝ} (hc : 0 < c) : F ν = B ν c - v ν c

F = B - v for every finite law.

theorem Feige.Lemma43.probabilityRelations (νP νM : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure νP] [MeasureTheory.IsFiniteMeasure νM] {c d : ℝ} (hc : 0 < c) (hd : 0 < d) : ProbabilityRelations νP νM c d

The elementary relation bundle required by Lemma43.transfer_identity is automatic for any two finite laws.