Probability measures carried by maximal chains

The auxiliary chain distribution mentioned in the proof outline is a finite probability mass function on the levels of a maximal chain. This file packages its expectation and relates the indicator of a threshold rejection event to rejectedMass.

noncomputable def Feige.CalibratedChain.expectation {m : ℕ} (C : CalibratedChain m) (g : ℕ → ℝ) : ℝ

Expectation of a payoff on the m + 1 genuine levels of a calibrated chain.

Equations

• C.expectation g = ∑ j ∈ Finset.range (m + 1), Feige.chainMass C.K j * g j

theorem Feige.CalibratedChain.expectation_one {m : ℕ} (C : CalibratedChain m) : (C.expectation fun (x : ℕ) => 1) = 1

theorem Feige.CalibratedChain.expectation_nonneg {m : ℕ} (C : CalibratedChain m) {g : ℕ → ℝ} (hg : ∀ j < m + 1, 0 ≤ g j) : 0 ≤ C.expectation g

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

The rejection indicator used for exact chain calibration.

Equations

• C.rejectionIndicator α j = if C.K j ≤ α then 1 else 0

theorem Feige.CalibratedChain.expectation_rejectionIndicator {m : ℕ} (C : CalibratedChain m) (α : ℝ) : C.expectation (C.rejectionIndicator α) = C.rejectedMass α

Expectation of the rejection indicator is exactly the previously defined rejection mass.

theorem Feige.CalibratedChain.expectation_rejection_le {m : ℕ} (C : CalibratedChain m) {α : ℝ} (hα : 0 ≤ α) : C.expectation (C.rejectionIndicator α) ≤ α

Exact calibration in expectation form.

noncomputable def Feige.booleanChainExpectation {m : ℕ} (γ β : Fin m → ℝ) (σ : Equiv.Perm (Fin m)) (hγ : ∀ (i : Fin m), 0 ≤ γ i) (hβ : ∀ (i : Fin m), 0 ≤ β i) (g : Finset (Fin m) → ℝ) : ℝ

Expectation E_{ν_C} g for the auxiliary maximal-chain law.

Equations

• Feige.booleanChainExpectation γ β σ hγ hβ g = (Feige.booleanCalibratedChain γ β σ hγ hβ).expectation fun (j : ℕ) => if hj : j < m + 1 then g (Feige.chainState σ ⟨j, hj⟩) else 0

noncomputable def Feige.booleanRejectionPayoff {m : ℕ} (γ β : Fin m → ℝ) (α : ℝ) (S : Finset (Fin m)) : ℝ

Increasing rejection payoff on the Boolean lattice.

Equations

• Feige.booleanRejectionPayoff γ β α S = if Feige.twoPointKFinset γ β S ≤ α then 1 else 0

theorem Feige.booleanChainExpectation_one {m : ℕ} (γ β : Fin m → ℝ) (σ : Equiv.Perm (Fin m)) (hγ : ∀ (i : Fin m), 0 ≤ γ i) (hβ : ∀ (i : Fin m), 0 ≤ β i) : (booleanChainExpectation γ β σ hγ hβ fun (x : Finset (Fin m)) => 1) = 1

theorem Feige.booleanChain_rejection_le {m : ℕ} (γ β : Fin m → ℝ) (σ : Equiv.Perm (Fin m)) (hγ : ∀ (i : Fin m), 0 ≤ γ i) (hβ : ∀ (i : Fin m), 0 ≤ β i) {α : ℝ} (hα : 0 ≤ α) : booleanChainExpectation γ β σ hγ hβ (booleanRejectionPayoff γ β α) ≤ α

Exact calibration stated directly for the statistic evaluated on the states of a maximal Boolean chain.