Documentation

LeanPool.MatrixMultiplicationAllFields.LinearAlgebra.MatrixMultiplication.AuxiliarySeparation.Spectrum.NormalizedStates

Compact convex spaces of normalized additive states #

These are the closed linear constraints in Appendix A. The nonemptiness of this state space, and its instantiation by the tensor restriction semiring, are separate statements.

source
def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.normalizedStates {S : Type u_1} [CommSemiring S] [Preorder S] (R : S → ℝ) (d : S) (k : ℝ) :
Set (S → ℝ)

Additive restriction-monotone states with a fixed detector inequality.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.normalizedStates_isClosed {S : Type u_1} [CommSemiring S] [Preorder S] (R : S → ℝ) (d : S) (k : ℝ) :
    IsClosed (normalizedStates R d k)
    source
    theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.normalizedStates_isCompact {S : Type u_1} [CommSemiring S] [Preorder S] (R : S → ℝ) (d : S) (k : ℝ) :
    IsCompact (normalizedStates R d k)
    source
    theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.normalizedStates_convex {S : Type u_1} [CommSemiring S] [Preorder S] (R : S → ℝ) (d : S) (k : ℝ) :
    Convex ℝ (normalizedStates R d k)
    source
    theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.state_zero {S : Type u_1} [CommSemiring S] [Preorder S] {R : S → ℝ} {d : S} {k : ℝ} {f : S → ℝ} (hf : f ∈ normalizedStates R d k) :
    f 0 = 0
    source
    theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.state_nat_mul {S : Type u_1} [CommSemiring S] [Preorder S] {R : S → ℝ} {d : S} {k : ℝ} {f : S → ℝ} (hf : f ∈ normalizedStates R d k) (n : ℕ) (x : S) :
    f (↑n * x) = ↑n * f x
    source
    theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.state_one_le {S : Type u_1} [CommSemiring S] [Preorder S] {R : S → ℝ} {d : S} {k : ℝ} {f : S → ℝ} (hf : f ∈ normalizedStates R d k) {z : S} (hz : 1 ≤ z) :
    1 ≤ f z
    source
    theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.state_rescale {S : Type u_1} [CommSemiring S] [Preorder S] {R : S → ℕ} {d : S} {k : ℝ} {f : S → ℝ} (hf : f ∈ normalizedStates (fun (x : S) => ↑(R x)) d k) (z : S) (hz : 1 ≤ z) (hmulmono : ∀ (x y : S), x ≤ y → z * x ≤ z * y) (hdom : ∀ (x : S), z * x ≤ ↑(R x) * z) :
    (fun (x : S) => f (z * x) / f z) ∈ normalizedStates (fun (x : S) => ↑(R x)) d k

    Translation followed by normalization preserves every state constraint. The two order hypotheses are exactly those supplied by tensor multiplication and the finite rank bound in the restriction semiring.