Catalyst.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Catalysts from additive completion certificates

Equality in the Grothendieck additive group means equality after adding a common element of the original semiring. This gives catalytic inequalities without assuming additive cancellation.

theorem OAI.MatrixMultiplication.AuxiliarySeparation.exists_catalyst_of_completion_eq line 22

Source documentation

A negative-unit certificate in the additive completion gives a catalytic inequality in the original semiring, even when its addition is not cancellative.

theorem exists_catalyst_of_completion_eq
    (hadd : ∀ a b c d : S, a ≤ b → c ≤ d → a + c ≤ b + d)
    (m k : ℕ) (d X Y s : S) (hXY : X ≤ Y)
    (heq : -(m : ℤ) • GrothendieckAddGroup.of (1 : S) =
      GrothendieckAddGroup.of Y - GrothendieckAddGroup.of X +
        GrothendieckAddGroup.of (d * s) - k • GrothendieckAddGroup.of s) :
    ∃ D : S, D + (m : S) + d * s ≤ D + (k : S) * s := by
…

theorem OAI.MatrixMultiplication.AuxiliarySeparation.exists_catalyst_of_completion_sum_eq line 56

Source documentation

A finite nonnegative integral combination of completion relations gives one catalytic inequality. The catalyst absorbs the aggregate of the ordered relations, and the resulting test element is the same combination of the original test elements.

theorem exists_catalyst_of_completion_sum_eq
    (hadd : ∀ a b c d : S, a ≤ b → c ≤ d → a + c ≤ b + d)
    {I : Type*} [Fintype I] (m k : ℕ) (d : S)
    (n : I → ℕ) (X Y Z : I → S) (hXY : ∀ i, X i ≤ Y i)
    (heq : -(m : ℤ) • GrothendieckAddGroup.of (1 : S) =
      ∑ i, n i • (GrothendieckAddGroup.of (Y i) - GrothendieckAddGroup.of (X i) +
        GrothendieckAddGroup.of (d * Z i) - k • GrothendieckAddGroup.of (Z i))) :
    ∃ D : S, D + (m : S) + d * (∑ i, n i • Z i) ≤
      D + (k : S) * (∑ i, n i • Z i) := by
…