Finite-order fan inequalities

Statements for paper Section 5.4: Theorem 5.11 (thm:fan) with its pointwise certificate (eq:fan-pointwise) and rejecting-order corollary (eq:fan-order), and Proposition 5.12 (prop:Rp). Proofs are deferred.

def TriangleInflation.ind (b : Bool) : ℕ

The indicator value of a Boolean, as a natural number.

Equations

• TriangleInflation.ind b = if b = true then 1 else 0

Arithmetic helpers for the pointwise certificate

theorem TriangleInflation.fan_pointwise (t : ℕ) (a : Bool) (b c : Fin t → Bool) : 2 * ∑ k : Fin t, ind a * ind (b k) * ind (c k) ≤ 2 * ind a + ∑ k : Fin t, ∑ l : Fin t, if k = l then 0 else ind (b k) * ind (c l)

Paper equation (eq:fan-pointwise), multiplied by two to stay inside ℕ: for every deterministic assignment of the fan {A^{11}} ∪ {B^{1k}, C^{1k} : k ∈ [t]}, with a = 𝟙[A^{11} = 0], b k = 𝟙[B^{1k} = 0], c k = 𝟙[C^{1k} = 0], ∑_k a b_k c_k ≤ a + ½ ∑_{k ≠ l} b_k c_l.

Real-valued indicators

Elementary expectation calculus

Transport along the symmetry group

Marginals of the tensor power

The fan expectations

The abstract fan inequalities

The three rootings

theorem TriangleInflation.fan_first (t : ℕ) (ht : 1 ≤ t) {P : ThreeBit → ℝ} (hP : IsLaw P) (h : NWFeasible t P) : ↑t * atom000 P ≤ margA P + ↑(t.choose 2) * (margB P * margC P)

Paper Theorem 5.11 (thm:fan), first inequality: if P ∈ I^NW_t then t z ≤ a + C(t,2) b c, where a = P_A(0), b = P_B(0), c = P_C(0), z = P(000).

theorem TriangleInflation.fan_second (t : ℕ) (ht : 1 ≤ t) {P : ThreeBit → ℝ} (hP : IsLaw P) (h : NWFeasible t P) : ↑t * (atom000 P ^ 2 - margA P * margB P * margC P) ≤ margA P * atom000 P - margA P * margB P * margC P

Paper Theorem 5.11 (thm:fan), second inequality: if P ∈ I^NW_t then t (z² - abc) ≤ az - abc.

theorem TriangleInflation.tminNW_le_of_finner_violation {P : ThreeBit → ℝ} (hP : IsLaw P) (hv : margA P * margB P * margC P < atom000 P ^ 2) : tminNW P ≤ ⌊(atom000 P * min (margA P) (min (margB P) (margC P)) - margA P * margB P * margC P) / (atom000 P ^ 2 - margA P * margB P * margC P)⌋₊ + 1

Paper Theorem 5.11 (thm:fan), rejecting-order corollary (eq:fan-order): a Finner violation z² > abc gives the explicit first rejecting order t_min^NW(P) ≤ ⌊(z min{a,b,c} - abc)/(z² - abc)⌋ + 1.

The floor is Nat.floor; the paper's ratio is at least 1, so the two agree.

theorem TriangleInflation.tminAI_le_of_finner_violation {P : ThreeBit → ℝ} (hP : IsLaw P) (hv : margA P * margB P * margC P < atom000 P ^ 2) : tminAI P ≤ ⌊(atom000 P * min (margA P) (min (margB P) (margC P)) - margA P * margB P * margC P) / (atom000 P ^ 2 - margA P * margB P * margC P)⌋₊ + 1

Paper Theorem 5.11 (thm:fan), rejecting-order corollary for the ancestral-independence hierarchy: the smaller feasible sets reject no later.

Proposition 5.12: no uniformly divergent distance lower bound

theorem TriangleInflation.nwFeasible_one {P : ThreeBit → ℝ} (hP : IsLaw P) : NWFeasible 1 P

Paper Proposition 5.12 (prop:Rp): order one is passed by every law.

theorem TriangleInflation.aiFeasible_one {P : ThreeBit → ℝ} (hP : IsLaw P) : AIFeasible 1 P

Order one is passed by every law for the ancestral-independence hierarchy as well.

theorem TriangleInflation.Rlaw_not_nwFeasible_two {p : ℝ} (h0 : 0 < p) (h1 : p < 1) : ¬NWFeasible 2 (Rlaw p)

theorem TriangleInflation.Rlaw_tminNW {p : ℝ} (h0 : 0 < p) (h1 : p < 1) : tminNW (Rlaw p) = 2

Paper Proposition 5.12 (prop:Rp): t_min^NW(R_p) = 2 for every 0 < p < 1, while R_p → δ_{111} ∈ C_tri as p ↓ 0. Hence no lower bound of the form t_min^H(P) ≥ c d_TV(P, C_tri)^{-α} can hold for all incompatible P.

theorem TriangleInflation.Rlaw_tminAI {p : ℝ} (h0 : 0 < p) (h1 : p < 1) : tminAI (Rlaw p) = 2

Paper Proposition 5.12 (prop:Rp) for the ancestral-independence hierarchy.