Assembly of the analytic insertion edges

This file performs the last finite bookkeeping step in the chain-insertion argument for Theorem 2.1. Once each genuine edge of the old chain is represented by the two signed-exponential endpoint laws from the local transfer step, and the terminal edge is represented by its one-sided common law, all positivity, monotonicity, and transfer hypotheses required by exists_insertChainPerm_dominates_reveal follow automatically.

def Feige.insertionEdgeScale {n : ℕ} (γ : Fin (n + 1) → ℝ) (σ : Equiv.Perm (Fin n)) (j : ℕ) : ℝ

The low-side scale of the old coordinate changed at edge j; it equals 1 at the terminal edge, which changes the distinguished exponential.

Equations

• Feige.insertionEdgeScale γ σ j = if hj : j < n then γ (σ ⟨j, hj⟩).castSucc else 1

theorem Feige.insertionTheta_eq_zero_of_ge {n : ℕ} (γ β : Fin (n + 1) → ℝ) (σ : Equiv.Perm (Fin n)) {r : ℕ} (hr : n + 1 ≤ r) : insertionTheta γ β σ r = 0

The zero-extended interpolation sequence is identically zero from its sentinel onward.

theorem Feige.exists_insertChainPerm_dominates_reveal_of_realizedEdges {n : ℕ} (γ β : Fin (n + 1) → ℝ) (hγpos : ∀ (i : Fin (n + 1)), 0 < γ i) (hγle : ∀ (i : Fin (n + 1)), γ i ≤ 1) (hβpos : ∀ (i : Fin (n + 1)), 0 < β i) (hγord : Antitone γ) (σ : Equiv.Perm (Fin n)) {g : Finset (Fin (n + 1)) → ℝ} (hg : Monotone g) (Fs : Fin n → List LikelihoodRatio.SignedExpFactor) (hrealInterior : ∀ (j : Fin n), Lemma43.RealizesInsertionEdge (insertionUpperK γ β σ) (insertionOldK γ β σ) (insertionWidth γ β σ) (insertionTheta γ β σ) (↑j) (TransferStein.zPlusLaw (MeasureTheory.volume.withDensity (LikelihoodRatio.finiteSignedExpSumDensity (Fs j))) (γ (σ j).castSucc)) (TransferStein.zMinusLaw (MeasureTheory.volume.withDensity (LikelihoodRatio.finiteSignedExpSumDensity (Fs j))) (β (σ j).castSucc)) (γ (Fin.last n)) (β (Fin.last n))) (μterminal : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure μterminal] (hterminalSupport : μterminal (Set.Ioi 0) = 0) (hrealTerminal : Lemma43.RealizesInsertionEdge (insertionUpperK γ β σ) (insertionOldK γ β σ) (insertionWidth γ β σ) (insertionTheta γ β σ) n (TransferStein.zPlusLaw μterminal 1) (TransferStein.zMinusLaw μterminal 1) (γ (Fin.last n)) (β (Fin.last n))) : ∃ (J : Fin (n + 1)), booleanChainExpectation (fun (i : Fin n) => γ i.castSucc) (fun (i : Fin n) => β i.castSucc) σ ⋯ ⋯ (revealedLastPayoff (twoPointHighProbability γ β (Fin.last n)) g) ≤ booleanChainExpectation γ β (insertChainPerm σ J) ⋯ ⋯ g

The chain-insertion conclusion after all measure-theoretic endpoint identifications have been exposed as RealizesInsertionEdge hypotheses.

There is one genuine signed-exponential edge for every old coordinate. The final edge changes the distinguished E₀ from positive to negative; its common law need only be supported on the nonpositive half-line.