OAI/Combinatorics/HadwigerCounterexample/FrameIntersectionBounds.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.HadwigerCounterexample.pad_matrix_inj line 14

   Source documentation

   Standard embedding padded by zeros.

   theorem pad_matrix_inj (a b : ℕ) (h : a ≤ b) :
       ∃ M : Mat (Fin b) (Fin a), Function.Injective M.mulVec := by
   …

   Mentions: OAI.HadwigerCounterexample.Mat

2. theorem OAI.HadwigerCounterexample.bounded_pack line 21
3. abbrev OAI.HadwigerCounterexample.KCand line 43
4. def OAI.HadwigerCounterexample.zeroPin line 45
5. theorem OAI.HadwigerCounterexample.largeJoin_pin line 48
6. theorem OAI.HadwigerCounterexample.num_kcand line 78
7. theorem OAI.HadwigerCounterexample.raw_join_cap line 91
8. theorem OAI.HadwigerCounterexample.sparse_usual line 118

   Source documentation

   The stronger join restriction is exponentially likely under the stated joint cap.

   theorem sparse_usual (p : Shape) (D : ℕ) (hd : 0 < D) :
       ∀ᶠ M : ℕ in atTop, ∀ᶠ n : ℕ in atTop, let N := M*n;
   …

   Mentions: OAI.HadwigerCounterexample.Shape