Pseudorandom sets in Grassmann graph have near-perfect expansion

Problem statement

Notes: Unavailable.

Source: S. Khot, D. Minzer, and M. Safra, `Pseudorandom sets in Grassmann graph have near-perfect expansion`, Annals of Math, 198 (1) 2023. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge (v1.0.0, e32eb14), AnnalsChallenge/AnnalsOfMathematics/2023-198-1-PseudorandomGrassmann.lean

Informal solution: Unavailable.

theorem declaration uses `sorry`theorem_1_12 (α : ℝ) (hα : α ∈ Set.Ioo 0 1) :
    ∃ ε > 0, ∃ r, ∀ᶠ (ℓ : ℕ) (k : ℕ) in atTop, ∀ S : Finset (PseudorandomGrassmann.GrVertex k ℓ),
      (hS : S.Nonempty) → 2 * #S ≤ Fintype.card (PseudorandomGrassmann.GrVertex k ℓ) →
        Φ (PseudorandomGrassmann.Gr k ℓ) S hS ≤ α → ∃ (A B : Submodule 𝔽₂ (Fin k → 𝔽₂)), A ≤ B ∧
          letI a := finrank 𝔽₂ A; letI b := k - finrank 𝔽₂ B
          a + b ≤ r ∧ #(S ∩ SubGr k ℓ A B) / #(SubGr k ℓ A B) ≥ (ε : ℝ) := byα:ℝhα:α ∈ Set.Ioo 0 1⊢ ∃ ε > 0,
  ∃ r,
    ∀ᶠ (ℓ : ℕ) (k : ℕ) in atTop,
      ∀ (S : Finset (GrVertex k ℓ)) (hS : S.Nonempty),
        2 * #S ≤ Fintype.card (GrVertex k ℓ) →
          ↑(Φ (Gr k ℓ) S hS) ≤ α →
            ∃ A B, A ≤ B ∧ finrank 𝔽₂ ↥A + (k - finrank 𝔽₂ ↥B) ≤ r ∧ ↑(#(S ∩ SubGr k ℓ A B)) / ↑(#(SubGr k ℓ A B)) ≥ ε
  sorryAll goals completed! 🐙