OAI/Analysis/PlaneSpectrum/NumberFields.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.EuclideanFiveColor.AlgebraicCayley.minpoly_reverse_eval_ne_zero line 10
2. lemma OAI.EuclideanFiveColor.AlgebraicCayley.reciprocal_denominator line 27

   Source documentation

   A scalar-rational common denominator for an algebraic linear reciprocal.

   lemma reciprocal_denominator (b : L) (hb : IsAlgebraic ℚ b) :
       ∃ (P : ℚ[X]) (R : L[X]), P.coeff 0 = 1 ∧
         (1-C b*X)*R = P.map (algebraMap ℚ L) ∧
         ∀ t : ℚ, 1-b*algebraMap ℚ L t ≠ 0 → P.eval t ≠ 0 := by
   …

3. def OAI.EuclideanFiveColor.AlgebraicCayley.polyLinear line 56

   Source documentation

   Coefficientwise transport by a rational linear functional.

   def polyLinear (ℓ : L →ₗ[ℚ] ℚ) (p : L[X]) : ℚ[X] :=
   …

4. lemma OAI.EuclideanFiveColor.AlgebraicCayley.coeff_polyLinear line 58
5. lemma OAI.EuclideanFiveColor.AlgebraicCayley.polyLinear_add line 60
6. lemma OAI.EuclideanFiveColor.AlgebraicCayley.polyLinear_monomial line 64
7. lemma OAI.EuclideanFiveColor.AlgebraicCayley.eval_polyLinear line 69
8. lemma OAI.EuclideanFiveColor.AlgebraicCayley.polyLinear_eq_zero_iff line 80
9. lemma OAI.EuclideanFiveColor.AlgebraicCayley.cayley_annihilation line 87

   Source documentation

   The first three formal coefficients of the Cayley curve force annihilation of 1, b and b². No analytic continuity is used.

   lemma cayley_annihilation (b : L) (hb : IsAlgebraic ℚ b) (ℓ : L →ₗ[ℚ] ℚ)
       (hd : ∀ t : ℚ, 1-b*(algebraMap ℚ L t) ≠ 0)
       (h : ∀ t : ℚ, ℓ ((1+b*(algebraMap ℚ L t))/(1-b*(algebraMap ℚ L t))) = 0) :
       ℓ 1 = 0 ∧ ℓ b = 0 ∧ ℓ (b^2) = 0 := by
   …

10. lemma OAI.EuclideanFiveColor.AlgebraicCayley.linearFraction_polynomials line 154
11. lemma OAI.EuclideanFiveColor.AlgebraicCayley.rational_functions_avoid line 183

    Source documentation

    Finite simultaneous avoidance for rational functions with no rational poles.

    lemma rational_functions_avoid {ι : Type*} (s : Finset ι) (f : ι → ℚ → ℚ)
        (hpoly : ∀ i ∈ s, ∃ P Q : ℚ[X], ∀ t, Q.eval t ≠ 0 ∧ P.eval t = Q.eval t*f i t)
        (hn : ∀ i ∈ s, ∃ t, f i t ≠ 0) :
        ∃ t, ∀ i ∈ s, f i t ≠ 0 := by
    …

12. lemma OAI.EuclideanFiveColor.AlgebraicCayley.finite_hyperplanes_avoid line 207

    Source documentation

    An affine-line rational curve escaping each hyperplane also escapes their finite union.

    lemma finite_hyperplanes_avoid {T : Type*} [Nonempty T]
        (f : T → L) (line : T → T → ℚ → T)
        (hzero : ∀ a b, line a b 0 = a) (hone : ∀ a b, line a b 1 = b)
        (hline : ∀ a b (ℓ : L →ₗ[ℚ] ℚ), ∃ P Q : ℚ[X], ∀ t,
          Q.eval t ≠ 0 ∧ P.eval t = Q.eval t * ℓ (f (line a b t)))
        (s : Finset (L →ₗ[ℚ] ℚ)) (hs : ∀ ℓ ∈ s, ∃ t, ℓ (f t) ≠ 0) :
        ∃ t, ∀ ℓ ∈ s, ℓ (f t) ≠ 0 := by
    …

