Calibrated measures on finite chains

This file formalizes the telescoping chain-calibration step used in the proof of Theorem 2.1. We use the sentinel convention K (m + 1) = 0; consequently every chain mass, including the last one, is uniformly the adjacent difference

q j = K j - K (j + 1).

The key fact is that the mass of a terminal segment beginning at t is exactly K t, which gives exact chain calibration whenever the rejected states form that terminal segment.

def Feige.chainMass (K : ℕ → ℝ) (j : ℕ) : ℝ

Adjacent-difference mass associated with a decreasing sequence.

Equations

• Feige.chainMass K j = K j - K (j + 1)

structure Feige.CalibratedChain (m : ℕ) : Type

A decreasing chain of m + 1 statistic values, extended by a zero sentinel at index m + 1.

• K : ℕ → ℝ

  The statistic along the chain.

• antitone : Antitone self.K
• initial : self.K 0 = 1
• sentinel : self.K (m + 1) = 0

noncomputable def Feige.CalibratedChain.rejectedMass {m : ℕ} (C : CalibratedChain m) (α : ℝ) : ℝ

Total chain mass of states whose statistic does not exceed α.

Equations

• C.rejectedMass α = ∑ j ∈ Finset.range (m + 1) with C.K j ≤ α, Feige.chainMass C.K j

theorem Feige.CalibratedChain.mass_nonneg {m : ℕ} (C : CalibratedChain m) (j : ℕ) : 0 ≤ chainMass C.K j

theorem Feige.CalibratedChain.sum_chainMass_shift (K : ℕ → ℝ) (t r : ℕ) : ∑ j ∈ Finset.range r, chainMass K (t + j) = K t - K (t + r)

A shifted telescoping sum of adjacent differences.

theorem Feige.CalibratedChain.sum_chainMass_Ico (K : ℕ → ℝ) {t u : ℕ} (htu : t ≤ u) : ∑ j ∈ Finset.Ico t u, chainMass K j = K t - K u

Telescoping over a half-open interval of indices.

theorem Feige.CalibratedChain.total_mass {m : ℕ} (C : CalibratedChain m) : ∑ j ∈ Finset.range (m + 1), chainMass C.K j = 1

The adjacent-difference masses telescope to one.

theorem Feige.CalibratedChain.terminal_mass {m : ℕ} (C : CalibratedChain m) {t : ℕ} (ht : t ≤ m + 1) : ∑ j ∈ Finset.range (m + 1 - t), chainMass C.K (t + j) = C.K t

The mass from position t through the final genuine state m is exactly the statistic value at t.

theorem Feige.CalibratedChain.terminal_mass_Ico {m : ℕ} (C : CalibratedChain m) {t : ℕ} (ht : t ≤ m + 1) : ∑ j ∈ Finset.Ico t (m + 1), chainMass C.K j = C.K t

theorem Feige.CalibratedChain.calibration_terminal {m : ℕ} (C : CalibratedChain m) {t : ℕ} (ht : t ≤ m + 1) {α : ℝ} (hreject : C.K t ≤ α) : ∑ j ∈ Finset.range (m + 1 - t), chainMass C.K (t + j) ≤ α

Terminal-segment form of exact chain calibration: if rejection begins at t, its chain probability is at most its threshold α.

theorem Feige.CalibratedChain.exact_chain_calibration {m : ℕ} (C : CalibratedChain m) {t : ℕ} (ht : t ≤ m + 1) {α : ℝ} (hα : 0 ≤ α) (hterminal : ∀ j < m + 1, C.K j ≤ α ↔ t ≤ j) (hreject : t ≤ m → C.K t ≤ α) : C.rejectedMass α ≤ α

Rejection-set formulation of exact chain calibration. Monotonicity makes the rejected states a terminal segment; hterminal names its first index. The case t = m + 1 represents an empty rejection set.

theorem Feige.CalibratedChain.exact_chain_calibration' {m : ℕ} (C : CalibratedChain m) {α : ℝ} (hα : 0 ≤ α) : C.rejectedMass α ≤ α

Exact calibration along a chain, with the first rejected state chosen automatically. The zero sentinel guarantees that such an index exists; if it is the sentinel itself, the genuine rejection set is empty.