SlotDerivative.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem346.SlotPolynomial.derivation_prod line 13

Source documentation

Leibniz rule for a finite product, expressed by replacing one factor.

theorem derivation_prod (D : Derivation R A A) (s : Finset S) (f : S → A) :
    D (∏ i ∈ s, f i) =
      ∑ i ∈ s, ∏ j ∈ s, Function.update f i (D (f i)) j := by
…

def OAI.Problem346.SlotPolynomial.polynomial line 41
Source documentation
Coordinate polynomial of a coefficient array and an assignment of slots to blocks.
```
def polynomial (c : (S → I) → R) (l : S → B) : MvPolynomial (B × I) R :=
…
```

theorem OAI.Problem346.SlotPolynomial.derivation_polynomial line 45

Source documentation

A directional block derivation replaces each occurrence of the source block in turn.

theorem derivation_polynomial [DecidableEq B]
    (c : (S → I) → R) (l : S → B) (src dst : B)
    (D : Derivation R (MvPolynomial (B × I) R) (MvPolynomial (B × I) R))
    (hD : ∀ b i, D (MvPolynomial.X (b, i)) =
      if b = src then MvPolynomial.X (dst, i) else 0) :
    D (polynomial c l) =
      ∑ s ∈ Finset.univ.filter (fun s => l s = src),
        polynomial c (Function.update l s dst) := by
…

Mentions: OAI.Problem346.SlotPolynomial.polynomial

theorem OAI.Problem346.SlotPolynomial.polynomial_reindex line 84
Source documentation
Reindexing slots moves the same permutation onto the coefficient array.
```
theorem polynomial_reindex (c : (S → I) → R) (l : S → B) (e : Equiv.Perm S) :
    polynomial c (l ∘ e) = polynomial (fun k => c (k ∘ e)) l := by
…
```
Mentions: OAI.Problem346.SlotPolynomial.polynomial
theorem OAI.Problem346.SlotPolynomial.polynomial_reindex_of_invariant line 101
Source documentation
Symmetry of coefficients induces invariance under the same permutation of slot labels.
```
theorem polynomial_reindex_of_invariant (c : (S → I) → R) (l : S → B)
    (e : Equiv.Perm S) (hc : ∀ k, c (k ∘ e) = c k) :
    polynomial c (l ∘ e) = polynomial c l := by
…
```
Mentions: OAI.Problem346.SlotPolynomial.polynomial

theorem OAI.Problem346.SlotPolynomial.polynomial_update_eq line 110

Source documentation

Swapping two equal-labelled slots shows that replacing either label gives the same polynomial.

theorem polynomial_update_eq (c : (S → I) → R) (l : S → B) (s t : S) (dst : B)
    (hl : l s = l t)
    (hc : ∀ k, c (k ∘ Equiv.swap s t) = c k) :
    polynomial c (Function.update l s dst) = polynomial c (Function.update l t dst) := by
…

Mentions: OAI.Problem346.SlotPolynomial.polynomial

theorem OAI.Problem346.SlotPolynomial.derivation_polynomial_eq_card_smul line 130

Source documentation

If all source-labelled slots are interchangeable, the derivative is a single replacement multiplied by their number.

theorem derivation_polynomial_eq_card_smul [DecidableEq B]
    (c : (S → I) → R) (l : S → B) (src dst : B) (t : S) (ht : l t = src)
    (D : Derivation R (MvPolynomial (B × I) R) (MvPolynomial (B × I) R))
    (hD : ∀ b i, D (MvPolynomial.X (b, i)) =
      if b = src then MvPolynomial.X (dst, i) else 0)
    (hc : ∀ s, l s = src → ∀ k, c (k ∘ Equiv.swap s t) = c k) :
    D (polynomial c l) =
      (Finset.univ.filter (fun s => l s = src)).card •
        polynomial c (Function.update l t dst) := by
…

Mentions: OAI.Problem346.SlotPolynomial.polynomial