ImmSecondLocalBound.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem335.immNormalizedMatrix_second_trace_le_localPolynomial_sum line 14
Source documentation
The actual finite normalized IMM second trace is bounded by the sum of the compatible local occupation-polynomial products. This has no source-validity, moment, or nonempty-index assumptions.
```
theorem immNormalizedMatrix_second_trace_le_localPolynomial_sum
    (n : ℕ) (hn : 0 < n) (side : Fin n → Bool) (a b : ℕ) :
    let A := immNormalizedMatrix n side a b
…
```
Mentions: OAI.Problem335.immNormalizedMatrix