Calibrated statistic sequences along maximal Boolean chains

This file evaluates twoPointKFinset on the states of a maximal chain and extends the resulting finite sequence by zero. The extension is a CalibratedChain, so the exact telescoping calibration lemma applies immediately.

noncomputable def Feige.booleanChainK {m : ℕ} (γ β : Fin m → ℝ) (σ : Equiv.Perm (Fin m)) (j : ℕ) : ℝ

The two-point statistic along the maximal chain encoded by σ, extended by zero from the sentinel index m + 1 onwards.

Equations

• Feige.booleanChainK γ β σ j = if hj : j < m + 1 then Feige.twoPointKFinset γ β (Feige.chainState σ ⟨j, hj⟩) else 0

@[simp]

theorem Feige.booleanChainK_of_lt {m : ℕ} (γ β : Fin m → ℝ) (σ : Equiv.Perm (Fin m)) {j : ℕ} (hj : j < m + 1) : booleanChainK γ β σ j = twoPointKFinset γ β (chainState σ ⟨j, hj⟩)

@[simp]

theorem Feige.booleanChainK_of_not_lt {m : ℕ} (γ β : Fin m → ℝ) (σ : Equiv.Perm (Fin m)) {j : ℕ} (hj : ¬j < m + 1) : booleanChainK γ β σ j = 0

theorem Feige.booleanChainK_sentinel {m : ℕ} (γ β : Fin m → ℝ) (σ : Equiv.Perm (Fin m)) : booleanChainK γ β σ (m + 1) = 0

theorem Feige.twoPointKFinset_nonneg {ι : Type u_1} [Fintype ι] (γ β : ι → ℝ) (S : Finset ι) : 0 ≤ twoPointKFinset γ β S

theorem Feige.booleanChainK_antitone {m : ℕ} (γ β : Fin m → ℝ) (σ : Equiv.Perm (Fin m)) (hγ : ∀ (i : Fin m), 0 ≤ γ i) (hβ : ∀ (i : Fin m), 0 ≤ β i) : Antitone (booleanChainK γ β σ)

theorem Feige.booleanChainK_initial {m : ℕ} (γ β : Fin m → ℝ) (σ : Equiv.Perm (Fin m)) (hγ : ∀ (i : Fin m), 0 ≤ γ i) : booleanChainK γ β σ 0 = 1

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

The calibrated sequence carried by a maximal Boolean-lattice chain.

Equations

• Feige.booleanCalibratedChain γ β σ hγ hβ = { K := Feige.booleanChainK γ β σ, antitone := ⋯, initial := ⋯, sentinel := ⋯ }

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

Exact calibration for the statistic values along any maximal Boolean-lattice chain.