Signed-sum laws along a Boolean insertion edge

The event defining twoPointKFinset is rewritten as nonnegativity of the corresponding signed exponential sum.

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

def Feige.stateSignedSum {ι : Type u_1} [Fintype ι] [DecidableEq ι] (γ β : ι → ℝ) (S : Finset ι) (e : Option ι → NNReal) : ℝ

The signed exponential statistic at Boolean state S.

Equations

• Feige.stateSignedSum γ β S e = ↑(e none) + ∑ i : ι, if i ∈ S then -(β i * ↑(e (some i))) else γ i * ↑(e (some i))

theorem Feige.measurable_stateSignedSum {ι : Type u_1} [Fintype ι] [DecidableEq ι] (γ β : ι → ℝ) (S : Finset ι) : Measurable (stateSignedSum γ β S)

noncomputable def Feige.stateLaw {ι : Type u_1} [Fintype ι] [DecidableEq ι] (γ β : ι → ℝ) (S : Finset ι) : MeasureTheory.Measure ℝ

Pushforward law of the signed sum at state S.

Equations

• Feige.stateLaw γ β S = MeasureTheory.Measure.map (Feige.stateSignedSum γ β S) (Feige.expProductMeasure ι)

instance Feige.stateLaw_isProbability {ι : Type u_1} [Fintype ι] [DecidableEq ι] (γ β : ι → ℝ) (S : Finset ι) : MeasureTheory.IsProbabilityMeasure (stateLaw γ β S)

theorem Feige.kEvent_twoPointVector_eq_stateSignedSum {ι : Type u_1} [Fintype ι] [DecidableEq ι] (γ β : ι → ℝ) (S : Finset ι) : kEvent (twoPointVector γ β ↑S) = stateSignedSum γ β S ⁻¹' Set.Ici 0

The original event in the definition of K is exactly nonnegativity of the signed sum.

theorem Feige.twoPointKFinset_eq_stateLaw {ι : Type u_1} [Fintype ι] [DecidableEq ι] (γ β : ι → ℝ) (S : Finset ι) : twoPointKFinset γ β S = ((stateLaw γ β S) (Set.Ici 0)).toReal

twoPointKFinset is the nonnegative-tail probability of the actual signed exponential state law.

def Feige.stateCommonSignedSum {ι : Type u_1} [Fintype ι] [DecidableEq ι] (γ β : ι → ℝ) (S : Finset ι) (changed : ι) (e : Option ι → NNReal) : ℝ

The common signed sum obtained by deleting the changed coordinate, on the original product sample space.

Equations

• Feige.stateCommonSignedSum γ β S changed e = ↑(e none) + ∑ i ∈ Finset.univ.erase changed, if i ∈ S then -(β i * ↑(e (some i))) else γ i * ↑(e (some i))

theorem Feige.measurable_stateCommonSignedSum {ι : Type u_1} [Fintype ι] [DecidableEq ι] (γ β : ι → ℝ) (S : Finset ι) (changed : ι) : Measurable (stateCommonSignedSum γ β S changed)

theorem Feige.stateSignedSum_eq_common_add {ι : Type u_1} [Fintype ι] [DecidableEq ι] (γ β : ι → ℝ) (S : Finset ι) (changed : ι) (hj : changed ∉ S) (e : Option ι → NNReal) : stateSignedSum γ β S e = stateCommonSignedSum γ β S changed e + γ changed * ↑(e (some changed))

At the low endpoint, the state sum is the common sum plus the changed positive exponential.

theorem Feige.stateSignedSum_insert_eq_common_sub {ι : Type u_1} [Fintype ι] [DecidableEq ι] (γ β : ι → ℝ) (S : Finset ι) (changed : ι) (hj : changed ∉ S) (e : Option ι → NNReal) : stateSignedSum γ β (insert changed S) e = stateCommonSignedSum γ β S changed e - β changed * ↑(e (some changed))

At the high endpoint, the changed coordinate contributes the corresponding negative exponential to the same common sum.

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

The common law on an insertion edge, constructed as the convolution of the unchanged signed exponential factors together with the distinguished rate-one exponential E₀.

Equations

• Feige.insertionCommonLaw γ β hγ hβ S changed = Feige.LikelihoodRatio.finiteSignedExpSumMeasure (Feige.LikelihoodRatio.commonFactors γ β hγ hβ S changed)

instance Feige.insertionCommonLaw_isProbability {ι : Type u_1} [Fintype ι] [DecidableEq ι] (γ β : ι → ℝ) (hγ : ∀ (i : ι), 0 < γ i) (hβ : ∀ (i : ι), 0 < β i) (S : Finset ι) (changed : ι) : MeasureTheory.IsProbabilityMeasure (insertionCommonLaw γ β hγ hβ S changed)

