Definitions for the Kalton-Roberts formalization

Core definitions used throughout the formalization of the companion paper.

Basic definitions from Section 1

def KaltonRoberts.IsApproxAdditive {U : Type u_1} [DecidableEq U] (f : Finset U → ℝ) (Δ : ℝ) : Prop

A function f : Finset U → ℝ is Δ-additive if f ∅ = 0 and |f A + f B − f (A ∪ B)| ≤ Δ for every pair of disjoint finite subsets A, B. Reference: Equation (1) in Section 1 of the companion paper.

Equations

• KaltonRoberts.IsApproxAdditive f Δ = (f ∅ = 0 ∧ ∀ (A B : Finset U), Disjoint A B → |f A + f B - f (A ∪ B)| ≤ Δ)

def KaltonRoberts.IsApproxAdditiveBA {α : Type u_1} [BooleanAlgebra α] (f : α → ℝ) (Δ : ℝ) : Prop

A function on an abstract Boolean algebra is Δ-additive if it vanishes at bottom and is additive up to Δ on disjoint joins.

This is the set-algebra formulation from Equation (1), with a set algebra represented by its Boolean algebra of events. A concrete algebra of subsets is the subtype of a BooleanSubalgebra (Set Ω).

Equations

• KaltonRoberts.IsApproxAdditiveBA f Δ = (f ⊥ = 0 ∧ ∀ (A B : α), Disjoint A B → |f A + f B - f (A ⊔ B)| ≤ Δ)

def KaltonRoberts.IsFinitelyAdditiveBA {α : Type u_1} [BooleanAlgebra α] (μ : α → ℝ) : Prop

A finitely additive signed measure on a Boolean algebra.

Equations

• KaltonRoberts.IsFinitelyAdditiveBA μ = (μ ⊥ = 0 ∧ ∀ (A B : α), Disjoint A B → μ (A ⊔ B) = μ A + μ B)

def KaltonRoberts.additiveFunction {U : Type u_1} (a : U → ℝ) : Finset U → ℝ

An additive signed measure on 2^U is identified with a function A ↦ ∑ i ∈ A, a i for some weight function a : U → ℝ. Reference: paragraph after Lemma 1.2 in Section 1 of the companion paper.

Equations

• KaltonRoberts.additiveFunction a A = ∑ i ∈ A, a i

noncomputable def KaltonRoberts.distToAdditive {U : Type u_1} (f : Finset U → ℝ) : ℝ

The ℓ∞-distance from f to the subspace of additive signed measures on 2^U. Reference: last paragraph of Section 1 in the companion paper, where M := ‖f‖_∞ = dist_∞(f, L) after subtracting a closest additive approximant.

Equations

• KaltonRoberts.distToAdditive f = ⨅ (a : U → ℝ), ⨆ (S : Finset U), |f S - KaltonRoberts.additiveFunction a S|

def KaltonRoberts.deficit {U : Type u_1} (f : Finset U → ℝ) (M : ℝ) (A : Finset U) : ℝ

The deficit of a set A relative to f and the value M: this is M − f(A). Used throughout Section 2–5 of the companion paper.

Equations

• KaltonRoberts.deficit f M A = M - f A

def KaltonRoberts.surplus {U : Type u_1} (f : Finset U → ℝ) (M : ℝ) (A : Finset U) : ℝ

The surplus of a set A relative to f and the value M: this is M + f(A). Used throughout Section 2–5 of the companion paper.

Equations

• KaltonRoberts.surplus f M A = M + f A

noncomputable def KaltonRoberts.krConstant : ℝ

The Kalton–Roberts constant K_KR is the infimum of all C ≥ 0 such that for every Boolean algebra of sets/events and every 1-additive function f : α → ℝ, there exists a finitely additive signed measure μ with sup |f − μ| ≤ C.

This abstract Boolean-algebra formulation captures the paper's statement for arbitrary set algebras: a set algebra is a Boolean subalgebra of Set Ω. Reference: paragraph after Equation (1) in Section 1 of the companion paper.

Equations

• One or more equations did not get rendered due to their size.

Expander definition from Section 3

def KaltonRoberts.ExpandersExist (α : ℚ) (r : ℕ) (θ : ℚ) : Prop

