Contracting.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Contracting averages and sparse splitting for nonamenable groups.

theorem OAI.Dixmier.rightRegular_opNorm line 14
theorem OAI.Dixmier.regular_sum_norm_le line 24
theorem OAI.Dixmier.amenable_of_all_sum_norm line 31
Source documentation
Contrapositive analytic argument using the invariant-mean definition.
```
theorem amenable_of_all_sum_norm
    (h : ∀ S : Finset G, 1 ∈ S → ‖∑ g ∈ S, rightRegular g‖ = (S.card : ℝ)) :
    Amenable G := by
…
```
Mentions: OAI.Dixmier.rightRegular, OAI.Dixmier.Amenable

theorem OAI.Dixmier.exists_contracting_sum line 55

Source documentation

Nonamenability provides a strict contraction after normalization.

theorem exists_contracting_sum (hG : ¬ Amenable G) :
    ∃ S : Finset G, 1 ∈ S ∧ 2 ≤ S.card ∧
      ∃ ρ : ℝ, 0 < ρ ∧ ρ < 1 ∧ ‖∑ g ∈ S, rightRegular g‖ ≤ (S.card : ℝ) * ρ := by
…

Mentions: OAI.Dixmier.Amenable, OAI.Dixmier.rightRegular

theorem OAI.Dixmier.contracting_average line 80

Source documentation

A contracting average with e ∈ S, d ≥ 2, and 0 < ρ < 1.

theorem contracting_average (hG : ¬ Amenable G) :
    ∃ S : Finset G, 1 ∈ S ∧ 2 ≤ S.card ∧
      ∃ ρ : ℝ, 0 < ρ ∧ ρ < 1 ∧
        ‖((S.card : ℂ)⁻¹) • (∑ g ∈ S, rightRegular g)‖ ≤ ρ := by
…

Mentions: OAI.Dixmier.Amenable, OAI.Dixmier.rightRegular

theorem OAI.Dixmier.sparse_splitting_of_nonamenable line 96

Source documentation

Sparse splitting from nonamenability. A single S and ρ work for every positive word length; all words remain separate labels, even when their group products agree.

theorem sparse_splitting_of_nonamenable (hG : ¬ Amenable G) :
    ∃ S : Finset G, 1 ∈ S ∧ 2 ≤ S.card ∧ ∃ ρ : ℝ, 0 < ρ ∧ ρ < 1 ∧
      ∀ ℓ : ℕ, 0 < ℓ → ∃ a : G → Word S ℓ → Bool,
        (∀ x, (rowOnes a x).card ≤ ⌈(S.card : ℝ)^ℓ * ρ^ℓ⌉₊) ∧
        ∀ y, (columnZeros a (wordProduct (fun s : S => (s : G)) ℓ) y).card ≤
          ⌈(S.card : ℝ)^ℓ * ρ^ℓ⌉₊ := by
…

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