Basic.lean`

27 declarations, 0 contain sorry, 0 declared as axioms

The tensor map with exactly `5M` copies

The branches have a common first coordinate space and common sizes on the other two legs. Their second and third coordinates carry a matching sector label. The three maps below are independent linear substitutions on the three legs of 5M complete copies of the source tensor.

def OAI.MatrixMultiplication.AuxiliarySeparation.sectorNumber line 31
Source documentation
The paper numbers sectors from one, while Fin M numbers them from zero.
```
def sectorNumber (i : Fin M) : ℤ := (i.val : ℤ) + 1
```
theorem OAI.MatrixMultiplication.AuxiliarySeparation.sectorNumber_bounds line 33
theorem OAI.MatrixMultiplication.AuxiliarySeparation.sectorNumber_injective line 39
def OAI.MatrixMultiplication.AuxiliarySeparation.sharedFirstTensor line 46
Source documentation
Branches sharing X, with matching and disjoint Y and Z sectors.
```
def sharedFirstTensor (B : Fin M → Tensor ℂ X Y Z) :
    Tensor ℂ X (Fin M × Y) (Fin M × Z) :=
…
```
def OAI.MatrixMultiplication.AuxiliarySeparation.firstProjectionMap line 51
Source documentation
The first local Fourier substitution guesses the missing sector.
```
def firstProjectionMap (ζ : ℂ) :
    (X × Fin M) → (Fin (5 * M) × X) → ℂ := by
…
```
def OAI.MatrixMultiplication.AuxiliarySeparation.secondProjectionMap line 58
Source documentation
The second local map knows the sector through its original coordinate.
```
def secondProjectionMap (ζ : ℂ) :
    ((Fin M × Y) × Fin M) → (Fin (5 * M) × (Fin M × Y)) → ℂ := by
…
```
def OAI.MatrixMultiplication.AuxiliarySeparation.thirdProjectionMap line 65
Source documentation
The third local map carries the single Fourier normalization factor.
```
def thirdProjectionMap (ζ : ℂ) :
    ((Fin M × Z) × Fin M) → (Fin (5 * M) × (Fin M × Z)) → ℂ := by
…
```
theorem OAI.MatrixMultiplication.AuxiliarySeparation.restrict_constantCopies line 72
theorem OAI.MatrixMultiplication.AuxiliarySeparation.restrict_constantCopies_delta line 83
def OAI.MatrixMultiplication.AuxiliarySeparation.projectedTensor line 100
Source documentation
The exact coefficient tensor after Fourier projection, before weighting.
```
def projectedTensor (ζ : ℂ) (B : Fin M → Tensor ℂ X Y Z) :
    Tensor ℂ (X × Fin M) ((Fin M × Y) × Fin M) ((Fin M × Z) × Fin M) :=
…
```
theorem OAI.MatrixMultiplication.AuxiliarySeparation.finiteProjection_restrict line 110
Source documentation
The paper's 5M copies and its three explicit local Fourier maps realize the projected tensor by an ordinary restriction.
```
theorem finiteProjection_restrict [Fintype X] [Fintype Y] [Fintype Z]
    (ζ : ℂ) (hζ : ζ ≠ 0) (B : Fin M → Tensor ℂ X Y Z) :
    Tensor.restrict (firstProjectionMap ζ) (secondProjectionMap ζ)
        (thirdProjectionMap ζ)
        (Tensor.directSum (fun _ : Fin (5 * M) => sharedFirstTensor B)) =
      projectedTensor ζ B := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.firstProjectionMap, OAI.MatrixMultiplication.AuxiliarySeparation.secondProjectionMap, OAI.MatrixMultiplication.AuxiliarySeparation.thirdProjectionMap, OAI.MatrixMultiplication.AuxiliarySeparation.sharedFirstTensor, OAI.MatrixMultiplication.AuxiliarySeparation.projectedTensor

def OAI.MatrixMultiplication.AuxiliarySeparation.separationPolynomial line 159

