Laws.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The determinant filtration uses an arbitrary binary law, while the three-sector filtration uses the uniform law on three branches.

def OAI.MatrixMultiplication.AuxiliarySeparation.binaryLaw line 23
Source documentation
The common binary probability law used for every permuted character.
```
def binaryLaw (q : ℝ) (hq₀ : 0 ≤ q) (hq₁ : q ≤ 1) : FiniteLaw (Fin 2) where
…
```
theorem OAI.MatrixMultiplication.AuxiliarySeparation.binaryLaw_zero line 31
theorem OAI.MatrixMultiplication.AuxiliarySeparation.binaryLaw_one line 34
theorem OAI.MatrixMultiplication.AuxiliarySeparation.binaryLaw_entropy line 38
Source documentation
The finite-law entropy agrees exactly with the binary entropy convention.
```
theorem binaryLaw_entropy (q : ℝ) (hq₀ : 0 ≤ q) (hq₁ : q ≤ 1) :
    finiteEntropy (binaryLaw q hq₀ hq₁).mass = Real.binEntropy q := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.binaryLaw
theorem OAI.MatrixMultiplication.AuxiliarySeparation.binaryLaw_product line 43
theorem OAI.MatrixMultiplication.AuxiliarySeparation.uniformThree_entropy_factor line 48
Source documentation
The three-sector entropy factor is 3 ^ p.
```
theorem uniformThree_entropy_factor (p : ℝ) :
    Real.exp (p * finiteEntropy (FiniteLaw.uniform (Fin 3)).mass) = (3 : ℝ) ^ p := by
…
```
theorem OAI.MatrixMultiplication.AuxiliarySeparation.uniformThree_product line 56