SharedPadding.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Padding shared-input tensors with different branch dimensions

The finite separation construction uses fixed ambient coordinate spaces on each leg. A family with a common first leg and varying second and third legs embeds into that setting without changing any character values. The extra coordinates introduced by padding have zero coefficients.

def OAI.MatrixMultiplication.AuxiliarySeparation.sharedFirstDependentTensor line 26
Source documentation
Branches sharing their first input but with independently sized other legs.
```
def sharedFirstDependentTensor (B : ∀ i, Tensor ℂ X (Y i) (Z i)) :
    Tensor ℂ X (Σ i, Y i) (Σ i, Z i) :=
…
```
def OAI.MatrixMultiplication.AuxiliarySeparation.paddedSharedBranch line 31
Source documentation
A branch in the two common sigma coordinate spaces, with zero padding.
```
def paddedSharedBranch (B : ∀ i, Tensor ℂ X (Y i) (Z i)) (i : Fin M) :
    Tensor ℂ X (Σ i, Y i) (Σ i, Z i) :=
…
```
theorem OAI.MatrixMultiplication.AuxiliarySeparation.sharedFirstDependentTensor_matching line 38
theorem OAI.MatrixMultiplication.AuxiliarySeparation.paddedSharedBranch_matching line 44
theorem OAI.MatrixMultiplication.AuxiliarySeparation.paddedSharedBranch_pullback line 50
theorem OAI.MatrixMultiplication.AuxiliarySeparation.paddedSharedBranch_ne_zero line 57
Source documentation
A nonzero branch remains nonzero after padding.
```
theorem paddedSharedBranch_ne_zero
    (B : ∀ i, Tensor ℂ X (Y i) (Z i)) (i : Fin M) (hB : B i ≠ 0) :
    paddedSharedBranch B i ≠ 0 := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.paddedSharedBranch
theorem OAI.MatrixMultiplication.AuxiliarySeparation.paddedSharedBranch_zero_middle line 65
theorem OAI.MatrixMultiplication.AuxiliarySeparation.paddedSharedBranch_zero_right line 73

theorem OAI.MatrixMultiplication.AuxiliarySeparation.sharedFirstTensor_paddedSharedBranch line 82

Source documentation

Redundant branch labels zero-extend the varying-dimension shared tensor.

theorem sharedFirstTensor_paddedSharedBranch
    (B : ∀ i, Tensor ℂ X (Y i) (Z i)) :
    sharedFirstTensor (paddedSharedBranch B) = Tensor.restrict
      (fun (x' : X) x => if x = x' then 1 else 0)
      (fun (y' : Fin M × (Σ i, Y i)) y => if (y.1, y) = y' then 1 else 0)
      (fun (z' : Fin M × (Σ i, Z i)) z => if (z.1, z) = z' then 1 else 0)
      (sharedFirstDependentTensor B) := by
…

Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.sharedFirstTensor, OAI.MatrixMultiplication.AuxiliarySeparation.paddedSharedBranch, OAI.MatrixMultiplication.AuxiliarySeparation.sharedFirstDependentTensor

theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.value_paddedSharedBranch line 121
Source documentation
Padding a branch changes no character value.
```
@[simp] theorem value_paddedSharedBranch (χ : Character)
    (B : ∀ i, Tensor ℂ X (Y i) (Z i)) (i : Fin M) :
    χ.value (paddedSharedBranch B i) = χ.value (B i) := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Character, OAI.MatrixMultiplication.AuxiliarySeparation.paddedSharedBranch
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.value_sharedFirstTensor_padded line 131
Source documentation
Passing to uniform ambient branch spaces adds no character cost.
```
@[simp] theorem value_sharedFirstTensor_padded (χ : Character)
    (B : ∀ i, Tensor ℂ X (Y i) (Z i)) :
    χ.value (sharedFirstTensor (paddedSharedBranch B)) =
      χ.value (sharedFirstDependentTensor B) := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Character, OAI.MatrixMultiplication.AuxiliarySeparation.sharedFirstTensor, OAI.MatrixMultiplication.AuxiliarySeparation.paddedSharedBranch, OAI.MatrixMultiplication.AuxiliarySeparation.sharedFirstDependentTensor