FiniteNoise.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Realizing the existing Håstad noise law with a finite uniform tape

A tape contains one element of Fin D per coordinate. The corresponding noise bit is true exactly when that element has value zero. For D > 0, its law is exactly Foundations.Hastad.noiseWeight ((D : ℝ)⁻¹).

The construction also permits an empty coordinate type and D = 1.

def OAI.MaxCutGames.Reduction.FiniteNoise.realizedBit line 21
def OAI.MaxCutGames.Reduction.FiniteNoise.realizedNoise line 23
theorem OAI.MaxCutGames.Reduction.FiniteNoise.realizedBit_eq_true_iff line 26
theorem OAI.MaxCutGames.Reduction.FiniteNoise.coordinate_fiber_sum line 31
Source documentation
The two fibers of a coordinate have their actual normalized finite counts.
```
theorem coordinate_fiber_sum {D : Nat} (positive : 0 < D) (b : Bool) :
    (∑ z : Fin D, if realizedBit z = b then (D : ℝ)⁻¹ else 0) =
      if b then (D : ℝ)⁻¹ else 1 - (D : ℝ)⁻¹ := by
…
```
Mentions: OAI.MaxCutGames.Reduction.FiniteNoise.realizedBit
theorem OAI.MaxCutGames.Reduction.FiniteNoise.noiseWeight_eq_fiber_sum line 56
Source documentation
Product distributivity computes the mass of every complete Boolean noise vector.
```
theorem noiseWeight_eq_fiber_sum {D : Nat} (positive : 0 < D) (μ : A → Bool) :
    noiseWeight ((D : ℝ)⁻¹) μ =
      ∑ z : A → Fin D,
        ∏ a, if realizedBit (z a) = μ a then (D : ℝ)⁻¹ else 0 := by
…
```
Mentions: OAI.MaxCutGames.Reduction.FiniteNoise.realizedBit
theorem OAI.MaxCutGames.Reduction.FiniteNoise.fiber_product_eq_indicator line 68
theorem OAI.MaxCutGames.Reduction.FiniteNoise.expect_realizedNoise line 82
Source documentation
Exact pushforward law for every observable, using the existing noise weight.
```
theorem expect_realizedNoise {D : Nat} (positive : 0 < D) (H : (A → Bool) → ℝ) :
    (𝔼 z : A → Fin D, H (realizedNoise z)) =
      ∑ μ : A → Bool, noiseWeight ((D : ℝ)⁻¹) μ * H μ := by
…
```
Mentions: OAI.MaxCutGames.Reduction.FiniteNoise.realizedNoise