OAI/Computability/FourierTransform/ProductMatrix.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Elementary tensor of local matrices in Pi indexing.

  1. def OAI.PowerSaving.digitProd line 14

    Source documentation

    Matrix tensor product indexed by digit tuples.

    def digitProd (M : ∀ j, Matrix (κ j) (μ j) R) :
    Matrix ((j:J) → κ j) ((j:J) → μ j) R :=
…
  2. theorem OAI.PowerSaving.digitProd_apply line 18
  3. theorem OAI.PowerSaving.prod_delta line 22

    Source documentation

    Product of Kronecker deltas.

    theorem prod_delta [∀ j, DecidableEq (κ j)] [DecidableEq ((j:J) → κ j)]
    (x y : (j:J) → κ j) :
    ∏ j:J, (if x j = y j then (1:R) else 0)
    = if x=y then 1 else 0 := by
…
  4. theorem OAI.PowerSaving.digitProd_one line 38
  5. theorem OAI.PowerSaving.digitProd_diagonal line 44
  6. theorem OAI.PowerSaving.digitProd_mul line 63