Source documentation

The polynomial after the Fourier projection and square weighting.

def separationPolynomial (ζ : ℂ) (B : Fin M → Tensor ℂ X Y Z) :
    Tensor (Polynomial ℂ) (X × Fin M)
      ((Fin M × Y) × Fin M) ((Fin M × Z) × Fin M) :=
…

def OAI.MatrixMultiplication.AuxiliarySeparation.separationTarget line 169
Source documentation
The surviving tensor: sector labels match on all three legs, while the additional second/third coordinates form a dot product.
```
def separationTarget (B : Fin M → Tensor ℂ X Y Z) :
    Tensor ℂ (X × Fin M) ((Fin M × Y) × Fin M) ((Fin M × Z) × Fin M) :=
…
```
theorem OAI.MatrixMultiplication.AuxiliarySeparation.separationPolynomial_coeff_zero line 175
Source documentation
The square-weighted polynomial has exactly the advertised constant tensor.
```
theorem separationPolynomial_coeff_zero {ζ : ℂ} (hM : 0 < M)
    (hζ : IsPrimitiveRoot ζ (5 * M)) (B : Fin M → Tensor ℂ X Y Z) :
    (fun x y z => (separationPolynomial ζ B x y z).coeff 0) =
      separationTarget B := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.separationPolynomial, OAI.MatrixMultiplication.AuxiliarySeparation.separationTarget

theorem OAI.MatrixMultiplication.AuxiliarySeparation.separationPolynomial_degree line 190

Source documentation

Its degree is bounded for each fixed finite separation construction.

theorem separationPolynomial_degree {ζ : ℂ} (hM : 0 < M)
    (hζ : IsPrimitiveRoot ζ (5 * M)) (B : Fin M → Tensor ℂ X Y Z)
    (x : X × Fin M) (y : (Fin M × Y) × Fin M) (z : (Fin M × Z) × Fin M) :
    (separationPolynomial ζ B x y z).degree ≤ ((M - 1) ^ 2 : ℕ) := by
…

Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.separationPolynomial

theorem OAI.MatrixMultiplication.AuxiliarySeparation.restrict_target_scalars line 204
def OAI.MatrixMultiplication.AuxiliarySeparation.firstSeparationMap line 222
Source documentation
The first local Fourier map followed by its integer weight.
```
def firstSeparationMap (ζ t : ℂ) (x : X × Fin M) (r : Fin (5 * M) × X) : ℂ :=
…
```
def OAI.MatrixMultiplication.AuxiliarySeparation.secondSeparationMap line 226
Source documentation
The second local Fourier map followed by its possibly negative weight.
```
def secondSeparationMap (ζ t : ℂ) (y : (Fin M × Y) × Fin M)
    (r : Fin (5 * M) × (Fin M × Y)) : ℂ :=
…
```
def OAI.MatrixMultiplication.AuxiliarySeparation.thirdSeparationMap line 231
Source documentation
The third local Fourier map followed by its possibly negative weight.
```
def thirdSeparationMap (ζ t : ℂ) (z : (Fin M × Z) × Fin M)
    (r : Fin (5 * M) × (Fin M × Z)) : ℂ :=
…
```
theorem OAI.MatrixMultiplication.AuxiliarySeparation.weightedProjection_restrict line 235
theorem OAI.MatrixMultiplication.AuxiliarySeparation.separationPolynomial_eval line 250
Source documentation
At every nonzero parameter the polynomial tensor is an ordinary restriction of exactly 5M complete source copies.
```
theorem separationPolynomial_eval [Fintype X] [Fintype Y] [Fintype Z]
    {ζ : ℂ} (hM : 0 < M) (hζ : IsPrimitiveRoot ζ (5 * M))
    (B : Fin M → Tensor ℂ X Y Z) (t : ℂ) (ht : t ≠ 0) :
    (fun x y z => (separationPolynomial ζ B x y z).eval t) =
      Tensor.restrict (firstSeparationMap ζ t) (secondSeparationMap ζ t)
        (thirdSeparationMap ζ t)
        (Tensor.directSum (fun _ : Fin (5 * M) => sharedFirstTensor B)) := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.separationPolynomial, OAI.MatrixMultiplication.AuxiliarySeparation.firstSeparationMap, OAI.MatrixMultiplication.AuxiliarySeparation.secondSeparationMap, OAI.MatrixMultiplication.AuxiliarySeparation.thirdSeparationMap, OAI.MatrixMultiplication.AuxiliarySeparation.sharedFirstTensor
