Triangular.lean`

26 declarations, 0 contain sorry, 0 declared as axioms

Triangular monotonicity, 05-corners:116–209. The arbitrary block-copy basis change is paid on both sides and cancels exactly, not estimated or assumed free.

theorem OAI.ExactFourier.MatrixPrice.triangular_experiment_bound line 15

theorem OAI.ExactFourier.MatrixPrice.upper_triangular line 33

Source documentation

The literal upper block triangular conclusion, including empty blocks.

theorem upper_triangular (M : Matrix α α ℂ) (C : Matrix α β ℂ)
    (D : Matrix β β ℂ) (hM : IsUnit M) (hD : IsUnit D) :
    p.value M + p.value D ≤ p.value (Matrix.fromBlocks M C 0 D) := by
…

theorem OAI.ExactFourier.MatrixPrice.lower_triangular line 58
def OAI.ExactFourier.CoefficientTime.truncMatrix line 85
theorem OAI.ExactFourier.CoefficientTime.truncMatrix_one line 89
theorem OAI.ExactFourier.CoefficientTime.truncMatrix_zero line 102
theorem OAI.ExactFourier.CoefficientTime.truncMatrix_add line 107
theorem OAI.ExactFourier.CoefficientTime.truncMatrix_mul line 112
def OAI.ExactFourier.CoefficientTime.truncHom line 163
Source documentation
Multiplication modulo z^t in the coefficient basis is a literal ring homomorphism.
```
noncomputable def truncHom {R : Type*} [Semiring R] (t : ℕ) :
    PowerSeries R →+* Matrix (Fin t) (Fin t) R where
…
```
theorem OAI.ExactFourier.CoefficientTime.trunc_isUnit line 172
Source documentation
Repeated invertible constant term makes the time coefficient matrix invertible.
```
theorem trunc_isUnit {R : Type*} [Ring R] (t : ℕ) (F : PowerSeries R)
    (hF : IsUnit (PowerSeries.constantCoeff F)) : IsUnit (truncMatrix t F) :=
…
```
Mentions: OAI.ExactFourier.CoefficientTime.truncMatrix
def OAI.ExactFourier.CoefficientTime.blockTruncHom line 176
theorem OAI.ExactFourier.CoefficientTime.blockTruncHom_apply line 181
theorem OAI.ExactFourier.CoefficientTime.blockTrunc_isUnit line 186
theorem OAI.ExactFourier.CoefficientTime.coeff_mul_truncated line 196
def OAI.ExactFourier.CoefficientTime.coefficientColumns line 205
theorem OAI.ExactFourier.CoefficientTime.blocks_mul_columns line 211
Source documentation
A matrix series acts on vectors of truncated coefficients by the literal coefficient product. This is the state-response and boundary-quotient interface.
```
theorem blocks_mul_columns {ι κ : Type*} [Fintype ι] [DecidableEq ι] (t : ℕ)
    (F : Matrix ι ι (PowerSeries ℂ)) (V : Matrix ι κ (PowerSeries ℂ)) :
    blockTruncHom t F * coefficientColumns t V = coefficientColumns t (F*V) := by
…
```
Mentions: OAI.ExactFourier.CoefficientTime.blockTruncHom, OAI.ExactFourier.CoefficientTime.coefficientColumns
theorem OAI.ExactFourier.CoefficientTime.blockTrunc_scalar line 221
Source documentation
The scalar Toeplitz factor acts identically on every spatial coordinate.
```
theorem blockTrunc_scalar {ι : Type*} [Fintype ι] [DecidableEq ι] (t : ℕ)
    (f : PowerSeries ℂ) :
    blockTruncHom t (Matrix.scalar ι f) = truncMatrix t f ⊗ₖ (1 : Matrix ι ι ℂ) := by
…
```
Mentions: OAI.ExactFourier.CoefficientTime.blockTruncHom, OAI.ExactFourier.CoefficientTime.truncMatrix
def OAI.ExactFourier.CoefficientTime.prefixScalar line 232
Source documentation
The scalar prefix change of basis leaves the suffix literally fixed. Its prefix-to-suffix block is zero because the convolution is lower triangular.
```
noncomputable def prefixScalar (t T : ℕ) (f : PowerSeries ℂ) :
    Matrix (Fin t) (Fin t) ℂ := fun a b =>
…
```
theorem OAI.ExactFourier.CoefficientTime.prefixScalar_one line 236
theorem OAI.ExactFourier.CoefficientTime.prefixScalar_mul line 241
theorem OAI.ExactFourier.CoefficientTime.prefixScalar_isUnit line 259

theorem OAI.ExactFourier.CoefficientTime.prefix_mul_columns line 269

Source documentation

On an early row the partial scalar convolution is a full coefficient convolution; on a late row it leaves the original series coefficient unchanged.

theorem prefix_mul_columns {ι κ : Type*} [Fintype ι] [DecidableEq ι]
    (t T : ℕ) (f : PowerSeries ℂ) (V : Matrix ι κ (PowerSeries ℂ))
    (a : Fin t × ι) (b : κ) :
    ((prefixScalar t T f ⊗ₖ (1 : Matrix ι ι ℂ)) * coefficientColumns t V) a b =
      if a.1.val < T then PowerSeries.coeff a.1.val (f * V a.2 b)
      else PowerSeries.coeff a.1.val (V a.2 b) := by
…

Mentions: OAI.ExactFourier.CoefficientTime.prefixScalar, OAI.ExactFourier.CoefficientTime.coefficientColumns

theorem OAI.ExactFourier.CoefficientTime.zero_prefix_columns_mul line 287
def OAI.ExactFourier.timeSplit line 313
theorem OAI.ExactFourier.MatrixPrice.blocks_lower line 324
theorem OAI.ExactFourier.MatrixPrice.trunc_lower_bound line 365