ProbabilityDefects.lean`

19 declarations, 0 contain sorry, 0 declared as axioms

Finite probabilities and their simultaneous translation defects

One ℓ¹ space on S × G carries the sum of all translation defects. In particular its norm is the exact finite sum, without a factor depending on S.card. This is the finite-probability input to the separation argument.

def OAI.ThompsonNonamenability.mass line 28
Source documentation
The total mass of a finitely supported real function.
```
def mass : (G →₀ ℝ) →ₗ[ℝ] ℝ :=
…
```
theorem OAI.ThompsonNonamenability.mass_apply line 32
theorem OAI.ThompsonNonamenability.mass_single line 36
def OAI.ThompsonNonamenability.IsProbabilityWeights line 40
Source documentation
Nonnegative finite weights with total mass one.
```
def IsProbabilityWeights (p : G →₀ ℝ) : Prop :=
…
```
theorem OAI.ThompsonNonamenability.isProbabilityWeights_single line 43
theorem OAI.ThompsonNonamenability.convex_probabilityWeights line 52
abbrev OAI.ThompsonNonamenability.DefectSpace line 63
Source documentation
The simultaneous defects use the ℓ¹ norm on the product index set.
```
abbrev DefectSpace (S : Finset G) := lp (fun _ : ({h // h ∈ S} × G) => ℝ) 1
…
```
def OAI.ThompsonNonamenability.diracDefect line 68
Source documentation
Translation defect of the point probability at g.
```
def diracDefect (S : Finset G) (g : G) : DefectSpace S :=
…
```
Mentions: OAI.ThompsonNonamenability.DefectSpace
def OAI.ThompsonNonamenability.defectMap line 72
Source documentation
The linear extension of the point-probability defects.
```
def defectMap (S : Finset G) : (G →₀ ℝ) →ₗ[ℝ] DefectSpace S :=
…
```
Mentions: OAI.ThompsonNonamenability.DefectSpace
theorem OAI.ThompsonNonamenability.defectMap_single line 76
theorem OAI.ThompsonNonamenability.single_apply_real line 80

theorem OAI.ThompsonNonamenability.diracDefect_apply line 88

Source documentation

Coordinate computation for a single point probability.

theorem diracDefect_apply (S : Finset G) (g : G) (h : S) (x : G) :
    diracDefect S g (h, x) =
      (Finsupp.single g (1 : ℝ)) (h.val⁻¹ * x) - (Finsupp.single g (1 : ℝ)) x := by
…

Mentions: OAI.ThompsonNonamenability.diracDefect

theorem OAI.ThompsonNonamenability.defectMap_apply line 108
Source documentation
The product coordinate is exactly the left translation difference.
```
theorem defectMap_apply (S : Finset G) (p : G →₀ ℝ) (h : S) (x : G) :
    defectMap S p (h, x) = p (h.val⁻¹ * x) - p x := by
…
```
Mentions: OAI.ThompsonNonamenability.defectMap

theorem OAI.ThompsonNonamenability.translation_difference_eq_zero_of_not_mem line 120

Source documentation

Each translation difference vanishes outside its exact finite support bound.

theorem translation_difference_eq_zero_of_not_mem (p : G →₀ ℝ) (h x : G)
    (hx : x ∉ p.support ∪ p.support.image (fun g => h * g)) :
    p (h⁻¹ * x) - p x = 0 := by
…

theorem OAI.ThompsonNonamenability.norm_defectMap line 132

Source documentation

Exact ℓ¹ norm of the simultaneous defect, with no S.card loss.

theorem norm_defectMap (S : Finset G) (p : G →₀ ℝ) :
    ‖defectMap S p‖ =
      ∑ h ∈ S, ∑ x ∈ p.support ∪ p.support.image (fun g => h * g),
        |p (h⁻¹ * x) - p x| := by
…

Mentions: OAI.ThompsonNonamenability.defectMap

def OAI.ThompsonNonamenability.defectSet line 158
Source documentation
The actual image of finite nonnegative probabilities under the defect map.
```
def defectSet (S : Finset G) : Set (DefectSpace S) :=
…
```
Mentions: OAI.ThompsonNonamenability.DefectSpace
theorem OAI.ThompsonNonamenability.convex_defectSet line 161
theorem OAI.ThompsonNonamenability.diracDefect_mem_defectSet line 164
theorem OAI.ThompsonNonamenability.defectSet_nonempty line 169