An (α, r, θ)-expander for parameter k is a bipartite multigraph G = (V, W; E) with |V| = 2k, |W| = 2θk, every vertex in V having degree r, such that every subset S ⊆ V with |S| ≤ 2αk has at least |S| distinct neighbours in W.

ExpandersExist α r θ asserts that such expanders exist for all sufficiently large admissible k.

Reference: paragraph before Lemma 3.2 in Section 3 of the companion paper.

Equations

• One or more equations did not get rendered due to their size.

Strong expander witness (Section 3, refined interface)

def KaltonRoberts.edgeNeighbors {V : Type u_1} {W : Type u_2} [DecidableEq W] {r : ℕ} (edge : V → Fin r → W) (v : V) : Finset W

Edge-neighbor set of vertex v in a bipartite graph with labelled edges.

Equations

• KaltonRoberts.edgeNeighbors edge v = Finset.image (edge v) Finset.univ

structure KaltonRoberts.FiniteExpanderWitness (r : ℕ) : Type 1

A concrete finite expander witness with r labelled edges per left vertex.

This represents a bipartite multigraph G = (V, W; E) where each left vertex v ∈ V has exactly r labelled edges edge v 0, …, edge v (r-1) going to right vertices in W. The expansion property guarantees that small left-subsets have many distinct right-neighbors.

Reference: paragraph before Lemma 3.2 in Section 3 of the companion paper.

• V : Type

  Left vertex type.

• W : Type

  Right vertex type.

• instFintypeV : Fintype self.V

  Fintype instance for V.

• instDecEqV : DecidableEq self.V

  DecidableEq instance for V.

• instFintypeW : Fintype self.W

  Fintype instance for W.

• instDecEqW : DecidableEq self.W

  DecidableEq instance for W.

• edge : self.V → Fin r → self.W

  The r labelled edges from each left vertex to right vertices.

• hV_pos : 0 < Fintype.card self.V

  V is nonempty.

• right_coverage (w : self.W) : ∃ (v : self.V) (e : Fin r), self.edge v e = w

  Right coverage: every right vertex is hit by at least one edge.

• expansionThreshold : ℕ

  Expansion threshold (typically ⌈2αk⌉).

• expansion (S : Finset self.V) : S.card ≤ self.expansionThreshold → (S.biUnion fun (v : self.V) => edgeNeighbors self.edge v).card ≥ S.card

  Expansion property: every subset of V of size at most expansionThreshold has at least as many distinct right-neighbors.

def KaltonRoberts.StrongExpandersExist (α : ℚ) (r : ℕ) (θ : ℚ) : Prop

StrongExpandersExist α r θ asserts that there exists a positive admissibility step step such that for all sufficiently large k divisible by step, there exists a FiniteExpanderWitness with:

• |V| = 2k,
• |W| = 2θk (exact integer, requiring admissibility),
• expansion threshold ⌈2αk⌉₊,
• right coverage,
• labelled r-edges.

The step/divisibility formulation corresponds to the paper's assertion that expanders exist for all sufficiently large admissible k, where admissible sizes form an infinite arithmetic progression.

Reference: Section 3 and Lemma 4.1 of the companion paper.

Equations

• One or more equations did not get rendered due to their size.

Entropy function from Section 4

noncomputable def KaltonRoberts.hEntropy (a b : ℝ) : ℝ

The function h(a, b) = a log a − b log b − (a − b) log(a − b) used in the definition of Φ_{r,θ}. Reference: paragraph before Equation (6) in Section 4 of the companion paper.

Equations

• KaltonRoberts.hEntropy a b = a * Real.log a - b * Real.log b - (a - b) * Real.log (a - b)

noncomputable def KaltonRoberts.Phi (r θ x : ℝ) : ℝ

The function Φ_{r,θ}(x) = h(1,x) + h(θ,x) + h(rx/θ, rx) − h(r, rx) from Equation (6) in Section 4 of the companion paper.

Equations

• KaltonRoberts.Phi r θ x = KaltonRoberts.hEntropy 1 x + KaltonRoberts.hEntropy θ x + KaltonRoberts.hEntropy (r * x / θ) (r * x) - KaltonRoberts.hEntropy r (r * x)

