Local transfer for finite signed-exponential common parts #
This module specializes the automatic pushforward-density and likelihood-ratio results to the exact common laws appearing on genuine Boolean-lattice insertion edges.
theorem
Feige.Lemma43.finiteSignedExp_theta_order
(Fs : List LikelihoodRatio.SignedExpFactor)
{a b c d : ℝ}
(ha : 0 ≤ a)
(hb : 0 ≤ b)
(hc : 0 < c)
(hd : 0 < d)
:
The order half of the local transfer result for a distinguished exponential plus an arbitrary finite list of signed scaled exponentials.
theorem
Feige.Lemma43.finiteSignedExp_complete
(Fs : List LikelihoodRatio.SignedExpFactor)
{a b c d : ℝ}
(ha : 0 < a)
(hb : 0 < b)
(hc : 0 < c)
(hd : 0 < d)
:
The full local transfer result, with every analytic and probability hypothesis discharged, for a finite signed-exponential common part.
theorem
Feige.Lemma43.commonFactors_theta_order
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(γ β : ι → ℝ)
(hγ : ∀ (i : ι), 0 < γ i)
(hβ : ∀ (i : ι), 0 < β i)
(S : Finset ι)
(changed : ι)
{c d : ℝ}
(hc : 0 < c)
(hd : 0 < d)
:
theta
(TransferStein.zMinusLaw
(MeasureTheory.volume.withDensity
(LikelihoodRatio.finiteSignedExpSumDensity (LikelihoodRatio.commonFactors γ β hγ hβ S changed)))
(β changed))
c d ≤ theta
(TransferStein.zPlusLaw
(MeasureTheory.volume.withDensity
(LikelihoodRatio.finiteSignedExpSumDensity (LikelihoodRatio.commonFactors γ β hγ hβ S changed)))
(γ changed))
c d
Actual insertion-edge specialization: the changed low coordinate is the positive shift and the changed high coordinate is the negative shift.
theorem
Feige.Lemma43.commonFactors_complete
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(γ β : ι → ℝ)
(hγ : ∀ (i : ι), 0 < γ i)
(hβ : ∀ (i : ι), 0 < β i)
(S : Finset ι)
(changed : ι)
{c d : ℝ}
(hc : 0 < c)
(hd : 0 < d)
:
CompleteConclusion (LikelihoodRatio.finiteSignedExpSumDensity (LikelihoodRatio.commonFactors γ β hγ hβ S changed))
(γ changed) (β changed) c d
The full automatic local transfer result on every genuine insertion edge.