OAI/LinearAlgebra/MatrixMultiplication/AuxiliarySeparation/Determinant/Filtration.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

The finite determinant filtration of polynomial multiplication

The first leg is kept fixed throughout. The second and third legs use the explicit quotient/kernel vectors of DeterminantKernel. The coefficient identity adaptedTensor_reconstruct verifies the actual multiplication on every basis input; it does not assume a simultaneous triangularization.

  1. abbrev OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.Index line 24
  2. def OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.vector line 27

    Source documentation

    The ordered quotient/kernel vectors in the actual polynomial pair space.

    def vector (e : ℕ) : Index e → DeterminantKernel.FormPair ℂ :=
…

    Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.Index, OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.FormPair

  3. def OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.adaptedTensor line 32

    Source documentation

    All multiplication coefficients in the explicit adapted bases. Here a=d+1, b=e+1, and no first-leg change of coordinates occurs.

    def adaptedTensor (d e : ℕ) : Tensor ℂ (Fin (d + 1)) (Index e) (Index (d + e))
  | i, .inl j, .inl k => if i.val + j.val = k.val then 1 else 0
  | i, .inl j, .inr k =>
      if j.val = e + 1 ∧ i.val < d ∧ e + i.val = k.val then 1 else 0
  | _, .inr _, .inl _ => 0
  | i, .inr j, .inr k => if i.val + j.val = k.val then 1 else 0

/-- The associated graded tensor, whose two branches still share the first leg. -/

    Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.Index

  4. def OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.gradedTensor line 40

    Source documentation

    The associated graded tensor, whose two branches still share the first leg.

    def gradedTensor (d e : ℕ) : Tensor ℂ (Fin (d + 1)) (Index e) (Index (d + e))
  | i, .inl j, .inl k => if i.val + j.val = k.val then 1 else 0
  | _, .inl _, .inr _ => 0
  | _, .inr _, .inl _ => 0
  | i, .inr j, .inr k => if i.val + j.val = k.val then 1 else 0

    Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.Index

  5. theorem OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.sum_coordinate line 46
  6. theorem OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.adaptedTensor_reconstruct line 60

    Source documentation

    Exact coordinate reconstruction of every first-leg slice, in common bases.

    theorem adaptedTensor_reconstruct (d e : ℕ) (i : Fin (d + 1)) (j : Index e) :
    (∑ k : Index (d + e), adaptedTensor d e i j k • vector (d + e) k) =
      DeterminantKernel.multiply (X ^ i.val) (vector e j) := by
…

    Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.Index, OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.adaptedTensor, OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.vector, OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.multiply

  7. theorem OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.adaptedTensor_unique line 95

    Source documentation

    The reconstruction uniquely determines every tensor coefficient.

    theorem adaptedTensor_unique (d e : ℕ)
    (T : Tensor ℂ (Fin (d + 1)) (Index e) (Index (d + e)))
    (hT : ∀ i j, (∑ k, T i j k • vector (d + e) k) =
      DeterminantKernel.multiply (X ^ i.val) (vector e j)) :
    T = adaptedTensor d e := by
…

    Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.Index, OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.vector, OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantKernel.multiply, OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.adaptedTensor

  8. theorem OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.gradedTensor_quotient line 108

    Source documentation

    The quotient branch is exactly C(a,b+1).

    theorem gradedTensor_quotient (d e : ℕ) (i : Fin (d + 1))
    (j : Fin (e + 2)) (k : Fin (d + e + 2)) :
    gradedTensor d e i (.inl j) (.inl k) =
      convolution (d + 1) (e + 2) i j (Fin.cast (by omega) k) := by
…

    Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.gradedTensor, OAI.MatrixMultiplication.AuxiliarySeparation.convolution, OAI.MatrixMultiplication.AuxiliarySeparation.omega

  9. theorem OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.gradedTensor_kernel line 115

    Source documentation

    The kernel branch is exactly C(a,b-1).

    theorem gradedTensor_kernel (d e : ℕ) (i : Fin (d + 1))
    (j : Fin e) (k : Fin (d + e)) :
    gradedTensor d e i (.inr j) (.inr k) =
      convolution (d + 1) e i j (Fin.cast (by omega) k) := by
…

    Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.gradedTensor, OAI.MatrixMultiplication.AuxiliarySeparation.convolution, OAI.MatrixMultiplication.AuxiliarySeparation.omega

  10. theorem OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.adaptedTensor_kernel_to_quotient line 121
  11. def OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.inputScale line 127

    Source documentation

    Polynomial diagonal maps; scaling the quotient input by X clears the negative input-kernel weight without changing the leading tensor.

    def inputScale (e : ℕ) : Index e → ℂ[X]
  | .inl _ => X
  | .inr _ => 1

    Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.Index

  12. def OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.outputScale line 131
  13. def OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.diagonalMap line 135
  14. theorem OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.restrict_diagonal line 138
  15. def OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.degeneration line 148

    Source documentation

    A checked polynomial degeneration to the two matched convolution branches.

    def degeneration (d e : ℕ) :
    Tensor.PolynomialRestrictionDegeneration (adaptedTensor d e)
      (gradedTensor d e) 1 0 1 1 where
