SupportExtension.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Recovering tensors from their supported coordinate subspaces

If a tensor has support inside three injectively embedded coordinate sets, it is exactly the extension by zero of its pullback to those sets. Characters therefore have the same value on the ambient tensor and this smaller tensor.

theorem OAI.MatrixMultiplication.AuxiliarySeparation.tensor_eq_extendByZero_pullback line 24

Source documentation

Support in embedded coordinate sets reconstructs the tensor by zero extension.

theorem tensor_eq_extendByZero_pullback (T : Tensor ℂ X' Y' Z')
    (fx : X → X') (fy : Y → Y') (fz : Z → Z')
    (hx : Function.Injective fx) (hy : Function.Injective fy)
    (hz : Function.Injective fz)
    (hs : ∀ x' y' z', T x' y' z' ≠ 0 →
      x' ∈ Set.range fx ∧ y' ∈ Set.range fy ∧ z' ∈ Set.range fz) :
    T = Tensor.restrict
      (fun x' x => if fx x = x' then 1 else 0)
      (fun y' y => if fy y = y' then 1 else 0)
      (fun z' z => if fz z = z' then 1 else 0)
      (Tensor.pullback fx fy fz T) := by
…

theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.value_eq_pullback_of_support line 64

Source documentation

A character ignores ambient coordinates outside a tensor's support.

theorem value_eq_pullback_of_support (χ : Character) (T : Tensor ℂ X' Y' Z')
    (fx : X → X') (fy : Y → Y') (fz : Z → Z')
    (hx : Function.Injective fx) (hy : Function.Injective fy)
    (hz : Function.Injective fz)
    (hs : ∀ x' y' z', T x' y' z' ≠ 0 →
      x' ∈ Set.range fx ∧ y' ∈ Set.range fy ∧ z' ∈ Set.range fz) :
    χ.value T = χ.value (Tensor.pullback fx fy fz T) := by
…

Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Character