PositiveMultiplier.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.MaxCutGames.Decoder.PositiveMultiplier.retained_mass_of_acceptance line 22

Source documentation

A 7/8 bound outside the retained set forces at least 0.92 retained mass when acceptance is at least 0.99. The statement keeps the exact rational constants, rather than assuming a low-rank mass premise.

theorem retained_mass_of_acceptance
    (w : J → ℝ) (a lam : (j : J) → I j → ℝ)
    (keep : (j : J) → I j → Prop)
    (hw : ∀ j, 0 ≤ w j) (htotal : energy w a = 1)
    (hone : ∀ j i, lam j i ≤ 1)
    (hhigh : ∀ j i, ¬ keep j i → lam j i ≤ 7 / 8)
    (haccept : (99 : ℝ) / 100 ≤ spectralEnergy w lam a) :
    (23 : ℝ) / 25 ≤ cutoffEnergy w keep a := by
…

theorem OAI.MaxCutGames.Decoder.PositiveMultiplier.positive_multiplier_comparison line 59

theorem OAI.MaxCutGames.Decoder.PositiveMultiplier.good_fiber_mass line 94

Source documentation

A finite probability law with mean at least 14.4 η assigns mass at least 10 η to acceptances at least 4 η.

theorem good_fiber_mass
    {Q : Type*} [Fintype Q] (μ p : Q → ℝ) (η : ℝ)
    (hμ : ∀ q, 0 ≤ μ q) (hμsum : ∑ q, μ q = 1)
    (hη : 0 ≤ η) (hp : ∀ q, p q ≤ 1)
    (hmean : (72 : ℝ) / 5 * η ≤ ∑ q, μ q * p q) :
    10 * η ≤ ∑ q, μ q * if 4 * η ≤ p q then 1 else 0 := by
…

def OAI.MaxCutGames.Decoder.PositiveMultiplier.equalityAcceptance line 126
Source documentation
The actual equality test, including zero perturbation factors.
```
def equalityAcceptance (ν : V → ℝ) (label : (E →ₗ[F2] V) → C) : ℝ := by
…
```
theorem OAI.MaxCutGames.Decoder.PositiveMultiplier.color_pair_sum line 132
theorem OAI.MaxCutGames.Decoder.PositiveMultiplier.equalityAcceptance_fourier line 142
Source documentation
Equality acceptance has the actual positive Fourier multiplier. Color indicators give the same equality expansion as output characters, with no extra factor depending on the output alphabet.
```
theorem equalityAcceptance_fourier (ν : V → ℝ)
    (label : (E →ₗ[F2] V) → C) :
    equalityAcceptance ν label =
      ∑ c, ∑ S : V →ₗ[F2] E,
        linearNoiseEigenvalue ν S * linearCoeff (colorIndicator label c) S ^ 2 := by
…
```
Mentions: OAI.MaxCutGames.Decoder.PositiveMultiplier.equalityAcceptance

theorem OAI.MaxCutGames.Decoder.PositiveMultiplier.matrix_test_comparison line 173

Source documentation

Spectral comparison applied to a genuine family of matrix labelings. The two explicit probability laws may be the latent gadget law and uniform sampling in the distinguished subspace, respectively.

theorem matrix_test_comparison
    (μ : Q → ℝ) (ν ρ : V → ℝ)
    (label : Q → (E →ₗ[F2] V) → C)
    (keep : (V →ₗ[F2] E) → Prop) (t : ℝ)
    (hμ : ∀ q, 0 ≤ μ q) (hμsum : ∑ q, μ q = 1)
    (hν : ∀ v, 0 ≤ ν v) (hνsum : ∑ v, ν v = 1)
    (hρ : ∀ v, 0 ≤ ρ v) (ht : 0 ≤ t)
    (hhigh : ∀ S : V →ₗ[F2] E, ¬ keep S → linearNoiseEigenvalue ν S ≤ 7 / 8)
    (hlow : ∀ S : V →ₗ[F2] E, keep S → t ≤ linearNoiseEigenvalue ρ S)
    (haccept : (99 : ℝ) / 100 ≤ ∑ q, μ q * equalityAcceptance ν (label q)) :
    (9 : ℝ) / 10 * t ≤ ∑ q, μ q * equalityAcceptance ρ (label q) := by
…

Mentions: OAI.MaxCutGames.Decoder.PositiveMultiplier.equalityAcceptance

def OAI.MaxCutGames.Decoder.PositiveMultiplier.subspaceLaw line 216
Source documentation
Pushforward of uniform sampling in K. For a subspace inclusion this is uniform sampling in that subspace; the definition also permits a linear map with nontrivial fibers without accidentally conditioning on nonzero vectors.
```
def subspaceLaw (ι : K →ₗ[F2] V) (v : V) : ℝ := by
…
```
theorem OAI.MaxCutGames.Decoder.PositiveMultiplier.subspaceLaw_nonneg line 221
theorem OAI.MaxCutGames.Decoder.PositiveMultiplier.subspaceLaw_sum line 230
theorem OAI.MaxCutGames.Decoder.PositiveMultiplier.subspaceLaw_normalized line 240
theorem OAI.MaxCutGames.Decoder.PositiveMultiplier.subspaceLaw_eigenvalue line 245
theorem OAI.MaxCutGames.Decoder.PositiveMultiplier.subspaceLaw_eigenvalue_lower line 272
theorem OAI.MaxCutGames.Decoder.PositiveMultiplier.matrix_spectral_comparison line 288