OAI/RingTheory/DirectFiniteness/Pairing.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.KaplanskyCounterexample.PolynomialPairing.Simplex line 14
2. def OAI.KaplanskyCounterexample.PolynomialPairing.point line 16
3. def OAI.KaplanskyCounterexample.PolynomialPairing.newton line 18
4. lemma OAI.KaplanskyCounterexample.PolynomialPairing.newton_degree line 21
5. lemma OAI.KaplanskyCounterexample.PolynomialPairing.newton_eval_zero line 33
6. lemma OAI.KaplanskyCounterexample.PolynomialPairing.newton_eval_diag_ne_zero line 43
7. theorem OAI.KaplanskyCounterexample.PolynomialPairing.exists_interpolation line 57

   Source documentation

   Triangular interpolation on the exact index simplex. The proof provides its total-degree bound, rather than using unrestricted finite-set interpolation.

   theorem exists_interpolation (a : Fin q ≃ Q) (values : Simplex n q d → Q) :
       ∃ f : MvPolynomial (Fin n) Q, f.totalDegree ≤ d ∧
         ∀ k : Simplex n q d, eval (point a k.val) f = values k := by
   …

   Mentions: OAI.KaplanskyCounterexample.PolynomialPairing.Simplex, OAI.KaplanskyCounterexample.PolynomialPairing.point

8. def OAI.KaplanskyCounterexample.PolynomialPairing.lineRestriction line 92

   Source documentation

   Restriction to the full parametrized affine line.

   def lineRestriction (u v : σ → Q) (P : MvPolynomial σ Q) : Polynomial Q :=
   …

9. lemma OAI.KaplanskyCounterexample.PolynomialPairing.lineRestriction_eval line 95
10. lemma OAI.KaplanskyCounterexample.PolynomialPairing.lineRestriction_degree line 103
11. lemma OAI.KaplanskyCounterexample.PolynomialPairing.sum_polynomial_eval line 123

    Source documentation

    The exact finite-field power-sum consequence used on every line.

    lemma sum_polynomial_eval [Fintype Q] (P : Polynomial Q)
        (hP : P.natDegree < Fintype.card Q - 1) : ∑ t : Q, P.eval t = 0 := by
    …

12. theorem OAI.KaplanskyCounterexample.PolynomialPairing.line_sum_zero line 133
13. theorem OAI.KaplanskyCounterexample.PolynomialPairing.affine_space_sum_zero line 140

    Source documentation

    Partitioning the entire affine space into coordinate-parallel lines.

    theorem affine_space_sum_zero [Fintype Q] [Fintype σ] (i : σ) (P : MvPolynomial σ Q)
        (hP : P.totalDegree < Fintype.card Q - 1) :
        ∑ x : σ → Q, MvPolynomial.eval x P = 0 := by
    …

14. def OAI.KaplanskyCounterexample.PolynomialPairing.simplexPoints line 160
15. lemma OAI.KaplanskyCounterexample.PolynomialPairing.mem_simplexPoints line 164
16. def OAI.KaplanskyCounterexample.PolynomialPairing.holePolynomial line 169

    Source documentation

    The interpolation choice is constrained by the exact degree cutoff.

    def holePolynomial (a : Fin q ≃ Q) (d : ℕ) (o : Fin n → Q) :
        MvPolynomial (Fin n) Q :=
    …

17. lemma OAI.KaplanskyCounterexample.PolynomialPairing.holePolynomial_degree line 174
18. lemma OAI.KaplanskyCounterexample.PolynomialPairing.holePolynomial_eval line 179
19. def OAI.KaplanskyCounterexample.PolynomialPairing.column line 186

    Source documentation

    The exact column vector x_v, indexed by the chosen holes.

    def column (a : Fin q ≃ Q) (d : ℕ) (O : Finset (Fin n → Q)) (v : Fin n → Q) : O → Q :=
    …

20. def OAI.KaplanskyCounterexample.PolynomialPairing.gramColumn line 189
21. lemma OAI.KaplanskyCounterexample.PolynomialPairing.sum_holes_gram line 193
22. lemma OAI.KaplanskyCounterexample.PolynomialPairing.gram_degree line 213
23. lemma OAI.KaplanskyCounterexample.PolynomialPairing.cutoff_degree line 219
24. lemma OAI.KaplanskyCounterexample.PolynomialPairing.sum_all_gram line 224

    Source documentation

    All entries of the Gram column sum vanish on the full affine space.

    lemma sum_all_gram (a : Fin q ≃ Q) (hq : q = Fintype.card Q) (hn : 0 < n)
        (O : Finset (Fin n → Q)) :
        ∑ v : Fin n → Q, gramColumn a ((q - 2) / 2) O v = 0 := by
    …

    Mentions: OAI.KaplanskyCounterexample.PolynomialPairing.gramColumn

25. theorem OAI.KaplanskyCounterexample.PolynomialPairing.sum_complement_gram line 237

    Source documentation

    The precise global identity on V, with no characteristic simplification.

    theorem sum_complement_gram (a : Fin q ≃ Q) (hq : q = Fintype.card Q) (hn : 0 < n)
        (O : Finset (Fin n → Q)) (hO : O ⊆ simplexPoints a n ((q - 2) / 2)) :
        ∑ v ∈ Finset.univ \ O, gramColumn a ((q - 2) / 2) O v = -1 := by
    …

    Mentions: OAI.KaplanskyCounterexample.PolynomialPairing.simplexPoints, OAI.KaplanskyCounterexample.PolynomialPairing.gramColumn

26. structure OAI.KaplanskyCounterexample.PolynomialPairing.AffineLine line 245

    Source documentation

    A full affine line, not a segment or a subset of one.

    structure AffineLine (Q : Type u_5) [Field Q] (n : ℕ) where
    …

27. def OAI.KaplanskyCounterexample.PolynomialPairing.AffineLine.param line 250
28. lemma OAI.KaplanskyCounterexample.PolynomialPairing.AffineLine.param_injective line 254
29. def OAI.KaplanskyCounterexample.PolynomialPairing.AffineLine.points line 263
30. lemma OAI.KaplanskyCounterexample.PolynomialPairing.AffineLine.card_points line 266
31. theorem OAI.KaplanskyCounterexample.PolynomialPairing.sum_line_gram line 269