Key lemmas from the Kalton-Roberts paper

Mathematical lemmas from Sections 1-4 of the companion paper.

Lemma 1.2: Finite reduction (Kalton–Roberts compact reduction)

noncomputable def KaltonRoberts.finiteBoolOrderIso (α : Type u_1) [BooleanAlgebra α] [Fintype α] : Finset { a : α // IsAtom a } ≃o α

A finite Boolean algebra is order-isomorphic to the powerset of its atoms, represented as Finset {a // IsAtom a}.

Equations

• KaltonRoberts.finiteBoolOrderIso α = Fintype.finsetOrderIsoSet.trans CompleteAtomicBooleanAlgebra.toSetOfIsAtom.symm

theorem KaltonRoberts.finite_boolean_algebra_bound_of_powerset (C : ℝ) (hfin : ∀ (U : Type u) [Fintype U] [inst : DecidableEq U] (f : Finset U → ℝ), IsApproxAdditive f 1 → ∃ (a : U → ℝ), ∀ (S : Finset U), |f S - additiveFunction a S| ≤ C) (α : Type u) [BooleanAlgebra α] [Finite α] (f : α → ℝ) (hf : IsApproxAdditiveBA f 1) : ∃ (μ : α → ℝ), IsFinitelyAdditiveBA μ ∧ ∀ (A : α), |f A - μ A| ≤ C

Transfer the finite powerset theorem to an arbitrary finite Boolean algebra.

theorem KaltonRoberts.booleanSubalgebra_closure_finite_of_finite {α : Type u_1} [BooleanAlgebra α] {s : Set α} (hs : s.Finite) : (↑(BooleanSubalgebra.closure s)).Finite

The Boolean subalgebra generated by a finite set is finite.

def KaltonRoberts.ApproxCoord {α : Type u_1} (f : α → ℝ) (C : ℝ) (A : α) : Set ℝ

Coordinate interval used in the compactness reduction.

Equations

• KaltonRoberts.ApproxCoord f C A = Set.Icc (f A - C) (f A + C)

@[reducible, inline]

abbrev KaltonRoberts.ApproxProduct {α : Type u_1} (f : α → ℝ) (C : ℝ) : Type u_1

Product of all coordinate intervals [f(A)-C, f(A)+C].

Equations

• KaltonRoberts.ApproxProduct f C = ((A : α) → ↑(KaltonRoberts.ApproxCoord f C A))

def KaltonRoberts.AddIdx (α : Type u_1) [BooleanAlgebra α] : Type u_1

Index type for finite-additivity equations.

Equations

• KaltonRoberts.AddIdx α = { p : α × α // Disjoint p.1 p.2 }

def KaltonRoberts.addCondition {α : Type u_1} [BooleanAlgebra α] (f : α → ℝ) (C : ℝ) (i : AddIdx α) : Set (ApproxProduct f C)

Closed additivity condition ν(A ⊔ B) = ν(A) + ν(B) inside the interval product.

Equations

• KaltonRoberts.addCondition f C i = {x : KaltonRoberts.ApproxProduct f C | ↑(x ((↑i).1 ⊔ (↑i).2)) = ↑(x (↑i).1) + ↑(x (↑i).2)}

theorem KaltonRoberts.compact_reduction_from_local {α : Type u_1} [BooleanAlgebra α] (C : ℝ) (hC : 0 ≤ C) (f : α → ℝ) (hlocal : ∀ (T : Finset α), ∃ (ν : α → ℝ), (∀ A ∈ T, |f A - ν A| ≤ C) ∧ ∀ A ∈ T, ∀ B ∈ T, Disjoint A B → A ⊔ B ∈ T → ν (A ⊔ B) = ν A + ν B) : ∃ (μ : α → ℝ), IsFinitelyAdditiveBA μ ∧ ∀ (A : α), |f A - μ A| ≤ C

Compactness/FIP step in the Kalton--Roberts finite reduction.

If every finite set of coordinates admits values in the intervals satisfying all additivity equations involving those coordinates, then a global finitely additive measure exists.

theorem KaltonRoberts.local_approximation_of_finite_boolean_algebras {α : Type u} [BooleanAlgebra α] (C : ℝ) (hfiniteBA : ∀ (β : Type u) [inst : BooleanAlgebra β] [Fintype β] (g : β → ℝ), IsApproxAdditiveBA g 1 → ∃ (μ : β → ℝ), IsFinitelyAdditiveBA μ ∧ ∀ (B : β), |g B - μ B| ≤ C) (f : α → ℝ) (hf : IsApproxAdditiveBA f 1) (T : Finset α) : ∃ (ν : α → ℝ), (∀ A ∈ T, |f A - ν A| ≤ C) ∧ ∀ A ∈ T, ∀ B ∈ T, Disjoint A B → A ⊔ B ∈ T → ν (A ⊔ B) = ν A + ν B

Finite satisfiability for the compactness reduction, obtained from the finite Boolean algebra theorem on the subalgebra generated by the requested coordinates.

theorem KaltonRoberts.finite_reduction (C : ℝ) (hC : 0 ≤ C) (hfin : ∀ (U : Type u) [Fintype U] [inst : DecidableEq U] (f : Finset U → ℝ), IsApproxAdditive f 1 → ∃ (a : U → ℝ), ∀ (S : Finset U), |f S - additiveFunction a S| ≤ C) (α : Type u) [BooleanAlgebra α] (f : α → ℝ) : IsApproxAdditiveBA f 1 → ∃ (μ : α → ℝ), IsFinitelyAdditiveBA μ ∧ ∀ (A : α), |f A - μ A| ≤ C

Lemma 1.2 (Kalton--Roberts compact reduction). If the main theorem holds for every finite power-set algebra 2^U with constant C, then it holds with the same constant for every Boolean algebra, hence for every set algebra.

The proof formalizes the compact product/FIP argument from the paper and the standard reduction from finite Boolean algebras to powersets of atoms.

Reference: Lemma 1.2 in Section 1 of the companion paper.

Lemma 2.1: Dual certificate

theorem KaltonRoberts.dual_certificate_exists {U : Type u_1} [DecidableEq U] [Fintype U] (f : Finset U → ℝ) (_hf : IsApproxAdditive f 1) (_hM : ∀ (S : Finset U), |f S| ≤ distToAdditive f) (_hbest : ∀ (a : U → ℝ), ∃ (S : Finset U), |f S - additiveFunction a S| ≥ distToAdditive f) : Nonempty (DualCertificate f (distToAdditive f))

Lemma 2.1 (Dual certificate). Let f : 2^U → ℝ be 1-additive. After subtracting a closest additive signed measure, there exists a rational dual certificate λ satisfying conditions (i)–(iii).

The proof uses the finite-dimensional Hahn–Banach criterion for best ℓ∞-approximation. The rationality follows from the polytope vertex argument.

Reference: Lemma 2.1 in Section 2 of the companion paper.

Lemma 2.4: Approximate modularity

theorem KaltonRoberts.approx_modularity {U : Type u_1} [DecidableEq U] (f : Finset U → ℝ) (hf : IsApproxAdditive f 1) (A B : Finset U) : |f A + f B - f (A ∪ B) - f (A ∩ B)| ≤ 2

theorem KaltonRoberts.deficit_intersection {U : Type u_1} [DecidableEq U] (f : Finset U → ℝ) (hf : IsApproxAdditive f 1) (M : ℝ) (hM : ∀ (S : Finset U), |f S| ≤ M) (A B : Finset U) (a b : ℝ) (hA : f A = M - a) (hB : f B = M - b) : f (A ∩ B) ≥ M - a - b - 2

Corollary 3.1: Mixed neighbouring intersections

theorem KaltonRoberts.mixed_intersection_frequency_mono (t₁ t₂ : ℝ) (_ht : 0 ≤ t₁) (_ht12 : t₁ ≤ t₂) (_ht2 : t₂ ≤ 1) (ℓ : ℕ) (τ : ℝ) (_hτ : 0 ≤ τ) (_hτ1 : τ ≤ 1) : (1 - τ) * t₁ ^ ℓ + τ * t₁ ^ (ℓ + 1) ≤ (1 - τ) * t₂ ^ ℓ + τ * t₂ ^ (ℓ + 1)

theorem KaltonRoberts.mixed_intersection_deficit_bound (E : ℝ) (hE : 0 ≤ E) (ℓ : ℕ) (hℓ : 1 ≤ ℓ) (τ : ℝ) (hτ : 0 ≤ τ) : ↑ℓ * E + 2 * (↑ℓ - 1) + τ * (E + 2) ≥ 0

Corollary 3.1, deficit bound (nonnegativity only).

NOTE: This only proves that the expression ℓ E + 2(ℓ − 1) + τ(E + 2) ≥ 0. This is NOT the actual Corollary 3.1 mixed-intersection theorem, which asserts that the average deficit of the constructed mixed intersection collection is at most this expression.

The honest construction-based version is mixed_intersection_weighted in Pipeline.lean.

Reference: Corollary 3.1 in Section 3 of the companion paper.

Lemma 3.2: One-sided recombination

theorem KaltonRoberts.one_sided_recombination_ineq (θ M D D' r : ℝ) (_hθ : 0 < θ) (hθ1 : θ < 1) (hrec : (1 - θ) * M ≤ D - θ * D' + 2 * r - 1 - θ) : M ≤ (D + 2 * r - 1 - θ) / (1 - θ) - θ / (1 - θ) * D'

Lemma 3.2 (One-sided recombination, algebraic consequence).

NOTE: This is only the algebraic manipulation from the recombination inequality hrec, not the full combinatorial Lemma 3.2. The construction used by the final theorem is one_sided_recombination_core_eps in EpsilonRecombination.lean.

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

theorem KaltonRoberts.one_sided_recombination_discard (θ M D D' r : ℝ) (_hθ : 0 < θ) (hθ1 : θ < 1) (hD' : 0 ≤ D') (hrec : (1 - θ) * M ≤ D - θ * D' + 2 * r - 1 - θ) : M ≤ (D + 2 * r - 1 - θ) / (1 - θ)

Equation (5) in Lemma 3.2: discarding the target deficit gives M ≤ (D + 2r − 1 − θ)/(1 − θ).

Reference: Equation (5) in Lemma 3.2 of the companion paper.

Lemma 3.3: Two-sided recombination

theorem KaltonRoberts.two_sided_recombination (_α r θ M D S D' S' : ℝ) (_hθ : 0 < θ) (_hθ1 : θ < 1) (h_pos : (1 - θ) * M ≤ D - θ * D' + 2 * r - 1 - θ) (h_neg : (1 - θ) * M ≤ S - θ * S' + 2 * r - 1 - θ) : (1 - θ) * M ≤ (D + S) / 2 - θ * (D' + S') / 2 + 2 * r - 1 - θ

Lemma 3.3 (Two-sided recombination, algebraic consequence).

NOTE: This is only the algebraic averaging of two one-sided inequalities, not the full combinatorial Lemma 3.3. The construction used by the final theorem is two_sided_recombination_core_eps in EpsilonRecombination.lean.

Reference: Lemma 3.3 (Equation (6)) in Section 3 of the companion paper.