InvariantMean.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

Positive normalized left-invariant means

The domain is the actual space of all bounded real functions on the group. Continuity is a consequence of positivity and normalization, not an assumption.

theorem OAI.ThompsonNonamenability.BoundedReal.smul_one_apply line 23
theorem OAI.ThompsonNonamenability.leftPull_apply line 30
theorem OAI.ThompsonNonamenability.leftPull_one line 34
theorem OAI.ThompsonNonamenability.leftPull_mul line 40
Source documentation
Pullback reverses the order of the two left multiplications.
```
theorem leftPull_mul (h k : G) (f : BoundedReal G) :
    leftPull (h * k) f = leftPull k (leftPull h f) := by
…
```
Mentions: OAI.ThompsonNonamenability.BoundedReal, OAI.ThompsonNonamenability.leftPull
instance OAI.ThompsonNonamenability.InvariantMean.(instance at line 48) line 48
theorem OAI.ThompsonNonamenability.InvariantMean.map_zero line 52
theorem OAI.ThompsonNonamenability.InvariantMean.map_add line 55
theorem OAI.ThompsonNonamenability.InvariantMean.map_sub line 59
theorem OAI.ThompsonNonamenability.InvariantMean.map_smul line 63
theorem OAI.ThompsonNonamenability.InvariantMean.map_const line 69
Source documentation
Evaluation of a constant function.
```
theorem map_const (M : InvariantMean G) (r : ℝ) :
    M (r • (1 : BoundedReal G)) = r := by
…
```
Mentions: OAI.ThompsonNonamenability.InvariantMean, OAI.ThompsonNonamenability.BoundedReal
theorem OAI.ThompsonNonamenability.InvariantMean.mono line 74
Source documentation
Positivity gives monotonicity for the pointwise order.
```
theorem mono (M : InvariantMean G) {f g : BoundedReal G}
    (hfg : ∀ x, f x ≤ g x) : M f ≤ M g := by
…
```
Mentions: OAI.ThompsonNonamenability.InvariantMean, OAI.ThompsonNonamenability.BoundedReal
theorem OAI.ThompsonNonamenability.InvariantMean.abs_apply_le_norm line 81
Source documentation
A mean has norm at most one, as a consequence of its defining axioms.
```
theorem abs_apply_le_norm (M : InvariantMean G) (f : BoundedReal G) :
    |M f| ≤ ‖f‖ := by
…
```
Mentions: OAI.ThompsonNonamenability.InvariantMean, OAI.ThompsonNonamenability.BoundedReal
def OAI.ThompsonNonamenability.InvariantMean.toContinuousLinearMap line 95
Source documentation
The continuous functional furnished automatically by a positive normalized mean.
```
def toContinuousLinearMap (M : InvariantMean G) : BoundedReal G →L[ℝ] ℝ :=
…
```
Mentions: OAI.ThompsonNonamenability.InvariantMean, OAI.ThompsonNonamenability.BoundedReal
theorem OAI.ThompsonNonamenability.InvariantMean.toContinuousLinearMap_apply line 100
theorem OAI.ThompsonNonamenability.InvariantMean.continuous line 103
theorem OAI.ThompsonNonamenability.InvariantMean.norm_toContinuousLinearMap_le_one line 106
theorem OAI.ThompsonNonamenability.InvariantMean.norm_toContinuousLinearMap line 114
Source documentation
Normalization makes the automatic functional's operator norm exactly one.
```
theorem norm_toContinuousLinearMap (M : InvariantMean G) :
    ‖M.toContinuousLinearMap‖ = 1 := by
…
```
Mentions: OAI.ThompsonNonamenability.InvariantMean