Weights.lean`

39 declarations, 0 contain sorry, 0 declared as axioms

Interval weights for the three-sector convolution degeneration

Section 5.2 assigns weights to the second and third coordinates of C(a, 3 * h + a - 1). The total weight is nonnegative on convolution support, and its zero set consists exactly of the three matching sector blocks. The middle block is a convolution with the last two legs exchanged and the first coordinate reversed.

def OAI.MatrixMultiplication.AuxiliarySeparation.Sector.sourceWidth line 19
Source documentation
Number of second-leg coordinates in the original convolution.
```
def sourceWidth (a h : ℕ) : ℕ := 3 * h + a - 1
```
def OAI.MatrixMultiplication.AuxiliarySeparation.Sector.rightStart line 22
Source documentation
Beginning of the right sector on both the second and third legs.
```
def rightStart (a h : ℕ) : ℕ := 2 * h + a - 1
```
def OAI.MatrixMultiplication.AuxiliarySeparation.Sector.Support line 25
Source documentation
A coefficient-one term of the original convolution tensor.
```
def Support (a h i j k : ℕ) : Prop :=
…
```
def OAI.MatrixMultiplication.AuxiliarySeparation.Sector.MiddleY line 29
Source documentation
The middle interval on the second tensor leg.
```
def MiddleY (a h j : ℕ) : Prop := h ≤ j ∧ j < rightStart a h
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Sector.rightStart
def OAI.MatrixMultiplication.AuxiliarySeparation.Sector.MiddleZ line 32
Source documentation
The middle interval on the third tensor leg.
```
def MiddleZ (a h k : ℕ) : Prop := h + a - 1 ≤ k ∧ k < rightStart a h
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Sector.rightStart
instance OAI.MatrixMultiplication.AuxiliarySeparation.Sector.(instance at line 34) line 34
instance OAI.MatrixMultiplication.AuxiliarySeparation.Sector.(instance at line 37) line 37
def OAI.MatrixMultiplication.AuxiliarySeparation.Sector.firstWeight line 41
Source documentation
No weight is assigned to the common first leg.
```
def firstWeight (_i : ℕ) : ℤ := 0
```
def OAI.MatrixMultiplication.AuxiliarySeparation.Sector.secondWeight line 44
Source documentation
Weight one on the middle second-leg interval, zero elsewhere.
```
def secondWeight (a h j : ℕ) : ℤ := if MiddleY a h j then 1 else 0
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Sector.MiddleY
def OAI.MatrixMultiplication.AuxiliarySeparation.Sector.thirdWeight line 47
Source documentation
Weight minus one on the middle third-leg interval, zero elsewhere.
```
def thirdWeight (a h k : ℕ) : ℤ := if MiddleZ a h k then -1 else 0
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Sector.MiddleZ
def OAI.MatrixMultiplication.AuxiliarySeparation.Sector.totalWeight line 50
Source documentation
Exponent of the degeneration parameter on one term.
```
def totalWeight (a h i j k : ℕ) : ℤ :=
…
```
def OAI.MatrixMultiplication.AuxiliarySeparation.Sector.MatchingSectors line 54
Source documentation
The three retained blocks have matching sector labels.
```
def MatchingSectors (a h j k : ℕ) : Prop :=
…
```
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Sector.middleY_of_middleZ line 60
Source documentation
A middle third-leg coordinate can only be reached from the middle second leg.
```
theorem middleY_of_middleZ {a h i j k : ℕ}
    (hs : Support a h i j k) (hz : MiddleZ a h k) : MiddleY a h j := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Sector.Support, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.MiddleZ, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.MiddleY
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Sector.totalWeight_eq_zero_or_one line 67
Source documentation
Every term has exponent zero or one, so no negative powers occur.
```
theorem totalWeight_eq_zero_or_one {a h i j k : ℕ}
    (hs : Support a h i j k) :
    totalWeight a h i j k = 0 ∨ totalWeight a h i j k = 1 := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Sector.Support, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.totalWeight
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Sector.totalWeight_nonneg line 74
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Sector.totalWeight_eq_zero_iff line 79
Source documentation
The constant coefficient consists exactly of the three matching blocks.
```
theorem totalWeight_eq_zero_iff {a h i j k : ℕ}
    (hs : Support a h i j k) :
    totalWeight a h i j k = 0 ↔ MatchingSectors a h j k := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Sector.Support, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.totalWeight, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.MatchingSectors
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Sector.totalWeight_eq_one_iff line 89
Source documentation
Only a middle second-leg coordinate paired with an outer third-leg coordinate is erased by the degeneration.
```
theorem totalWeight_eq_one_iff {a h i j k : ℕ}
    (hs : Support a h i j k) :
    totalWeight a h i j k = 1 ↔ MiddleY a h j ∧ ¬ MiddleZ a h k := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Sector.Support, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.totalWeight, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.MiddleY, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.MiddleZ
def OAI.MatrixMultiplication.AuxiliarySeparation.Sector.LeftBranch line 97
Source documentation
Parametrization of the left copy of C(a,h).
```
def LeftBranch (a h i j k : ℕ) : Prop :=
…
```
def OAI.MatrixMultiplication.AuxiliarySeparation.Sector.MiddleBranch line 101
Source documentation
Parametrization of the middle copy with the second and third legs exchanged.
```
def MiddleBranch (a h i j k : ℕ) : Prop :=
…
```
def OAI.MatrixMultiplication.AuxiliarySeparation.Sector.RightBranch line 106
Source documentation
Parametrization of the right translated copy of C(a,h).
```
def RightBranch (a h i j k : ℕ) : Prop :=
…
```
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Sector.leftBranch_iff line 111
Source documentation
The left block preserves the actual first coordinate.
```
theorem leftBranch_iff {a h i j k : ℕ} (hs : Support a h i j k) :
    LeftBranch a h i j k ↔ j < h ∧ k < h + a - 1 := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Sector.Support, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.LeftBranch
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Sector.middleBranch_iff line 122
Source documentation
The middle support equation becomes convolution after reversing the first coordinate and exchanging the second and third legs.
```
theorem middleBranch_iff {a h i j k : ℕ} (hs : Support a h i j k) :
    MiddleBranch a h i j k ↔ MiddleY a h j ∧ MiddleZ a h k := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Sector.Support, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.MiddleBranch, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.MiddleY, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.MiddleZ
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Sector.rightBranch_iff line 134
Source documentation
The right block is the same convolution after translating the two outer coordinates.
```
theorem rightBranch_iff {a h i j k : ℕ} (hs : Support a h i j k) :
    RightBranch a h i j k ↔ rightStart a h ≤ j ∧ rightStart a h ≤ k := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Sector.Support, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.RightBranch, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.rightStart
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Sector.left_support_coordinates line 147
Source documentation
On the left coordinate block, the support equation is the ordinary convolution equation.
```
theorem left_support_coordinates {a h i r s : ℕ} (hi : i < a) (hr : r < h) :
    Support a h i r s ↔ s = i + r := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Sector.Support
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Sector.right_support_coordinates line 153
Source documentation
Translation of the right block preserves the convolution equation.
```
theorem right_support_coordinates {a h i r s : ℕ} (hi : i < a) (hr : r < h) :
    Support a h i (rightStart a h + r) (rightStart a h + s) ↔ s = i + r := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Sector.Support, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.rightStart
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Sector.middle_support_coordinates line 160
Source documentation
In middle-block coordinates the support equation is convolution with the first coordinate reversed and the other two coordinates exchanged.
```
theorem middle_support_coordinates {a h i s r : ℕ}
    (hi : i < a) (hr : r < h) :
    Support a h i (h + s) (h + a - 1 + r) ↔ s = a - 1 - i + r := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Sector.Support
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Sector.retained_support_iff line 167
Source documentation
Exact retained support of the three-sector degeneration.
```
theorem retained_support_iff {a h i j k : ℕ} (hs : Support a h i j k) :
    totalWeight a h i j k = 0 ↔
      LeftBranch a h i j k ∨ MiddleBranch a h i j k ∨ RightBranch a h i j k := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Sector.Support, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.totalWeight, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.LeftBranch, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.MiddleBranch, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.RightBranch
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Sector.LeftBranch.support line 175
Source documentation
Every displayed left-branch term belongs to the original convolution.
```
theorem LeftBranch.support {a h i j k : ℕ} (hb : LeftBranch a h i j k) :
    Support a h i j k := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Sector.LeftBranch, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.Support
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Sector.MiddleBranch.support line 182
Source documentation
Every displayed middle-branch term belongs to the original convolution.
```
theorem MiddleBranch.support {a h i j k : ℕ} (hb : MiddleBranch a h i j k) :
    Support a h i j k := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Sector.MiddleBranch, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.Support
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Sector.RightBranch.support line 189
Source documentation
Every displayed right-branch term belongs to the original convolution.
```
theorem RightBranch.support {a h i j k : ℕ} (hb : RightBranch a h i j k) :
    Support a h i j k := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Sector.RightBranch, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.Support
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Sector.support_and_weight_zero_iff line 197
Source documentation
Exact equality of the retained support and the three explicitly parametrized convolution branches, without a pre-existing support assumption.
```
theorem support_and_weight_zero_iff (a h i j k : ℕ) :
    (Support a h i j k ∧ totalWeight a h i j k = 0) ↔
      LeftBranch a h i j k ∨ MiddleBranch a h i j k ∨ RightBranch a h i j k := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Sector.Support, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.totalWeight, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.LeftBranch, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.MiddleBranch, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.RightBranch
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Sector.reverse_reverse line 209
Source documentation
The first-coordinate reversal is involutive on its natural range.
```
theorem reverse_reverse {a u : ℕ} (hu : u < a) :
    a - 1 - (a - 1 - u) = u := by
…
```