noncomputable def KaltonRoberts.Phi'' (r θ x : ℝ) : ℝ

The second derivative Φ''_{r,θ}(x) = (r−2)/x + (r−1)/(1−x) − 1/(θ−x), from Equation (8) in Section 4 of the companion paper.

Equations

• KaltonRoberts.Phi'' r θ x = (r - 2) / x + (r - 1) / (1 - x) - 1 / (θ - x)

Numerical constants from Section 5

def KaltonRoberts.q₀ : ℚ

The case-split parameter q₀ = 7437/15625. Reference: Equation (9) in Section 5 of the companion paper.

Equations

• KaltonRoberts.q₀ = 7437 / 15625

def KaltonRoberts.p₀ : ℚ

The complementary parameter p₀ = 1 − q₀ = 8188/15625. Reference: Equation (9) in Section 5 of the companion paper.

Equations

• KaltonRoberts.p₀ = 8188 / 15625

def KaltonRoberts.α₁ : ℚ

The frequency cap in Case 1: α₁ = 1003/10000. Reference: Equation (9) in Section 5 of the companion paper.

Equations

• KaltonRoberts.α₁ = 1003 / 10000

def KaltonRoberts.α₂ : ℚ

The frequency cap in Case 2: α₂ = 47/625. Reference: Equation (9) in Section 5 of the companion paper.

Equations

• KaltonRoberts.α₂ = 47 / 625

def KaltonRoberts.τ₁ : ℚ

The mixing parameter τ₁ from Equation (10) in Section 5 of the companion paper. Satisfies (1 − τ₁) q₀³ + τ₁ q₀⁴ = α₁.

Equations

• KaltonRoberts.τ₁ = (KaltonRoberts.q₀ ^ 3 - KaltonRoberts.α₁) / (KaltonRoberts.q₀ ^ 3 - KaltonRoberts.q₀ ^ 4)

def KaltonRoberts.τ₂ : ℚ

The mixing parameter τ₂ from Equation (10) in Section 5 of the companion paper. Satisfies (1 − τ₂) p₀⁴ + τ₂ p₀⁵ = α₂.

Equations

• KaltonRoberts.τ₂ = (KaltonRoberts.p₀ ^ 4 - KaltonRoberts.α₂) / (KaltonRoberts.p₀ ^ 4 - KaltonRoberts.p₀ ^ 5)

def KaltonRoberts.C₁ : ℚ

The Case 1 bound C₁ from Equation (14) in Section 5 of the companion paper.

Equations

• KaltonRoberts.C₁ = 23662339508853784054849 / 1192830849380162250000

def KaltonRoberts.C₂ : ℚ

The Case 2 bound C₂, which is the final headline constant, from Equation (17) in Section 5 of the companion paper.

Equations

• KaltonRoberts.C₂ = 694198146664396294486127753 / 34994834677886019996000000

def KaltonRoberts.krUpper : ℚ

The simplified upper bound 9919/500 = 19.838, from the statement of Theorem 1.1 in Section 1 of the companion paper.

Equations

• KaltonRoberts.krUpper = 9919 / 500

Dual certificate structure (Section 2)

structure KaltonRoberts.DualCertificate {U : Type u_1} [DecidableEq U] [Fintype U] (f : Finset U → ℝ) (M : ℝ) : Type u_1

A dual certificate λ for best ℓ∞-approximation. Reference: Lemma 2.1 in Section 2 of the companion paper.

• lam : Finset U → ℝ

  The signed measure λ on 2^U.

• norm_one : ∑ S : Finset U, |self.lam S| = 1

  (i) ‖λ‖₁ = 1.

• zero_marginals (i : U) : {S : Finset U | i ∈ S}.sum self.lam = 0

  (ii) Zero item marginals: ∑_{A ∋ i} λ_A = 0 for all i ∈ U.

• pos_support (S : Finset U) : 0 < self.lam S → f S = M

  (iii) λ_A > 0 only when f(A) = M.

• neg_support (S : Finset U) : self.lam S < 0 → f S = -M

  (iii) λ_A < 0 only when f(A) = −M.