theorem OAI.MatrixMultiplication.AuxiliarySeparation.polynomial_degeneration_of_nonzero_restrictions line 278
theorem OAI.MatrixMultiplication.AuxiliarySeparation.finiteSeparation_degeneratesTo line 306
Source documentation
Exact finite separation: 5M source copies degenerate to all M branches, each retaining an M-dimensional dot-product factor.
```
theorem finiteSeparation_degeneratesTo [Fintype X] [Fintype Y] [Fintype Z]
    (hM : 0 < M) (B : Fin M → Tensor ℂ X Y Z) :
    Tensor.DegeneratesTo
      (Tensor.directSum (fun _ : Fin (5 * M) => sharedFirstTensor B))
      (separationTarget B) := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.sharedFirstTensor, OAI.MatrixMultiplication.AuxiliarySeparation.separationTarget
def OAI.MatrixMultiplication.AuxiliarySeparation.separationFirstEquiv line 321
Source documentation
The first-leg relabeling adds the trivial first coordinate of the dot product.
```
def separationFirstEquiv : (X × Fin M) ≃ (Fin M × (X × Unit)) where
…
```
def OAI.MatrixMultiplication.AuxiliarySeparation.separationSideEquiv line 328
Source documentation
The other two relabelings merely reassociate their coordinates.
```
def separationSideEquiv (A : Type*) : ((Fin M × A) × Fin M) ≃
    (Fin M × (A × Fin M)) := Equiv.prodAssoc _ _ _
```
theorem OAI.MatrixMultiplication.AuxiliarySeparation.separationTarget_eq_directSum line 332
Source documentation
The separated target, expressed as a genuine full direct sum of products.
```
theorem separationTarget_eq_directSum (B : Fin M → Tensor ℂ X Y Z) :
    separationTarget B =
      Tensor.pullback
        separationFirstEquiv (separationSideEquiv Y) (separationSideEquiv Z)
        (Tensor.directSum (fun h => Tensor.product (B h)
          (Tensor.cyclic (Tensor.cyclic (Tensor.dotPairing (K := ℂ) (Fin M)))))) := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.separationTarget, OAI.MatrixMultiplication.AuxiliarySeparation.separationFirstEquiv, OAI.MatrixMultiplication.AuxiliarySeparation.separationSideEquiv

theorem OAI.MatrixMultiplication.AuxiliarySeparation.finiteSeparation_directSum_degeneratesTo line 351

Source documentation

The finite separation theorem with the output written literally as a full direct sum of the M branch/dot-product tensors.

theorem finiteSeparation_directSum_degeneratesTo
    [Fintype X] [Fintype Y] [Fintype Z]
    (hM : 0 < M) (B : Fin M → Tensor ℂ X Y Z) :
    Tensor.DegeneratesTo
      (Tensor.directSum (fun _ : Fin (5 * M) => sharedFirstTensor B))
      (Tensor.directSum (fun h => Tensor.product (B h)
        (Tensor.cyclic (Tensor.cyclic (Tensor.dotPairing (K := ℂ) (Fin M)))))) := by
…

Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.sharedFirstTensor

OAI/LinearAlgebra/MatrixMultiplication/AuxiliarySeparation/Separation/Basic.lean

The tensor map with exactly 5M copies

`OAI/LinearAlgebra/MatrixMultiplication/AuxiliarySeparation/Separation/Basic.lean`

The tensor map with exactly `5M` copies