Fully automatic local exponential transfer interface

This file discharges the bounded-integrability hypotheses in the transfer Stein identities and assembles the probability relations and density identifications.

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

theorem Feige.Lemma43Complete.integrable_affine_prod_of_bound (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure μ] {g : ℝ → ℝ} (hg : Measurable g) (C : ℝ) (hC : ∀ (x : ℝ), ‖g x‖ ≤ C) (r : ℝ) : MeasureTheory.Integrable (fun (p : ℝ × ℝ) => g (p.1 + r * p.2)) (μ.prod (ProbabilityTheory.expMeasure 1))

theorem Feige.Lemma43Complete.integrable_phiPlus (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure μ] {d : ℝ} (hd : 0 < d) (a : ℝ) : MeasureTheory.Integrable (TransferStein.phiPlus d a) μ

theorem Feige.Lemma43Complete.integrable_phiMinus (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure μ] {d : ℝ} (hd : 0 < d) (b : ℝ) : MeasureTheory.Integrable (TransferStein.phiMinus d b) μ

theorem Feige.Lemma43Complete.integrable_psiPlus (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure μ] (c a : ℝ) : MeasureTheory.Integrable (TransferStein.psiPlus c a) μ

theorem Feige.Lemma43Complete.integrable_psiMinus (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure μ] (c b : ℝ) : MeasureTheory.Integrable (TransferStein.psiMinus c b) μ

theorem Feige.Lemma43Complete.integrable_phiDerivPlus (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure μ] {d : ℝ} (hd : 0 < d) (a : ℝ) : MeasureTheory.Integrable (TransferStein.phiDerivPlus d a) μ

theorem Feige.Lemma43Complete.integrable_phiDerivMinus (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure μ] {d : ℝ} (hd : 0 < d) (b : ℝ) : MeasureTheory.Integrable (TransferStein.phiDerivMinus d b) μ

theorem Feige.Lemma43Complete.integrable_psiDerivPlus (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure μ] {c : ℝ} (hc : 0 < c) (a : ℝ) : MeasureTheory.Integrable (TransferStein.psiDerivPlus c a) μ

theorem Feige.Lemma43Complete.integrable_psiDerivMinus (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure μ] {c : ℝ} (hc : 0 < c) (b : ℝ) : MeasureTheory.Integrable (TransferStein.psiDerivMinus c b) μ

theorem Feige.Lemma43Complete.equation23_A_probability_auto (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure μ] {a b d : ℝ} (ha : 0 < a) (hb : 0 < b) (hd : 0 < d) : d * (∫ (z : ℝ), TransferTestFunctions.transferPhi d z ∂TransferStein.zPlusLaw μ a - ∫ (z : ℝ), TransferTestFunctions.transferPhi d z ∂TransferStein.zMinusLaw μ b) = a * TransferStein.uProbability (TransferStein.zPlusLaw μ a) d + b * TransferStein.uProbability (TransferStein.zMinusLaw μ b) d

The lower-test transfer identity, with all bounded-integrability hypotheses discharged.

theorem Feige.Lemma43Complete.equation23_B_probability_auto (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure μ] {a b c : ℝ} (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : c * (∫ (z : ℝ), TransferTestFunctions.transferPsi c z ∂TransferStein.zPlusLaw μ a - ∫ (z : ℝ), TransferTestFunctions.transferPsi c z ∂TransferStein.zMinusLaw μ b) = a * TransferStein.vProbability (TransferStein.zPlusLaw μ a) c + b * TransferStein.vProbability (TransferStein.zMinusLaw μ b) c

The upper-test transfer identity, again with no integrability inputs.

theorem Feige.Lemma43Complete.complete_for_density {f : ℝ → ENNReal} (hf : Measurable f) (hflc : LikelihoodRatio.FourPointLogConcave f) [MeasureTheory.IsProbabilityMeasure (MeasureTheory.volume.withDensity f)] {a b c d : ℝ} (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) (hd : 0 < d) : have νP := TransferStein.zPlusLaw (MeasureTheory.volume.withDensity f) a; have νM := TransferStein.zMinusLaw (MeasureTheory.volume.withDensity f) 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) ∧ Lemma43.theta νM c d ≤ Lemma43.theta νP c d ∧ 0 < Lemma43.w νP c d ∧ 0 < Lemma43.w νM c d

The local transfer result for the actual positive and negative exponential shifts of an arbitrary probability density. Probability relations, Stein integrability, density identification, denominator positivity, and the likelihood-ratio order are all discharged internally.