The terminal law in the insertion argument

The common variable on the terminal edge is the sum of the negative old coordinates, with the distinguished positive exponential removed.

def Feige.terminalCommonSignedSum {n : ℕ} (β : Fin (n + 1) → ℝ) (e : Fin n → NNReal) : ℝ

The all-negative signed exponential sum at the terminal chain state.

Equations

• Feige.terminalCommonSignedSum β e = -∑ i : Fin n, β i.castSucc * ↑(e i)

noncomputable def Feige.terminalCommonLaw {n : ℕ} (β : Fin (n + 1) → ℝ) : MeasureTheory.Measure ℝ

The law of the terminal all-negative signed exponential sum.

Equations

• Feige.terminalCommonLaw β = MeasureTheory.Measure.map (Feige.terminalCommonSignedSum β) (MeasureTheory.Measure.pi fun (x : Fin n) => Feige.nnexpMeasure)

theorem Feige.measurable_terminalCommonSignedSum {n : ℕ} (β : Fin (n + 1) → ℝ) : Measurable (terminalCommonSignedSum β)

instance Feige.terminalCommonLaw_isProbability {n : ℕ} (β : Fin (n + 1) → ℝ) : MeasureTheory.IsProbabilityMeasure (terminalCommonLaw β)

theorem Feige.terminalCommonLaw_Ioi_zero {n : ℕ} (β : Fin (n + 1) → ℝ) (hβ : ∀ (i : Fin (n + 1)), 0 < β i) : (terminalCommonLaw β) (Set.Ioi 0) = 0

theorem Feige.zPlus_terminalCommonLaw_eq_stateLaw_univ {n : ℕ} (γ β : Fin (n + 1) → ℝ) : TransferStein.zPlusLaw (terminalCommonLaw β) 1 = stateLaw (fun (i : Fin n) => γ i.castSucc) (fun (i : Fin n) => β i.castSucc) Finset.univ

theorem Feige.realizesInsertionEdge_terminal {n : ℕ} (γ β : Fin (n + 1) → ℝ) (hγ : ∀ (i : Fin (n + 1)), 0 < γ i) (hβ : ∀ (i : Fin (n + 1)), 0 < β i) (σ : Equiv.Perm (Fin n)) : Lemma43.RealizesInsertionEdge (insertionUpperK γ β σ) (insertionOldK γ β σ) (insertionWidth γ β σ) (insertionTheta γ β σ) n (TransferStein.zPlusLaw (terminalCommonLaw β) 1) (TransferStein.zMinusLaw (terminalCommonLaw β) 1) (γ (Fin.last n)) (β (Fin.last n))