13. def OAI.EuclideanFiveColor.AlgebraicCayley.realSlice line 235
14. def OAI.EuclideanFiveColor.AlgebraicCayley.asN line 236
15. lemma OAI.EuclideanFiveColor.AlgebraicCayley.coe_asN line 242
16. def OAI.EuclideanFiveColor.AlgebraicCayley.iN line 244
17. lemma OAI.EuclideanFiveColor.AlgebraicCayley.coe_iN line 245
18. lemma OAI.EuclideanFiveColor.AlgebraicCayley.iN_sq line 246
19. lemma OAI.EuclideanFiveColor.AlgebraicCayley.cayley_den_ne line 247
20. def OAI.EuclideanFiveColor.AlgebraicCayley.realCayley line 252
21. lemma OAI.EuclideanFiveColor.AlgebraicCayley.cayley_real_norm line 254
22. lemma OAI.EuclideanFiveColor.AlgebraicCayley.cayley_functional_escape line 266
23. def OAI.EuclideanFiveColor.AlgebraicCayley.realLine line 306
24. lemma OAI.EuclideanFiveColor.AlgebraicCayley.realLine_zero line 309
25. lemma OAI.EuclideanFiveColor.AlgebraicCayley.realLine_one line 311
26. lemma OAI.EuclideanFiveColor.AlgebraicCayley.cayley_line_polynomials line 312
27. lemma OAI.EuclideanFiveColor.AlgebraicCayley.cayley_finite_avoid line 330
28. def OAI.EuclideanFiveColor.GeneralPosition.General line 346
29. lemma OAI.EuclideanFiveColor.GeneralPosition.exists_general line 351

    Source documentation

    Finite general-position sets from avoidance of finitely many proper subspaces.

    lemma exists_general (A : Set V) (hd : 2 ≤ finrank ℚ V)
        (ha : ∀ P : Finset (Submodule ℚ V), (∀ p ∈ P, p < ⊤) →
          ∃ x ∈ A, ∀ p ∈ P, x ∉ p) (n : ℕ) :
        ∃ s : Finset V, s.card = n ∧ (s : Set V) ⊆ A ∧ General s := by
    …

    Mentions: OAI.EuclideanFiveColor.GeneralPosition.General

30. lemma OAI.EuclideanFiveColor.GeneralPosition.General.spans line 404
31. def OAI.EuclideanFiveColor.AlgebraicCayley.generatingSet line 419
32. def OAI.EuclideanFiveColor.AlgebraicCayley.generatedField line 421
33. lemma OAI.EuclideanFiveColor.AlgebraicCayley.generatedField_I line 423
34. lemma OAI.EuclideanFiveColor.AlgebraicCayley.generatedField_real line 426
35. lemma OAI.EuclideanFiveColor.AlgebraicCayley.generatedField_imag line 431
36. lemma OAI.EuclideanFiveColor.AlgebraicCayley.generatedField_contains line 436
37. lemma OAI.EuclideanFiveColor.AlgebraicCayley.generatedField_conj line 440
38. lemma OAI.EuclideanFiveColor.AlgebraicCayley.generatedField_re_closed line 457
39. lemma OAI.EuclideanFiveColor.AlgebraicCayley.generatedField_im_closed line 462
40. lemma OAI.EuclideanFiveColor.AlgebraicCayley.generatedField_finite line 469
41. lemma OAI.EuclideanFiveColor.AlgebraicCayley.finrank_ge_two line 489
42. lemma OAI.EuclideanFiveColor.AlgebraicCayley.cayley_subspaces_avoid line 498
43. lemma OAI.EuclideanFiveColor.AlgebraicCayley.numberField_general_position line 514