OAI/Computability/RationalHitting/Affine.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.RationalHitting.Affine.Form line 10
2. def OAI.RationalHitting.Affine.constant line 11
3. def OAI.RationalHitting.Affine.varForm line 12
4. def OAI.RationalHitting.Affine.eval line 14
5. lemma OAI.RationalHitting.Affine.eval_constant line 21
6. lemma OAI.RationalHitting.Affine.eval_variable line 23
7. def OAI.RationalHitting.Affine.constMatrix line 26
8. lemma OAI.RationalHitting.Affine.eval_constMatrix line 27
9. def OAI.RationalHitting.Formula.Index line 37
10. instance OAI.RationalHitting.Formula.indexFintype line 42
11. instance OAI.RationalHitting.Formula.indexDecidableEq line 47
12. lemma OAI.RationalHitting.Formula.card_index line 52
13. def OAI.RationalHitting.Formula.row line 72
14. def OAI.RationalHitting.Formula.col line 77
15. def OAI.RationalHitting.Formula.pencil line 83
16. abbrev OAI.RationalHitting.Formula.realized line 91
17. abbrev OAI.RationalHitting.Formula.rowR line 92
18. abbrev OAI.RationalHitting.Formula.colR line 93
19. abbrev OAI.RationalHitting.Formula.scalar line 94
20. lemma OAI.RationalHitting.Formula.realized_add line 96
21. lemma OAI.RationalHitting.Formula.realized_mul line 101
22. lemma OAI.RationalHitting.Formula.realized_inv line 107
23. lemma OAI.RationalHitting.Formula.rowR_add line 113
24. lemma OAI.RationalHitting.Formula.colR_add line 116
25. lemma OAI.RationalHitting.Formula.rowR_mul line 119
26. lemma OAI.RationalHitting.Formula.colR_mul line 123
27. lemma OAI.RationalHitting.Formula.rowR_inv line 127
28. lemma OAI.RationalHitting.Formula.colR_inv line 131
29. lemma OAI.RationalHitting.Formula.leaf_realization line 136
30. theorem OAI.RationalHitting.Formula.Eval.realization line 150

    Source documentation

    Exact affine realization of every defined original subtree.

    theorem Eval.realization {f : Formula n} {a : R} (ha : Eval c X f a) :
        ∃ M : Matrix f.Index f.Index R,
          realized c X f * M = 1 ∧ M * realized c X f = 1 ∧
          rowR c f * M * colR c f = scalar a := by
    …

    Mentions: OAI.RationalHitting.Formula, OAI.RationalHitting.Formula.Eval, OAI.RationalHitting.Formula.realized, OAI.RationalHitting.Formula.rowR, OAI.RationalHitting.Formula.colR, OAI.RationalHitting.Formula.scalar

31. def OAI.RationalHitting.Formula.inverseNodes line 234

    Source documentation

    The list retains occurrences, not just distinct subexpressions.

    def inverseNodes : Formula n → List (Formula n)
      | .var _ | .const _ => []
      | .add f g | .mul f g => inverseNodes f ++ inverseNodes g
      | .inv f => .inv f :: inverseNodes f
    
    /-- `.inv f` here denotes the root augmentation pencil, not a new counted gate. -/

    Mentions: OAI.RationalHitting.Formula, OAI.RationalHitting.Formula.pencil

32. def OAI.RationalHitting.Formula.certificates line 240

    Source documentation

    .inv f here denotes the root augmentation pencil, not a new counted gate.

    def certificates (f : Formula n) := inverseNodes f ++ [.inv f]

    Mentions: OAI.RationalHitting.Formula, OAI.RationalHitting.Formula.inverseNodes

33. lemma OAI.RationalHitting.Formula.Eval.pencil_isUnit line 242
34. lemma OAI.RationalHitting.Formula.Eval.augmented_isUnit_iff line 247
35. lemma OAI.RationalHitting.Formula.Eval.inverseNodes_units line 255
36. lemma OAI.RationalHitting.Formula.eval_of_inverseNodes_units line 268
37. theorem OAI.RationalHitting.Formula.certificates_iff line 290

    Source documentation

    Full original-tree definedness and invertible final value are equivalent to all affine-pencil certificates. No rational cancellation is performed.

    theorem certificates_iff (f : Formula n) :
        (∀ h ∈ certificates f, IsUnit (realized c X h)) ↔
          ∃ a, Eval c X f a ∧ IsUnit a := by
    …

    Mentions: OAI.RationalHitting.Formula, OAI.RationalHitting.Formula.certificates, OAI.RationalHitting.Formula.realized, OAI.RationalHitting.Formula.Eval

38. lemma OAI.RationalHitting.Formula.inverseNodes_length line 305
39. lemma OAI.RationalHitting.Formula.size_le_of_mem_inverseNodes line 308
40. lemma OAI.RationalHitting.Formula.certificate_bounds line 326
41. def OAI.RationalHitting.Affine.coeff line 352
42. def OAI.RationalHitting.Affine.homogeneous line 354
43. lemma OAI.RationalHitting.Affine.homogeneous_one line 357
44. lemma OAI.RationalHitting.Affine.normalized line 361
45. lemma OAI.RationalHitting.Affine.normalized_pencil line 376
46. lemma OAI.RationalHitting.Affine.normalized_pencil_unit line 386
47. lemma OAI.RationalHitting.Affine.eval_reindex line 398

    Source documentation

    Reindexing a pencil's coefficients does not alter its matrix evaluation.

    lemma eval_reindex.{v_2, v_3, v_4, v_5} {n : ℕ} {K : Type v_2} [Field K]
      [CharZero K] {ι : Type v_3} {κ : Type v_4} [Fintype ι] [DecidableEq ι] [Fintype κ]
      [DecidableEq κ] (L : Matrix ι ι (RationalHitting.Affine.Form n)) (X : Fin n → Matrix κ κ K)
      {ι' : Type v_5} (e : ι ≃ ι') :
      ((Matrix.reindex e e) L).map ⇑(RationalHitting.Affine.eval (algebraMap ℚ (Matrix κ κ K)) X) =
        (Matrix.reindex e e) (L.map ⇑(RationalHitting.Affine.eval (algebraMap ℚ (Matrix κ κ K)) X)) := rfl

    Mentions: OAI.RationalHitting.Affine.Form, OAI.RationalHitting.Affine.eval

48. lemma OAI.RationalHitting.Affine.homogeneous_flat line 406

    Source documentation

    Homogeneous affine coefficients give exactly the ordinary Kronecker pencil.

    lemma homogeneous_flat.{v_2, v_3, v_4} {n : ℕ} {K : Type v_2} [Field K]
      [CharZero K] {ι : Type v_3} {κ : Type v_4} [Fintype ι] [DecidableEq ι] [Fintype κ]
      [DecidableEq κ] (L : Matrix ι ι (RationalHitting.Affine.Form n))
      (Z : Fin (n + 1) → Matrix κ κ K) :
      (Matrix.compRingEquiv ι κ K)
          (L.map (RationalHitting.Affine.homogeneous (algebraMap ℚ (Matrix κ κ K)) Z)) =
        fun a b => ∑ r, (algebraMap ℚ K) (RationalHitting.Affine.coeff (L a.1 b.1) r) * Z r a.2 b.2 := by
    …

    Mentions: OAI.RationalHitting.Affine.Form, OAI.RationalHitting.Affine.homogeneous, OAI.RationalHitting.Affine.coeff