MonomialCut.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem346.symMonomial_cut line 13
Source documentation
Splitting a list of equal factors at a cutoff is graded multiplication of two pure powers.
```
theorem symMonomial_cut (r m : ℕ) (x y : V) :
    symMonomial (r+m) V (fun j => if j.val < r then x else y) =
      symPowMul r m (symMonomial r V (fun _ => x))
        (symMonomial m V (fun _ => y)) := by
…
```
Mentions: OAI.Problem346.symMonomial, OAI.Problem346.symPowMul

theorem OAI.Problem346.symMonomialRaw_cut line 25

Source documentation

Cast-free raw form of the cutoff identity.

theorem symMonomialRaw_cut (r m : ℕ) (x y : V) :
    symMonomialRaw (r+m) V (fun j => if j.val < r then x else y) =
      SymmetricAlgebra.ι ℂ V x ^ r * SymmetricAlgebra.ι ℂ V y ^ m := by
…

Mentions: OAI.Problem346.symMonomialRaw

theorem OAI.Problem346.multilinear_cut_endpoint line 33

Source documentation

The all-row terminal cutoff in the second transfer matches its common-power product form.

theorem multilinear_cut_endpoint (r m : ℕ)
    (T : SymmetricMultilinearForm (r+1) (r+m) V)
    (x t : V) (v : Fin r → V) :
    T (Fin.cons (symMonomial (r+m) V (fun _ => t))
      (fun i => symMonomial (r+m) V (fun j => if j.val < r then x else v i))) =
    T (Fin.cons (symMonomial (r+m) V (fun _ => t))
      (fun i => symPowMul r m (symMonomial r V (fun _ => x))
        (symMonomial m V (fun _ => v i)))) := by
…

Mentions: OAI.Problem346.SymmetricMultilinearForm, OAI.Problem346.symMonomial, OAI.Problem346.symPowMul

theorem OAI.Problem346.multilinear_cut_endpoint_zero line 44

Source documentation

Vanishing on arbitrary residual products gives vanishing on the terminal cutoff.

theorem multilinear_cut_endpoint_zero (r m : ℕ)
    (T : SymmetricMultilinearForm (r+1) (r+m) V)
    (h : ∀ x t : V, ∀ Q : Fin r → SymPow m V,
      T (Fin.cons (symMonomial (r+m) V (fun _ => t))
        (fun i => symPowMul r m (symMonomial r V (fun _ => x)) (Q i))) = 0)
    (x t : V) (v : Fin r → V) :
    T (Fin.cons (symMonomial (r+m) V (fun _ => t))
      (fun i => symMonomial (r+m) V (fun j => if j.val < r then x else v i))) = 0 := by
…

Mentions: OAI.Problem346.SymmetricMultilinearForm, OAI.Problem346.SymPow, OAI.Problem346.symMonomial, OAI.Problem346.symPowMul