Density identification for the local transfer step

This file connects the pushforward laws zPlusLaw and zMinusLaw to the convolution densities LikelihoodRatio.fPlus and fMinus.

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

theorem Feige.Lemma43Density.lintegral_expMeasure_one_eq {g : ℝ → ENNReal} (hg : Measurable g) : ∫⁻ (s : ℝ), g s ∂ProbabilityTheory.expMeasure 1 = ∫⁻ (s : ℝ) in Set.Ici 0, g s * LikelihoodRatio.expWeight s

Rate-one exponential integration in the ENNReal form used by the likelihood-ratio convolution densities.

theorem Feige.Lemma43Density.lintegral_zPlusLaw_eq_fPlus {f h : ℝ → ENNReal} (hf : Measurable f) (hh : Measurable h) (a : ℝ) : ∫⁻ (z : ℝ), h z ∂TransferStein.zPlusLaw (MeasureTheory.volume.withDensity f) a = ∫⁻ (x : ℝ), LikelihoodRatio.fPlus f a x * h x

Nonnegative test functions under Z₊ = Y + aE can be integrated against the explicit convolution density fPlus.

theorem Feige.Lemma43Density.zPlusLaw_eq_withDensity_fPlus {f : ℝ → ENNReal} (hf : Measurable f) (a : ℝ) : TransferStein.zPlusLaw (MeasureTheory.volume.withDensity f) a = MeasureTheory.volume.withDensity (LikelihoodRatio.fPlus f a)

The pushforward law of a positive exponential shift has density LikelihoodRatio.fPlus.

theorem Feige.Lemma43Density.lintegral_zMinusLaw_eq_fMinus {f h : ℝ → ENNReal} (hf : Measurable f) (hh : Measurable h) (b : ℝ) : ∫⁻ (z : ℝ), h z ∂TransferStein.zMinusLaw (MeasureTheory.volume.withDensity f) b = ∫⁻ (x : ℝ), LikelihoodRatio.fMinus f b x * h x

Nonnegative test functions under Z₋ = Y - bE can be integrated against the explicit convolution density fMinus.

theorem Feige.Lemma43Density.zMinusLaw_eq_withDensity_fMinus {f : ℝ → ENNReal} (hf : Measurable f) (b : ℝ) : TransferStein.zMinusLaw (MeasureTheory.volume.withDensity f) b = MeasureTheory.volume.withDensity (LikelihoodRatio.fMinus f b)

The pushforward law of a negative exponential shift has density LikelihoodRatio.fMinus.

theorem Feige.Lemma43Density.ofReal_u_withDensity_eq_uIntegral {g : ℝ → ENNReal} (hg : Measurable g) [MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.withDensity g)] {d : ℝ} (hd : 0 < d) : ENNReal.ofReal (Lemma43.u (MeasureTheory.volume.withDensity g) d) = LikelihoodRatio.uIntegral g d

For a finite measure presented by a density, the actual upper-tail probability used by Lemma43 is its uIntegral.

theorem Feige.Lemma43Density.ofReal_v_withDensity_eq_vIntegral {g : ℝ → ENNReal} (hg : Measurable g) [MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.withDensity g)] {c : ℝ} (hc : 0 < c) : ENNReal.ofReal (Lemma43.v (MeasureTheory.volume.withDensity g) c) = LikelihoodRatio.vIntegral g c

The analogous density identification for the lower-tail probability.

theorem Feige.Lemma43Density.densityIdentification_zPlus_zMinus {f : ℝ → ENNReal} (hf : Measurable f) [MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.withDensity f)] {a b c d : ℝ} (hc : 0 < c) (hd : 0 < d) : Lemma43.DensityIdentification f (TransferStein.zPlusLaw (MeasureTheory.volume.withDensity f) a) (TransferStein.zMinusLaw (MeasureTheory.volume.withDensity f) b) a b c d

The four density identifications required by Lemma43 are automatic for the actual positive and negative exponential-shift laws of a density.

theorem Feige.Lemma43Density.theta_order_zPlus_zMinus {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) : Lemma43.theta (TransferStein.zMinusLaw (MeasureTheory.volume.withDensity f) b) c d ≤ Lemma43.theta (TransferStein.zPlusLaw (MeasureTheory.volume.withDensity f) a) c d

Consequently, the likelihood-ratio order of the two actual shifted laws needs no separate density-identification hypothesis.