SparseMask.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Finite support estimates for mask differences. The label type is retained even when the products s_i collide.

def OAI.Dixmier.rowOnes line 14
def OAI.Dixmier.columnZeros line 17
def OAI.Dixmier.rowDifference line 20
def OAI.Dixmier.columnDifference line 23
theorem OAI.Dixmier.bool_ne_true_union line 27
theorem OAI.Dixmier.bool_ne_false_union line 30
theorem OAI.Dixmier.rowDifference_subset line 34
Source documentation
A row difference is supported on the union of the two one-sets.
```
theorem rowDifference_subset (a : G → I → Bool) (g x : G) :
    rowDifference a g x ⊆ rowOnes a x ∪ rowOnes a (g⁻¹ * x) := by
…
```
Mentions: OAI.Dixmier.rowDifference, OAI.Dixmier.rowOnes
theorem OAI.Dixmier.columnDifference_subset line 41
Source documentation
Column support uses zero-sets at y and g⁻¹y.
```
theorem columnDifference_subset (a : G → I → Bool) (s : I → G) (g y : G) :
    columnDifference a s g y ⊆ columnZeros a s y ∪ columnZeros a s (g⁻¹ * y) := by
…
```
Mentions: OAI.Dixmier.columnDifference, OAI.Dixmier.columnZeros
theorem OAI.Dixmier.rowDifference_card_le line 49
Source documentation
The row support bound p=min(2r,n), without distinctness of group products.
```
theorem rowDifference_card_le (a : G → I → Bool) (r : ℕ)
    (hr : ∀ x, (rowOnes a x).card ≤ r) (g x : G) :
    (rowDifference a g x).card ≤ min (2 * r) (Fintype.card I) := by
…
```
Mentions: OAI.Dixmier.rowOnes, OAI.Dixmier.rowDifference

theorem OAI.Dixmier.columnDifference_card_le line 61

Source documentation

The column support bound p=min(2r,n).

theorem columnDifference_card_le (a : G → I → Bool) (s : I → G) (r : ℕ)
    (hc : ∀ y, (columnZeros a s y).card ≤ r) (g y : G) :
    (columnDifference a s g y).card ≤ min (2 * r) (Fintype.card I) := by
…

Mentions: OAI.Dixmier.columnZeros, OAI.Dixmier.columnDifference

def OAI.Dixmier.boolComplex line 73
theorem OAI.Dixmier.difference_mask_norm line 76
Source documentation
The scalar difference mask has absolute value at most one.
```
theorem difference_mask_norm (b c : Bool) : ‖boolComplex b - boolComplex c‖ ≤ 1 := by
…
```
Mentions: OAI.Dixmier.boolComplex
theorem OAI.Dixmier.difference_mask_ne_zero line 80
Source documentation
Nonzero complex mask coefficients correspond exactly to unequal bits.
```
theorem difference_mask_ne_zero (b c : Bool) :
    boolComplex b - boolComplex c ≠ 0 ↔ b ≠ c := by
…
```
Mentions: OAI.Dixmier.boolComplex