OAI/RingTheory/DirectFiniteness/PrescribedPairing.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.KaplanskyCounterexample.hole_size_inequalities line 12

   Source documentation

   The numerical interval for the holes gives exactly the strict rectangular inequality and the ell-squared packing bound, without rounding assumptions.

   lemma hole_size_inequalities {N m ℓ : ℕ} (hN : 0 < N) (hmN : m ≤ N)
       (hℓ : 3 ≤ ℓ) (hlo : 2 * N ≤ m * (ℓ+1)^2)
       (hhi : m * (ℓ+1)^2 ≤ 7 * N) :
       0 < m ∧ m < N-m ∧ N-m ≤ m * ℓ^2 := by
   …

2. def OAI.KaplanskyCounterexample.PolynomialPairing.complementMatrix line 32
3. lemma OAI.KaplanskyCounterexample.PolynomialPairing.complementMatrix_global line 36
4. lemma OAI.KaplanskyCounterexample.PolynomialPairing.sum_fullLine_gram line 55
5. lemma OAI.KaplanskyCounterexample.PolynomialPairing.complementMatrix_local line 68