NormalizedStates.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

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.

def OAI.MatrixMultiplication.AuxiliarySeparation.normalizedStates line 23
Source documentation
Additive restriction-monotone states with a fixed detector inequality.
```
def normalizedStates (R : S → ℝ) (d : S) (k : ℝ) : Set (S → ℝ) :=
…
```
theorem OAI.MatrixMultiplication.AuxiliarySeparation.normalizedStates_isClosed line 29
theorem OAI.MatrixMultiplication.AuxiliarySeparation.normalizedStates_isCompact line 55
theorem OAI.MatrixMultiplication.AuxiliarySeparation.normalizedStates_convex line 62
theorem OAI.MatrixMultiplication.AuxiliarySeparation.state_zero line 93
theorem OAI.MatrixMultiplication.AuxiliarySeparation.state_nat_mul line 99
theorem OAI.MatrixMultiplication.AuxiliarySeparation.state_one_le line 109
theorem OAI.MatrixMultiplication.AuxiliarySeparation.state_rescale line 116
Source documentation
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.
```
theorem state_rescale {R : S → ℕ} {d : S} {k : ℝ} {f : S → ℝ}
    (hf : f ∈ normalizedStates (fun x => (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 : S) * z) :
    (fun x => f (z * x) / f z) ∈ normalizedStates (fun x => (R x : ℝ)) d k := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.normalizedStates