Sign estimates from conditional uniformity

A balanced Boolean observation has zero mean on a uniform output. Any bounded statistic of the retained tag can multiply its sign without changing that cancellation. The remaining error is bounded by the finite absolute sum defining twice total variation. No positivity or normalization of the original weights is needed for this calculation.

theorem Algebraic.Cutwidth.Extractor.Internal.weightSign_mul_le_dist {Tag : Type u_1} {Out : Type u_2} [Fintype Tag] [Fintype Out] (p : Tag × Out → ℝ) (bit : Out → Bool) (balanced : mapWeight bit (uniformWeight Out) = uniformWeight Bool) (mask : Tag → ℝ) (bound : ∀ (tag : Tag), |mask tag| ≤ 1) : |∑ z : Tag × Out, p z * ((if bit z.2 = true then 1 else -1) * mask z.1)| ≤ 2 * weightDist p (uniformSecondWeight p)

theorem Algebraic.Cutwidth.Extractor.Internal.weightSign_xor_le_dist {Tag : Type u_1} {Out : Type u_2} [Fintype Tag] [Fintype Out] (p : Tag × Out → ℝ) (bit : Out → Bool) (balanced : mapWeight bit (uniformWeight Out) = uniformWeight Bool) (mask : Tag → Bool) : |∑ z : Tag × Out, p z * if (bit z.2 ^^ mask z.1) = true then 1 else -1| ≤ 2 * weightDist p (uniformSecondWeight p)

theorem Algebraic.Cutwidth.Extractor.Internal.mapWeight_uniform_bool_coordinate {M : ℕ} (j : Fin M) : mapWeight (fun (x : Fin M → Bool) => x j) (uniformWeight (Fin M → Bool)) = uniformWeight Bool

theorem Algebraic.Cutwidth.Extractor.Internal.affineLeakage_sign_mul_le_of_not_mem_badSeeds {n d t : ℕ} {Out : Type u_1} [Fintype Out] (cb : (Fin n → Bool) → (Fin d → Bool) → List Bool → Out) (p : (Fin n → Bool) → ℝ) (leak : (Fin n → Bool) → Option (Fin t) → Fin d → Bool) (advice : Option (Fin t) → List Bool) (γ : ℝ) (y : Fin d → Bool) (good : y ∉ affineLeakageBadSeeds cb p leak advice γ) (b : Fin n → Bool) (ys : Fin t → Fin d → Bool) (bit : Out → Bool) (balanced : mapWeight bit (uniformWeight Out) = uniformWeight Bool) (mask : (Fin t → Out) → ℝ) (bound : ∀ (outputs : Fin t → Out), |mask outputs| ≤ 1) : |∑ x : Fin n → Bool, p x * ((if bit (cb (xorInput x b) (xorInput y (leak x none)) (advice none)) = true then 1 else -1) * mask fun (i : Fin t) => cb (xorInput x b) (xorInput (ys i) (leak x (some i))) (advice (some i)))| ≤ 2 * γ

theorem Algebraic.Cutwidth.Extractor.Internal.affineLeakage_sign_le_of_not_mem_badSeeds {n d t : ℕ} {Out : Type u_1} [Fintype Out] (cb : (Fin n → Bool) → (Fin d → Bool) → List Bool → Out) (p : (Fin n → Bool) → ℝ) (leak : (Fin n → Bool) → Option (Fin t) → Fin d → Bool) (advice : Option (Fin t) → List Bool) (γ : ℝ) (y : Fin d → Bool) (good : y ∉ affineLeakageBadSeeds cb p leak advice γ) (b : Fin n → Bool) (ys : Fin t → Fin d → Bool) (bit : Out → Bool) (balanced : mapWeight bit (uniformWeight Out) = uniformWeight Bool) (mask : (Fin t → Out) → Bool) : |∑ x : Fin n → Bool, p x * if (bit (cb (xorInput x b) (xorInput y (leak x none)) (advice none)) ^^ mask fun (i : Fin t) => cb (xorInput x b) (xorInput (ys i) (leak x (some i))) (advice (some i))) = true then 1 else -1| ≤ 2 * γ

theorem Algebraic.Cutwidth.Extractor.Internal.affineLeakage_coordinate_sign_le_of_not_mem_badSeeds {n d t M : ℕ} (cb : (Fin n → Bool) → (Fin d → Bool) → List Bool → Fin M → Bool) (p : (Fin n → Bool) → ℝ) (leak : (Fin n → Bool) → Option (Fin t) → Fin d → Bool) (advice : Option (Fin t) → List Bool) (γ : ℝ) (y : Fin d → Bool) (good : y ∉ affineLeakageBadSeeds cb p leak advice γ) (b : Fin n → Bool) (ys : Fin t → Fin d → Bool) (j : Fin M) (mask : (Fin t → Fin M → Bool) → Bool) : |∑ x : Fin n → Bool, p x * if (cb (xorInput x b) (xorInput y (leak x none)) (advice none) j ^^ mask fun (i : Fin t) => cb (xorInput x b) (xorInput (ys i) (leak x (some i))) (advice (some i))) = true then 1 else -1| ≤ 2 * γ