The distance rate of the Navascués–Wolfe hierarchy

The theorem rate_triangle proves the binary-triangle bound with coefficient 1 - (1 - 1/n)³ by separating copied-triangle pairs according to shared source indices. This is weaker than the coefficient 1/n in manuscript Corollary 6.1 (prop:promised, eq:nw-rate) at revision 2aa1f05ce932fdeef3896c83d287abd77cd8befb. ConvexOrder.rate_triangle_sharp proves the latter estimate for the binary triangle.

Both statements produce a compatible law at the asserted squared Euclidean distance. The general correlation-scenario result and the rejecting-order bounds expressed using the infimum distance to the compatible set are beyond the scope of this module.

def TriangleInflation.sqNorm (w : ThreeBit → ℝ) : ℝ

The squared Euclidean norm of a weight function on three bits.

Equations

• TriangleInflation.sqNorm w = ∑ x : TriangleInflation.ThreeBit, w x ^ 2

Auxiliary facts

The proof of rate_triangle uses a collision-counting estimate with three source types. The facts it needs about product laws, about the symmetry group of the inflation, and about the empirical law of a random copied triangle are not stated in the imported files, so they are proved here privately.

Marginals of a product law

theorem TriangleInflation.sum_ind_eq (a b : ThreeBit) : (∑ c : ThreeBit, (if a = c then 1 else 0) * if b = c then 1 else 0) = if a = b then 1 else 0

Two indicators of a common value multiply to the indicator of agreement.

The symmetry group of the inflation

theorem TriangleInflation.sym_sum {t : ℕ} {Γ : Assign t → ℝ} (hsym : SymmetricLaw t Γ) (π : Equiv.Perm (Fin t) × Equiv.Perm (Fin t) × Equiv.Perm (Fin t)) (F : Assign t → ℝ) : ∑ ω : Assign t, Γ ω * F (relabel π ω) = ∑ ω : Assign t, Γ ω * F ω

The defining invariance of a symmetric law, applied inside an expectation.

The law of one and of two copied triangles

theorem TriangleInflation.marg_two {n : ℕ} {P : ThreeBit → ℝ} (hP : IsLaw P) {Γ : Assign n → ℝ} (hsym : SymmetricLaw n Γ) (hdiag : pushforward Γ readDiagonal = tensorPow n P) {i j k i' j' k' : Fin n} (hi : i ≠ i') (hj : j ≠ j') (hk : k ≠ k') : (∑ ω : Assign n, Γ ω * if readTriangle i j k ω = readTriangle i' j' k' ω then 1 else 0) = sqNorm P

Two copied triangles sharing no copy index have the joint law P ⊗ P, so they agree with probability ‖P‖₂².

The empirical law of a random copied triangle

def TriangleInflation.triCount {n : ℕ} (ω : Assign n) (w : ThreeBit) : ℝ

The number of copied triangles that a deterministic assignment reads as w.

Equations

• TriangleInflation.triCount ω w = ∑ c : TriangleInflation.Cell n, if TriangleInflation.readTriangle c.1 c.2.1 c.2.2 ω = w then 1 else 0

noncomputable def TriangleInflation.qLaw (n : ℕ) (ω : Assign n) : ThreeBit → ℝ

The empirical law of the n³ copied triangles of a deterministic assignment: sample the three copy indices uniformly and independently, and output the three bits that the assignment gives to the corresponding copied triangle. This is the law q_ω of the proof of paper Corollary 6.1.

Equations

• TriangleInflation.qLaw n ω w = TriangleInflation.triCount ω w / ↑n ^ 3

theorem TriangleInflation.qLaw_isLaw {n : ℕ} (hn : 1 ≤ n) (ω : Assign n) : IsLaw (qLaw n ω)

theorem TriangleInflation.qLaw_compatible {n : ℕ} (hn : 1 ≤ n) (ω : Assign n) : TriangleCompatible (qLaw n ω)

Counting the pairs of copied triangles

theorem TriangleInflation.sum_ne_pair (n : ℕ) : (∑ x : Fin n × Fin n, if x.1 ≠ x.2 then 1 else 0) = ↑n ^ 2 - ↑n

The number of ordered pairs of distinct copy indices.

The two expectation identities

theorem TriangleInflation.expect_qLaw {n : ℕ} (hn : 1 ≤ n) {P : ThreeBit → ℝ} (hP : IsLaw P) {Γ : Assign n → ℝ} (hsym : SymmetricLaw n Γ) (hdiag : pushforward Γ readDiagonal = tensorPow n P) (w : ThreeBit) : ∑ ω : Assign n, Γ ω * qLaw n ω w = P w

The empirical law of a random copied triangle has mean P.

theorem TriangleInflation.exists_le_of_weighted {α : Type u_1} [Fintype α] {Γ : α → ℝ} (h0 : ∀ (a : α), 0 ≤ Γ a) (h1 : ∑ a : α, Γ a = 1) (v : α → ℝ) (c : ℝ) (hle : ∑ a : α, Γ a * v a ≤ c) : ∃ (a : α), v a ≤ c

A weighted average is at least the minimum over the support.

The distance rate

theorem TriangleInflation.rate_triangle (n : ℕ) (hn : 1 ≤ n) {P : ThreeBit → ℝ} (hP : IsLaw P) (h : NWFeasible n P) : ∃ (Qc : ThreeBit → ℝ), IsLaw Qc ∧ TriangleCompatible Qc ∧ (sqNorm fun (x : ThreeBit) => P x - Qc x) ≤ (1 - (1 - 1 / ↑n) ^ 3) * (1 - sqNorm P)

A collision-counting distance bound for the binary triangle: if P is feasible at order n, some triangle-compatible law Qc satisfies ‖P - Qc‖₂² ≤ [1 - (1 - 1/n)³] (1 - ‖P‖₂²). The sharper coefficient 1/n of manuscript Corollary 6.1 is proved in rate_triangle_sharp in ConvexOrder.lean.