Documentation

LeanPool.HighContrastHomogenization.Provider.Regularity.FiniteAffineSlopeMatrix

High-contrast homogenization: Provider.Regularity.FiniteAffineSlopeMatrix #

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

Matrix realization of finite affine best-fit slopes #

This module represents the finite-solution best-fit slope endomorphism by a matrix and constructs its inverse only from an explicit bijectivity proof. Quantitative good-event estimates and slope-family iteration are separate.

source
noncomputable def HCPolySupport.HighContrast.finiteAffineBestFitSlopeMatrix {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (k m : ℤ) (hkm : k ≤ m) :
Mat d

Matrix of the finite-solution best-fit slope endomorphism.

Equations
Instances For
    source
    @[simp]
    theorem HCPolySupport.HighContrast.finiteAffineBestFitSlopeMatrix_apply {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (k m : ℤ) (hkm : k ≤ m) (e : Vec d) :
    matVecMul (finiteAffineBestFitSlopeMatrix a k m hkm) e = (finiteAffineBestFitSlope a k m hkm) e

    The slope matrix acts with the same column-vector orientation as the underlying linear map.

    source
    theorem HCPolySupport.HighContrast.finiteAffineBestFitSlopeMatrix_isUnit_det_iff_injective {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (k m : ℤ) (hkm : k ≤ m) :
    IsUnit (Matrix.det (finiteAffineBestFitSlopeMatrix a k m hkm)) ↔ Function.Injective ⇑(finiteAffineBestFitSlope a k m hkm)

    The slope matrix has unit determinant exactly when the slope map is injective.

    source
    theorem HCPolySupport.HighContrast.finiteAffineBestFitSlopeMatrix_isUnit_det_iff_bijective {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (k m : ℤ) (hkm : k ≤ m) :
    IsUnit (Matrix.det (finiteAffineBestFitSlopeMatrix a k m hkm)) ↔ Function.Bijective ⇑(finiteAffineBestFitSlope a k m hkm)

    In finite dimension, the determinant gate is equivalently bijectivity of the finite-solution best-fit slope map.

    source
    noncomputable def HCPolySupport.HighContrast.finiteAffineBestFitSlopeEquiv {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (k m : ℤ) (hkm : k ≤ m) (hbij : Function.Bijective ⇑(finiteAffineBestFitSlope a k m hkm)) :
    Vec d ≃ₗ[ℝ] Vec d

    The linear equivalence supplied by a proved bijective best-fit slope map. This declaration is the first inverse-bearing object in the module.

    Equations
    Instances For
      source
      noncomputable def HCPolySupport.HighContrast.finiteAffineBestFitSlopeInverseLinearMap {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (k m : ℤ) (hkm : k ≤ m) (hbij : Function.Bijective ⇑(finiteAffineBestFitSlope a k m hkm)) :
      Vec d →ₗ[ℝ] Vec d

      Inverse linear map of a proved bijective finite-solution best-fit slope map.

      Equations
      Instances For
        source
        noncomputable def HCPolySupport.HighContrast.finiteAffineBestFitSlopeInverseMatrix {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (k m : ℤ) (hkm : k ≤ m) (hbij : Function.Bijective ⇑(finiteAffineBestFitSlope a k m hkm)) :
        Mat d

        Matrix of the proof-gated inverse slope map.

        Equations
        Instances For
          source
          @[simp]
          theorem HCPolySupport.HighContrast.finiteAffineBestFitSlopeInverseMatrix_apply {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (k m : ℤ) (hkm : k ≤ m) (hbij : Function.Bijective ⇑(finiteAffineBestFitSlope a k m hkm)) (e : Vec d) :
          matVecMul (finiteAffineBestFitSlopeInverseMatrix a k m hkm hbij) e = (finiteAffineBestFitSlopeInverseLinearMap a k m hkm hbij) e

          The inverse slope matrix acts as the inverse linear map.

          source
          theorem HCPolySupport.HighContrast.finiteAffineBestFitSlope_apply_inverseMatrix {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (k m : ℤ) (hkm : k ≤ m) (hbij : Function.Bijective ⇑(finiteAffineBestFitSlope a k m hkm)) (e : Vec d) :
          (finiteAffineBestFitSlope a k m hkm) (matVecMul (finiteAffineBestFitSlopeInverseMatrix a k m hkm hbij) e) = e

          Applying the slope map after its proof-gated inverse recovers the slope.

          source
          @[simp]
          theorem HCPolySupport.HighContrast.finiteAffineBestFitSlopeMatrix_mul_inverseMatrix {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (k m : ℤ) (hkm : k ≤ m) (hbij : Function.Bijective ⇑(finiteAffineBestFitSlope a k m hkm)) :
          finiteAffineBestFitSlopeMatrix a k m hkm * finiteAffineBestFitSlopeInverseMatrix a k m hkm hbij = 1

          The slope matrix times its proof-gated inverse matrix is the identity.

          source
          @[simp]
          theorem HCPolySupport.HighContrast.finiteAffineBestFitSlopeInverseMatrix_mul_matrix {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (k m : ℤ) (hkm : k ≤ m) (hbij : Function.Bijective ⇑(finiteAffineBestFitSlope a k m hkm)) :
          finiteAffineBestFitSlopeInverseMatrix a k m hkm hbij * finiteAffineBestFitSlopeMatrix a k m hkm = 1

          The proof-gated inverse matrix times the slope matrix is the identity.

          source
          theorem HCPolySupport.HighContrast.finiteAffineBestFitSlopeInverseMatrix_isUnit_det {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (k m : ℤ) (hkm : k ≤ m) (hbij : Function.Bijective ⇑(finiteAffineBestFitSlope a k m hkm)) :
          IsUnit (Matrix.det (finiteAffineBestFitSlopeInverseMatrix a k m hkm hbij))

          A proof-gated inverse slope matrix also has unit determinant.