…

    Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.adaptedTensor, OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.gradedTensor

  16. abbrev OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.OriginalIndex line 186
  17. def OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.originalBasis line 189

    Source documentation

    The original monomial bases in the s and w components.

    def originalBasis (e : ℕ) :
    Module.Basis (OriginalIndex e) ℂ (DeterminantBasis.BoundedPair ℂ e) :=
…

    Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.OriginalIndex, OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantBasis.BoundedPair

  18. theorem OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.degree_shift_lt line 193
  19. def OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.boundedShift line 206

    Source documentation

    Multiplication by a fixed first-input monomial between the bounded spaces.

    def boundedShift (d e : ℕ) (i : Fin (d + 1)) :
    Polynomial.degreeLT ℂ (e + 1) →ₗ[ℂ] Polynomial.degreeLT ℂ (d + e + 1) where
…
  20. def OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.boundedMultiply line 213

    Source documentation

    The same first monomial multiplies both components.

    def boundedMultiply (d e : ℕ) (i : Fin (d + 1)) :
    DeterminantBasis.BoundedPair ℂ e →ₗ[ℂ] DeterminantBasis.BoundedPair ℂ (d + e) :=
…

    Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantBasis.BoundedPair

  21. theorem OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.forget_boundedMultiply line 217
  22. def OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.sourceTensor line 223

    Source documentation

    Polynomial multiplication in its original monomial coordinates.

    def sourceTensor (d e : ℕ) :
    Tensor ℂ (Fin (d + 1)) (OriginalIndex e) (OriginalIndex (d + e)) :=
…

    Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.OriginalIndex

  23. theorem OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.sourceTensor_inl_inl line 228
  24. theorem OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.sourceTensor_inr_inr line 235
  25. theorem OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.sourceTensor_inl_inr line 242
  26. theorem OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.sourceTensor_inr_inl line 247
  27. def OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.originalCoordinate line 253

    Source documentation

    Record the polynomial coordinate and the choice of s or w separately.

    def originalCoordinate (e : ℕ) : OriginalIndex e → Fin (e + 1) × Bool
  | .inl j => (j, false)
  | .inr j => (j, true)

/-- The source is exactly polynomial convolution tensored with a two-coordinate
dot product whose singleton is on the unchanged first leg. -/

    Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.OriginalIndex, OAI.MatrixMultiplication.AuxiliarySeparation.convolution

  28. theorem OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.sourceTensor_product line 259

    Source documentation

    The source is exactly polynomial convolution tensored with a two-coordinate dot product whose singleton is on the unchanged first leg.

    theorem sourceTensor_product (d e : ℕ) :
    sourceTensor d e =
      Tensor.pullback (fun i : Fin (d + 1) => (i, ())) (originalCoordinate e)
        (fun k => (Fin.cast (by omega) (originalCoordinate (d + e) k).1,
          (originalCoordinate (d + e) k).2))
        (Tensor.product (convolution (d + 1) (e + 1))
          (Tensor.cyclic (Tensor.cyclic (Tensor.dotPairing (K := ℂ) Bool)))) := by
…

    Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.sourceTensor, OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.originalCoordinate, OAI.MatrixMultiplication.AuxiliarySeparation.omega, OAI.MatrixMultiplication.AuxiliarySeparation.convolution

  29. def OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.inputChange line 272

    Source documentation

    The input matrix has adapted vectors as columns in the original basis.

    def inputChange (e : ℕ) (j : Index e) (old : OriginalIndex e) : ℂ :=
…

    Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.Index, OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.OriginalIndex

  30. def OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.outputDualChange line 276

    Source documentation

    The output-dual matrix uses the inverse basis change, as required for tensors.

    def outputDualChange (e : ℕ) (k : Index e) (old : OriginalIndex e) : ℂ :=
…

    Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.Index, OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.OriginalIndex

  31. def OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.fixedFirst line 280

    Source documentation

    The first input is unchanged, including throughout the basis change.

    def fixedFirst (d : ℕ) (i j : Fin (d + 1)) : ℂ := if i = j then 1 else 0
  32. theorem OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.restrict_fixedFirst line 282
  33. theorem OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.boundedMultiply_adapted_coordinates line 291
  34. theorem OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.sourceTensor_coordinate_change line 309

    Source documentation

    A concrete restriction, with the identity first map, changes the original two-copy convolution into the simultaneously triangular coefficient tensor.

    theorem sourceTensor_coordinate_change (d e : ℕ) :
    Tensor.restrict (fixedFirst d) (inputChange e) (outputDualChange (d + e))
      (sourceTensor d e) = adaptedTensor d e := by
…

    Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.fixedFirst, OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.inputChange, OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.outputDualChange, OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.sourceTensor, OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.adaptedTensor