theorem Feige.insertionCommonLaw_eq_withDensity {ι : Type u_1} [Fintype ι] [DecidableEq ι] (γ β : ι → ℝ) (hγ : ∀ (i : ι), 0 < γ i) (hβ : ∀ (i : ι), 0 < β i) (S : Finset ι) (changed : ι) : insertionCommonLaw γ β hγ hβ S changed = MeasureTheory.volume.withDensity (LikelihoodRatio.finiteSignedExpSumDensity (LikelihoodRatio.commonFactors γ β hγ hβ S changed))

The common law has exactly the explicit finite signed-exponential density used by the TP2 argument.

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

Law of the low endpoint obtained by adding the changed coordinate's positive scaled exponential to the common part.

Equations

• Feige.insertionLowEndpointLaw γ β hγ hβ S changed = Feige.TransferStein.zPlusLaw (Feige.insertionCommonLaw γ β hγ hβ S changed) (γ changed)

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

Law of the high endpoint obtained by subtracting the changed coordinate's scaled exponential from the common part.

Equations

• Feige.insertionHighEndpointLaw γ β hγ hβ S changed = Feige.TransferStein.zMinusLaw (Feige.insertionCommonLaw γ β hγ hβ S changed) (β changed)

theorem Feige.insertionLowEndpointLaw_eq_zPlus {ι : Type u_1} [Fintype ι] [DecidableEq ι] (γ β : ι → ℝ) (hγ : ∀ (i : ι), 0 < γ i) (hβ : ∀ (i : ι), 0 < β i) (S : Finset ι) (changed : ι) : insertionLowEndpointLaw γ β hγ hβ S changed = TransferStein.zPlusLaw (insertionCommonLaw γ β hγ hβ S changed) (γ changed)

theorem Feige.insertionHighEndpointLaw_eq_zMinus {ι : Type u_1} [Fintype ι] [DecidableEq ι] (γ β : ι → ℝ) (hγ : ∀ (i : ι), 0 < γ i) (hβ : ∀ (i : ι), 0 < β i) (S : Finset ι) (changed : ι) : insertionHighEndpointLaw γ β hγ hβ S changed = TransferStein.zMinusLaw (insertionCommonLaw γ β hγ hβ S changed) (β changed)

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

The real-valued signed contribution of one coordinate.

Equations

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

theorem Feige.measurable_signedCoordinate {ι : Type u_1} [DecidableEq ι] (γ β : ι → ℝ) (hγ : ∀ (i : ι), 0 < γ i) (hβ : ∀ (i : ι), 0 < β i) (S : Finset ι) (i : ι) : Measurable (signedCoordinate γ β hγ hβ S i)

theorem Feige.map_signedCoordinate_nnexpMeasure {ι : Type u_1} [DecidableEq ι] (γ β : ι → ℝ) (hγ : ∀ (i : ι), 0 < γ i) (hβ : ∀ (i : ι), 0 < β i) (S : Finset ι) (i : ι) : MeasureTheory.Measure.map (signedCoordinate γ β hγ hβ S i) nnexpMeasure = (LikelihoodRatio.stateFactor γ β hγ hβ S i).sourceLaw

theorem Feige.iIndepFun_signedCoordinates {ι : Type u_1} [Fintype ι] [DecidableEq ι] (γ β : ι → ℝ) (hγ : ∀ (i : ι), 0 < γ i) (hβ : ∀ (i : ι), 0 < β i) (S : Finset ι) : ProbabilityTheory.iIndepFun (fun (o : Option ι) (e : Option ι → NNReal) => match o with | none => ↑(e none) | some i => signedCoordinate γ β hγ hβ S i (e (some i))) (expProductMeasure ι)

The distinguished exponential and all transformed coordinates are jointly independent on the canonical product space.

def Feige.transformedCoordinate {ι : Type u_1} [DecidableEq ι] (γ β : ι → ℝ) (hγ : ∀ (i : ι), 0 < γ i) (hβ : ∀ (i : ι), 0 < β i) (S : Finset ι) (o : Option ι) (e : Option ι → NNReal) : ℝ

The distinguished exponential or a signed coordinate on the product space.

Equations

• Feige.transformedCoordinate γ β hγ hβ S none e = ↑(e none)
• Feige.transformedCoordinate γ β hγ hβ S (some i) e = Feige.signedCoordinate γ β hγ hβ S i (e (some i))

theorem Feige.measurable_transformedCoordinate {ι : Type u_1} [DecidableEq ι] (γ β : ι → ℝ) (hγ : ∀ (i : ι), 0 < γ i) (hβ : ∀ (i : ι), 0 < β i) (S : Finset ι) (o : Option ι) : Measurable (transformedCoordinate γ β hγ hβ S o)

