OAI/Computability/UniqueGames/Analysis/MatrixRestrictions.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.UniqueGamesTheorem.Fourier.MatrixRestrictions.Ambient line 18
2. abbrev OAI.UniqueGamesTheorem.Fourier.MatrixRestrictions.Parameter line 22
3. def OAI.UniqueGamesTheorem.Fourier.MatrixRestrictions.embed line 26

   Source documentation

   The canonical inclusion of L(E/W,C') into L(E,C).

   def embed (W : Submodule F2 E)
       (C' : Submodule F2 C) (A : Parameter W C') : (E →ₗ[F2] C) :=
   …

   Mentions: OAI.UniqueGamesTheorem.Fourier.MatrixRestrictions.Parameter

4. theorem OAI.UniqueGamesTheorem.Fourier.MatrixRestrictions.embed_apply line 30
5. theorem OAI.UniqueGamesTheorem.Fourier.MatrixRestrictions.embed_injective line 34
6. theorem OAI.UniqueGamesTheorem.Fourier.MatrixRestrictions.embed_vanishes line 43
7. theorem OAI.UniqueGamesTheorem.Fourier.MatrixRestrictions.embed_range line 51
8. theorem OAI.UniqueGamesTheorem.Fourier.MatrixRestrictions.exists_embed_iff line 58

   Source documentation

   These are exactly the maps vanishing on W with image in C'.

   theorem exists_embed_iff (W : Submodule F2 E)
       (C' : Submodule F2 C) (B : (E →ₗ[F2] C)) :
       (∃ A : Parameter W C', embed W C' A = B) ↔
         W ≤ LinearMap.ker B ∧ LinearMap.range B ≤ C' := by
   …

   Mentions: OAI.UniqueGamesTheorem.Fourier.MatrixRestrictions.Parameter, OAI.UniqueGamesTheorem.Fourier.MatrixRestrictions.embed

9. theorem OAI.UniqueGamesTheorem.Fourier.MatrixRestrictions.quotient_embed_zero line 78

   Source documentation

   Quotient rows are unchanged by every admissible restriction perturbation.

   theorem quotient_embed_zero (W : Submodule F2 E)
       (C' : Submodule F2 C) (A : Parameter W C') :
       C'.mkQ.comp (embed W C' A) = 0 := by
   …

   Mentions: OAI.UniqueGamesTheorem.Fourier.MatrixRestrictions.Parameter, OAI.UniqueGamesTheorem.Fourier.MatrixRestrictions.embed

10. def OAI.UniqueGamesTheorem.Fourier.MatrixRestrictions.translate line 86
11. theorem OAI.UniqueGamesTheorem.Fourier.MatrixRestrictions.translate_injective line 90
12. theorem OAI.UniqueGamesTheorem.Fourier.MatrixRestrictions.quotient_translate line 96
13. def OAI.UniqueGamesTheorem.Fourier.MatrixRestrictions.embedding line 110

    Source documentation

    The perturbation inclusion is itself a binary linear map.

    def embedding (W : Submodule F2 E) (C' : Submodule F2 C) :
        Parameter W C' →ₗ[F2] (E →ₗ[F2] C) where
    …

    Mentions: OAI.UniqueGamesTheorem.Fourier.MatrixRestrictions.Parameter

14. def OAI.UniqueGamesTheorem.Fourier.MatrixRestrictions.order line 122
15. def OAI.UniqueGamesTheorem.Fourier.MatrixRestrictions.restrict line 126

    Source documentation

    Restrict a real observable to the actual affine quotient-map domain.

    def restrict (f : (E →ₗ[F2] C) → ℝ) (W : Submodule F2 E)
        (C' : Submodule F2 C) (X : E →ₗ[F2] C) : Parameter W C' → ℝ :=
    …

    Mentions: OAI.UniqueGamesTheorem.Fourier.MatrixRestrictions.Parameter

16. instance OAI.UniqueGamesTheorem.Fourier.MatrixRestrictions.parameterFintype line 130
17. theorem OAI.UniqueGamesTheorem.Fourier.MatrixRestrictions.parameter_card_pos line 139

    Source documentation

    Every actual restriction domain has at least its zero map.

    theorem parameter_card_pos [Finite E] [Finite C]
        (W : Submodule F2 E) (C' : Submodule F2 C) :
        0 < Fintype.card (Parameter W C') := Fintype.card_pos

    Mentions: OAI.UniqueGamesTheorem.Fourier.MatrixRestrictions.Parameter

18. structure OAI.UniqueGamesTheorem.Fourier.MatrixRestrictions.Row line 144

    Source documentation

    An actual row includes its target subspace as part of its index.

    structure Row (E C : Type*) [AddCommGroup E] [Module F2 E]
        [AddCommGroup C] [Module F2 C] where
    …

19. structure OAI.UniqueGamesTheorem.Fourier.MatrixRestrictions.Witness line 149
20. def OAI.UniqueGamesTheorem.Fourier.MatrixRestrictions.samples line 155
21. theorem OAI.UniqueGamesTheorem.Fourier.MatrixRestrictions.samples_length line 160
22. theorem OAI.UniqueGamesTheorem.Fourier.MatrixRestrictions.samples_nonempty line 164
23. theorem OAI.UniqueGamesTheorem.Fourier.MatrixRestrictions.mem_samples_iff line 171
24. theorem OAI.UniqueGamesTheorem.Fourier.MatrixRestrictions.samples_nodup line 178
25. def OAI.UniqueGamesTheorem.Fourier.MatrixRestrictions.system line 185

    Source documentation

    Actual affine matrix restrictions instantiate the generic deletion interface.

    noncomputable def system [Finite E] [Finite C] (r : Nat) :
        Deletion.RestrictionSystem (E →ₗ[F2] C) (Row E C) (Witness E C) where
    …

    Mentions: OAI.UniqueGamesTheorem.Fourier.Deletion.RestrictionSystem, OAI.UniqueGamesTheorem.Fourier.MatrixRestrictions.Row, OAI.UniqueGamesTheorem.Fourier.MatrixRestrictions.Witness

26. theorem OAI.UniqueGamesTheorem.Fourier.MatrixRestrictions.remainder_restriction_count line 198

    Source documentation

    Every actual affine restriction of order at most r obeys the residual count bound after whole-row deletion. No linear containment assumption remains.

    theorem remainder_restriction_count [Finite E] [Finite C]
        (H : (E →ₗ[F2] C) → Bool) (r p q : Nat) (t : Witness E C)
        (ht : order t.vanishing t.target ≤ r) :
        q * Deletion.trueCount (Deletion.remainder (system r) H p q) (samples t) ≤
          p * Fintype.card (Parameter t.vanishing t.target) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Fourier.MatrixRestrictions.Witness, OAI.UniqueGamesTheorem.Fourier.MatrixRestrictions.order, OAI.UniqueGamesTheorem.Fourier.Deletion.trueCount, OAI.UniqueGamesTheorem.Fourier.Deletion.remainder, OAI.UniqueGamesTheorem.Fourier.MatrixRestrictions.system, OAI.UniqueGamesTheorem.Fourier.MatrixRestrictions.samples, OAI.UniqueGamesTheorem.Fourier.MatrixRestrictions.Parameter

27. theorem OAI.UniqueGamesTheorem.Fourier.MatrixRestrictions.trueCount_eq_countP line 206
28. theorem OAI.UniqueGamesTheorem.Fourier.MatrixRestrictions.samples_trueCount line 214

    Source documentation

    Exact numerator for uniform sampling of the actual affine restriction.

    theorem samples_trueCount [Finite E] [Finite C] (H : (E →ₗ[F2] C) → Bool)
        (t : Witness E C) :
        Deletion.trueCount H (samples t) =
          (Finset.univ.filter fun A : Parameter t.vanishing t.target =>
            H (translate t.vanishing t.target t.base A) = true).card := by
    …

    Mentions: OAI.UniqueGamesTheorem.Fourier.MatrixRestrictions.Witness, OAI.UniqueGamesTheorem.Fourier.Deletion.trueCount, OAI.UniqueGamesTheorem.Fourier.MatrixRestrictions.samples, OAI.UniqueGamesTheorem.Fourier.MatrixRestrictions.Parameter, OAI.UniqueGamesTheorem.Fourier.MatrixRestrictions.translate

29. def OAI.UniqueGamesTheorem.Fourier.MatrixRestrictions.density line 227
30. theorem OAI.UniqueGamesTheorem.Fourier.MatrixRestrictions.density_eq_count_div line 232
31. theorem OAI.UniqueGamesTheorem.Fourier.MatrixRestrictions.dense_iff_lt_density line 240
32. theorem OAI.UniqueGamesTheorem.Fourier.MatrixRestrictions.remainder_restriction_density line 256

    Source documentation

    Whole-row deletion gives the normalized real restriction bound on every actual affine restriction of the permitted dimension and codimension.

    theorem remainder_restriction_density [Finite E] [Finite C]
        (H : (E →ₗ[F2] C) → Bool) (r p q : Nat) (hq : 0 < q)
        (t : Witness E C) (ht : order t.vanishing t.target ≤ r) :
        density (Deletion.remainder (system r) H p q) t ≤ (p : ℝ) / q := by
    …

    Mentions: OAI.UniqueGamesTheorem.Fourier.MatrixRestrictions.Witness, OAI.UniqueGamesTheorem.Fourier.MatrixRestrictions.order, OAI.UniqueGamesTheorem.Fourier.MatrixRestrictions.density, OAI.UniqueGamesTheorem.Fourier.Deletion.remainder, OAI.UniqueGamesTheorem.Fourier.MatrixRestrictions.system

33. theorem OAI.UniqueGamesTheorem.Fourier.MatrixRestrictions.remainder_restriction_sq_expect line 273

    Source documentation

    The same bound expressed as the squared normalized real L² norm. This is the restriction-global hypothesis used by the Fourier level theorem.

    theorem remainder_restriction_sq_expect [Finite E] [Finite C]
        (H : (E →ₗ[F2] C) → Bool) (r p q : Nat) (hq : 0 < q)
        (W : Submodule F2 E) (C' : Submodule F2 C)
        (horder : order W C' ≤ r) (X : E →ₗ[F2] C) :
        (𝔼 A : Parameter W C',
          (restrict (fun Y => if Deletion.remainder (system r) H p q Y
            then (1 : ℝ) else 0) W C' X A) ^ 2) ≤ (p : ℝ) / q := by
    …

    Mentions: OAI.UniqueGamesTheorem.Fourier.MatrixRestrictions.order, OAI.UniqueGamesTheorem.Fourier.MatrixRestrictions.Parameter, OAI.UniqueGamesTheorem.Fourier.MatrixRestrictions.restrict, OAI.UniqueGamesTheorem.Fourier.Deletion.remainder, OAI.UniqueGamesTheorem.Fourier.MatrixRestrictions.system

34. def OAI.UniqueGamesTheorem.Fourier.MatrixRestrictions.quotientKernelEquiv line 293

    Source documentation

    A dual map killed by the quotient has a unique factor with values in W. This is the exact finite object counted in the parity argument of Lemma 5.3.

    def quotientKernelEquiv (W : Submodule F2 E) :
        {T : C →ₗ[F2] E // W.mkQ.comp T = 0} ≃ (C →ₗ[F2] W) where
    …

35. theorem OAI.UniqueGamesTheorem.Fourier.MatrixRestrictions.quotientKernel_card line 312
36. theorem OAI.UniqueGamesTheorem.Fourier.MatrixRestrictions.quotientKernel_filter_card line 320
37. theorem OAI.UniqueGamesTheorem.Fourier.MatrixRestrictions.deletedSet_iff_exists_target line 330

    Source documentation

    Every deleted point determines its row once the target subspace is fixed. Thus the union bound ranges over target subspaces, not over row values.

    theorem deletedSet_iff_exists_target [Finite E] [Finite C]
        (H : (E →ₗ[F2] C) → Bool) (r p q : Nat) (X : E →ₗ[F2] C) :
        Deletion.DeletedSet (system r) H p q X ↔
          ∃ C' : Submodule F2 C,
            Deletion.BadRow (system r) H p q ⟨C', C'.mkQ.comp X⟩ := by
    …

    Mentions: OAI.UniqueGamesTheorem.Fourier.Deletion.DeletedSet, OAI.UniqueGamesTheorem.Fourier.MatrixRestrictions.system, OAI.UniqueGamesTheorem.Fourier.Deletion.BadRow

38. theorem OAI.UniqueGamesTheorem.Fourier.MatrixRestrictions.badRow_codim_le line 343
39. theorem OAI.UniqueGamesTheorem.Fourier.MatrixRestrictions.deletedSet_iff_exists_admissible_target line 354