Common densities on insertion edges

For a Boolean state, every unchanged low coordinate contributes a positive scaled exponential and every unchanged high coordinate contributes a negative scaled exponential. This file packages those factors and applies the finite-convolution TP2 theorem to the common part of any genuine edge.

def Feige.LikelihoodRatio.stateFactor {ι : Type u_1} [DecidableEq ι] (γ β : ι → ℝ) (hγ : ∀ (i : ι), 0 < γ i) (hβ : ∀ (i : ι), 0 < β i) (S : Finset ι) (i : ι) : SignedExpFactor

The signed exponential contributed by coordinate i in state S.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Feige.LikelihoodRatio.commonFactors {ι : Type u_1} [Fintype ι] [DecidableEq ι] (γ β : ι → ℝ) (hγ : ∀ (i : ι), 0 < γ i) (hβ : ∀ (i : ι), 0 < β i) (S : Finset ι) (changed : ι) : List SignedExpFactor

All signed exponential factors shared by the two endpoints of the edge which changes changed.

Equations

• Feige.LikelihoodRatio.commonFactors γ β hγ hβ S changed = List.map (Feige.LikelihoodRatio.stateFactor γ β hγ hβ S) (Finset.univ.erase changed).toList

theorem Feige.LikelihoodRatio.fourPointLogConcave_commonFactors {ι : Type u_1} [Fintype ι] [DecidableEq ι] (γ β : ι → ℝ) (hγ : ∀ (i : ι), 0 < γ i) (hβ : ∀ (i : ι), 0 < β i) (S : Finset ι) (changed : ι) : FourPointLogConcave (finiteSignedExpSumDensity (commonFactors γ β hγ hβ S changed))

Every genuine insertion-edge common density satisfies the exact four-point hypothesis consumed by the likelihood-ratio proof.

theorem Feige.LikelihoodRatio.translationTP2_commonFactors {ι : Type u_1} [Fintype ι] [DecidableEq ι] (γ β : ι → ℝ) (hγ : ∀ (i : ι), 0 < γ i) (hβ : ∀ (i : ι), 0 < β i) (S : Finset ι) (changed : ι) : TranslationTP2 (finiteSignedExpSumDensity (commonFactors γ β hγ hβ S changed))

Translation-TP2 form of the same insertion-edge conclusion.