theorem Feige.map_transformedCoordinate_some {ι : Type u_1} [Fintype ι] [DecidableEq ι] (γ β : ι → ℝ) (hγ : ∀ (i : ι), 0 < γ i) (hβ : ∀ (i : ι), 0 < β i) (S : Finset ι) (i : ι) : MeasureTheory.Measure.map (transformedCoordinate γ β hγ hβ S (some i)) (expProductMeasure ι) = (LikelihoodRatio.stateFactor γ β hγ hβ S i).sourceLaw

def Feige.commonIndexSet {ι : Type u_1} [DecidableEq ι] (T : Finset ι) : Finset (Option ι)

The distinguished index together with the coordinate indices in T.

Equations

• Feige.commonIndexSet T = insert none (Finset.image some T)

theorem Feige.sum_commonIndexSet {ι : Type u_1} [DecidableEq ι] (γ β : ι → ℝ) (hγ : ∀ (i : ι), 0 < γ i) (hβ : ∀ (i : ι), 0 < β i) (S T : Finset ι) (e : Option ι → NNReal) : ∑ o ∈ commonIndexSet T, transformedCoordinate γ β hγ hβ S o e = ↑(e none) + ∑ i ∈ T, signedCoordinate γ β hγ hβ S i (e (some i))

theorem Feige.finiteSignedExpSumSourceMeasure_perm {Fs Gs : List LikelihoodRatio.SignedExpFactor} (h : Fs.Perm Gs) : LikelihoodRatio.finiteSignedExpSumSourceMeasure Fs = LikelihoodRatio.finiteSignedExpSumSourceMeasure Gs

theorem Feige.map_common_coordinate_sum {ι : Type u_1} [Fintype ι] [DecidableEq ι] (γ β : ι → ℝ) (hγ : ∀ (i : ι), 0 < γ i) (hβ : ∀ (i : ι), 0 < β i) (S T : Finset ι) : MeasureTheory.Measure.map (fun (e : Option ι → NNReal) => ∑ o ∈ commonIndexSet T, transformedCoordinate γ β hγ hβ S o e) (expProductMeasure ι) = LikelihoodRatio.finiteSignedExpSumSourceMeasure (List.map (LikelihoodRatio.stateFactor γ β hγ hβ S) T.toList)

theorem Feige.stateCommonLaw_eq_insertionCommonLaw {ι : Type u_1} [Fintype ι] [DecidableEq ι] (γ β : ι → ℝ) (hγ : ∀ (i : ι), 0 < γ i) (hβ : ∀ (i : ι), 0 < β i) (S : Finset ι) (changed : ι) : MeasureTheory.Measure.map (stateCommonSignedSum γ β S changed) (expProductMeasure ι) = insertionCommonLaw γ β hγ hβ S changed

theorem Feige.zPlusLaw_eq_conv_map_mul (ν : MeasureTheory.Measure ℝ) [MeasureTheory.SFinite ν] (t : ℝ) : TransferStein.zPlusLaw ν t = ν.conv (MeasureTheory.Measure.map (fun (x : ℝ) => t * x) (ProbabilityTheory.expMeasure 1))

theorem Feige.zMinusLaw_eq_conv_map_neg_mul (ν : MeasureTheory.Measure ℝ) [MeasureTheory.SFinite ν] (t : ℝ) : TransferStein.zMinusLaw ν t = ν.conv (MeasureTheory.Measure.map (fun (x : ℝ) => -(t * x)) (ProbabilityTheory.expMeasure 1))

theorem Feige.stateLaw_eq_finiteSignedExpSumMeasure {ι : Type u_1} [Fintype ι] [DecidableEq ι] (γ β : ι → ℝ) (hγ : ∀ (i : ι), 0 < γ i) (hβ : ∀ (i : ι), 0 < β i) (S : Finset ι) : stateLaw γ β S = LikelihoodRatio.finiteSignedExpSumMeasure (List.map (LikelihoodRatio.stateFactor γ β hγ hβ S) Finset.univ.toList)

theorem Feige.insertionLowEndpointLaw_eq_stateLaw {ι : Type u_1} [Fintype ι] [DecidableEq ι] (γ β : ι → ℝ) (hγ : ∀ (i : ι), 0 < γ i) (hβ : ∀ (i : ι), 0 < β i) (S : Finset ι) (changed : ι) (hj : changed ∉ S) : insertionLowEndpointLaw γ β hγ hβ S changed = stateLaw γ β S

theorem Feige.insertionHighEndpointLaw_eq_stateLaw_insert {ι : Type u_1} [Fintype ι] [DecidableEq ι] (γ β : ι → ℝ) (hγ : ∀ (i : ι), 0 < γ i) (hβ : ∀ (i : ι), 0 < β i) (S : Finset ι) (changed : ι) : insertionHighEndpointLaw γ β hγ hβ S changed = stateLaw γ β (insert changed S)