ShortcodeFiberConditioning.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.UniqueGamesTheorem.Inverse.ShortcodeFromGrassmann.uniform_pair_mixture line 18

Source documentation

Exact decomposition of a uniform two-factor law with a self-loop on either zero factor. No nonemptiness is required of the nonzero subtypes.

theorem uniform_pair_mixture {A B : Type*} [Fintype A] [Fintype B]
    [Zero A] [Zero B] (h : A → B → ℝ)
    (hleft : ∀ b, h 0 b = 1) (hright : ∀ a, h a 0 = 1) :
    (𝔼 a, 𝔼 b, h a b) =
      (Fintype.card A : ℝ)⁻¹ + (Fintype.card B : ℝ)⁻¹ -
        (Fintype.card A : ℝ)⁻¹ * (Fintype.card B : ℝ)⁻¹ +
      (1 - ((Fintype.card A : ℝ)⁻¹ + (Fintype.card B : ℝ)⁻¹ -
        (Fintype.card A : ℝ)⁻¹ * (Fintype.card B : ℝ)⁻¹)) *
        (𝔼 p : {a : A // a ≠ 0} × {b : B // b ≠ 0}, h p.1.val p.2.val) := by
…

theorem OAI.UniqueGamesTheorem.Inverse.ShortcodeFromGrassmann.vector_card_real line 90
theorem OAI.UniqueGamesTheorem.Inverse.ShortcodeFromGrassmann.binary_zero_mass_nonneg line 94

theorem OAI.UniqueGamesTheorem.Inverse.ShortcodeFromGrassmann.conditioned_output_fiber line 108

Source documentation

The actual equality test has a nonempty output fiber retaining at least η/2 after both factors are conditioned to be nonzero. The displayed order samples a uniform matrix in that fiber first, as required by the Grassmann neighbor correspondence.

theorem conditioned_output_fiber {ell m : ℕ}
    (f : Mat ell m → Vector ell) {η : ℝ} (hη : 0 < η) (hη1 : η < 1)
    (hzero : ((2 : ℝ) ^ ell)⁻¹ + ((2 : ℝ) ^ m)⁻¹ -
      ((2 : ℝ) ^ (ell + m))⁻¹ ≤ η / 2)
    (haccept : η ≤ equalityAcceptance f) :
    ∃ y, (matrixFiber f y).Nonempty ∧
      η / 2 ≤ (matrixFiber f y).expect (fun M =>
        𝔼 p : {a : Vector ell // a ≠ 0} × {l : Vector m // l ≠ 0},
          if f (M + rankOne p.1.val p.2.val) = y then (1 : ℝ) else 0) := by
…

Mentions: OAI.UniqueGamesTheorem.Inverse.ShortcodeFromGrassmann.matrixFiber