A weighted determinant polynomial with satellites

MathlibAnnex.Satellite.satellitePolynomial

def

Adds linear row-replacement contributions to a base determinant.

Statement

Let , with reference sup norm, and a finite index set. Let be a family of continuous real linear functionals on , and another such family. Choose and coefficients . Let be the standard coordinate vectors. Put and replace row by when writing .

Definition

The full defining expression is Both sums are finite. If is empty, only remains. If , the empty determinant is and the inner sum is empty, so the value is .

Assumptions

Only the finite indices, the real weight, coefficient vectors and the two families of continuous linear functionals are inputs. There is no norm model , contraction condition, positive-weight hypothesis or invertibility hypothesis.

Conclusion

The definition returns the scalar . The satellites are additional dual functionals, not vectors or points of a net.

The private coordinate and row-replacement aliases in the exact local aliases identify reference vectors, frame rows, and standard-basis matrices. They do not restrict the defining polynomial to admissible configurations; such a restriction is imposed only in later theorems.

def satellitePolynomial {n : ℕ} {J : Type*} [Fintype J]
    (weight : ℝ) (coeff : J → Coord n)
    (B : DualFrame n) (sat : J → (Coord n →L[ℝ] ℝ)) : ℝ :=
  weight * frameDet B +
    ∑ a : J, ∑ i : Fin n, coeff a i * replacementDet B i (sat a)

private abbrev Coord (n : ℕ) := Fin n → ℝ

private abbrev DualFrame (n : ℕ) := DeterminantFrame.Frame n (Coord n)
private abbrev dualFrameMatrix {n : ℕ} := DeterminantFrame.frameMatrix (Pi.basisFun ℝ (Fin n))
private abbrev frameDet {n : ℕ} := DeterminantFrame.frameDeterminant (Pi.basisFun ℝ (Fin n))
private abbrev replacementDet {n : ℕ} := DeterminantFrame.replacementDeterminant (Pi.basisFun ℝ (Fin n))

Read exact source with highlighted declaration · Raw UTF-8 source · Card PDF · Back to Project