theorem OAI.MatrixMultiplication.AuxiliarySeparation.Sector.middleBranch_coordinates_unique line 214

Source documentation

The middle branch has unique reversed-convolution coordinates.

theorem middleBranch_coordinates_unique {a h i k u r u' r' : ℕ}
    (hu : u < a) (hu' : u' < a)
    (hi : i = a - 1 - u) (hi' : i = a - 1 - u')
    (hk : k = h + a - 1 + r) (hk' : k = h + a - 1 + r') :
    u = u' ∧ r = r' := by
…

theorem OAI.MatrixMultiplication.AuxiliarySeparation.Sector.leftBranch_not_middleBranch line 222
Source documentation
The left and middle branches use disjoint second-leg coordinates.
```
theorem leftBranch_not_middleBranch {a h i j k : ℕ}
    (hl : LeftBranch a h i j k) : ¬ MiddleBranch a h i j k := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Sector.LeftBranch, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.MiddleBranch
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Sector.leftBranch_not_rightBranch line 231
Source documentation
The left and right branches use disjoint second-leg coordinates.
```
theorem leftBranch_not_rightBranch {a h i j k : ℕ}
    (hl : LeftBranch a h i j k) : ¬ RightBranch a h i j k := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Sector.LeftBranch, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.RightBranch
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Sector.middleBranch_not_rightBranch line 241
Source documentation
The middle and right branches use disjoint second-leg coordinates.
```
theorem middleBranch_not_rightBranch {a h i j k : ℕ}
    (hm : MiddleBranch a h i j k) : ¬ RightBranch a h i j k := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Sector.MiddleBranch, OAI.MatrixMultiplication.AuxiliarySeparation.Sector.RightBranch
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Sector.leftBranch_nonempty line 250
Source documentation
Positivity of the two original dimensions makes the left branch nonempty.
```
theorem leftBranch_nonempty {a h : ℕ} (ha : 0 < a) (hh : 0 < h) :
    ∃ i j k, LeftBranch a h i j k :=
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Sector.LeftBranch
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Sector.middleBranch_nonempty line 255
Source documentation
Positivity makes the exchanged middle branch nonempty as well.
```
theorem middleBranch_nonempty {a h : ℕ} (ha : 0 < a) (hh : 0 < h) :
    ∃ i j k, MiddleBranch a h i j k := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Sector.MiddleBranch
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Sector.rightBranch_nonempty line 260
Source documentation
Positivity also makes the translated right branch nonempty.
```
theorem rightBranch_nonempty {a h : ℕ} (ha : 0 < a) (hh : 0 < h) :
    ∃ i j k, RightBranch a h i j k := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Sector.RightBranch