Regular.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

Regular convolution operators, product lists with multiplicity, and sparse splitting from a contracting average.

def OAI.Dixmier.reindexL2 line 17
theorem OAI.Dixmier.reindexL2_apply line 20
theorem OAI.Dixmier.l2_norm_sq line 23
theorem OAI.Dixmier.reindexL2_norm line 26
def OAI.Dixmier.reindexIsometry line 32
def OAI.Dixmier.rightRegular line 41
Source documentation
The right regular representation R_t ξ(x)=ξ(xt).
```
def rightRegular : G →* (ScalarL2 G →L[ℂ] ScalarL2 G) where
…
```
Mentions: OAI.Dixmier.ScalarL2
theorem OAI.Dixmier.rightRegular_apply line 46
theorem OAI.Dixmier.rightRegular_norm_map line 49
def OAI.Dixmier.leftRegular line 53
Source documentation
Left regular operators U_g commute with the right regular operators.
```
def leftRegular : G →* (ScalarL2 G →L[ℂ] ScalarL2 G) where
…
```
Mentions: OAI.Dixmier.ScalarL2
theorem OAI.Dixmier.leftRegular_apply line 58
theorem OAI.Dixmier.left_right_commute line 61
def OAI.Dixmier.Word line 66
instance OAI.Dixmier.wordFintype line 70
def OAI.Dixmier.wordProduct line 76
theorem OAI.Dixmier.word_card line 80

theorem OAI.Dixmier.sum_wordProduct line 91

Source documentation

Product lists are indexed by words, not by their possibly colliding values.

theorem sum_wordProduct {I R : Type*} [Fintype I] [Semiring R]
    (s : I → G) (φ : G →* R) (n : ℕ) :
    (∑ w : Word I n, φ (wordProduct s n w)) = (∑ i, φ (s i)) ^ n := by
…

Mentions: OAI.Dixmier.Word, OAI.Dixmier.wordProduct

theorem OAI.Dixmier.sparse_mask_for_words line 104

Source documentation

Sparse splitting for words from a norm bound on the finite average.

theorem sparse_mask_for_words {I : Type*} [Fintype I] (s : I → G)
    {ρ : ℝ} (_hρ : 0 ≤ ρ)
    (havg : ‖∑ i, rightRegular (s i)‖ ≤ (Fintype.card I : ℝ) * ρ) (ℓ : ℕ) (hℓ : 0 < ℓ) :
    ∃ a : G → Word I ℓ → Bool,
      (∀ x, (rowOnes a x).card ≤ ⌈(Fintype.card I : ℝ) ^ ℓ * ρ ^ ℓ⌉₊) ∧
      ∀ y, (columnZeros a (wordProduct s ℓ) y).card ≤
        ⌈(Fintype.card I : ℝ) ^ ℓ * ρ ^ ℓ⌉₊ := by
…

Mentions: OAI.Dixmier.rightRegular, OAI.Dixmier.Word, OAI.Dixmier.rowOnes, OAI.Dixmier.columnZeros, OAI.Dixmier.wordProduct