GlobalColors.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

Globally defined colors of the actual Thompson-group images

A non-basic image, or a basic image failing the simultaneous family respect condition, receives zero. Thus every correlation is bounded on the entire actual group, including outside a finite set used for averaging.

def OAI.ThompsonNonamenability.imagePartitionOption line 29
Source documentation
The genuine partial image of the uniform partition, made total with none.
```
def imagePartitionOption (g : F) (n : ℕ) : Option BasicPartition := by
…
```
Mentions: OAI.ThompsonNonamenability.F, OAI.ThompsonNonamenability.BasicPartition
def OAI.ThompsonNonamenability.GlobalAdmissible line 34
Source documentation
One condition for the whole actual parent/child family at a group element.
```
def GlobalAdmissible (D n : ℕ) (g : F) : Prop :=
…
```
Mentions: OAI.ThompsonNonamenability.F
def OAI.ThompsonNonamenability.globalColor line 37
theorem OAI.ThompsonNonamenability.globalColor_of_imageBasic line 41
theorem OAI.ThompsonNonamenability.globalColor_of_image_admissible line 46
theorem OAI.ThompsonNonamenability.globalColor_of_not_admissible line 55
theorem OAI.ThompsonNonamenability.globalColor_norm_le line 66
theorem OAI.ThompsonNonamenability.eventually_global_admissible line 72
Source documentation
The actual finite group set has one common admissibility level.
```
theorem eventually_global_admissible (D : ℕ) (K : Finset F) :
    ∃ N, ∀ n ≥ N, ∀ g ∈ K, GlobalAdmissible D n g := by
…
```
Mentions: OAI.ThompsonNonamenability.F, OAI.ThompsonNonamenability.GlobalAdmissible
theorem OAI.ThompsonNonamenability.exists_common_admissible line 80
theorem OAI.ThompsonNonamenability.globalColor_parent line 86
Source documentation
The exact recursive identity at every admissible actual group point.
```
theorem globalColor_parent (hD : 0 < D) (f : UnitBall E → UnitBall E)
    (n : ℕ) (g : F) (hg : GlobalAdmissible D n g) (i : Fin D) :
    globalColor hD f n (.inl i) g =
      f (ballMean hD (fun j => globalColor hD f n (.inr (i, j)) g)) := by
…
```
Mentions: OAI.ThompsonNonamenability.UnitBall, OAI.ThompsonNonamenability.F, OAI.ThompsonNonamenability.GlobalAdmissible, OAI.ThompsonNonamenability.globalColor, OAI.ThompsonNonamenability.ballMean
theorem OAI.ThompsonNonamenability.globalColor_covariance line 96
Source documentation
Source and target admissibility suffice; the transport need not preserve any other selected interval.
```
theorem globalColor_covariance (hD : 0 < D) (f : UnitBall E → UnitBall E)
    (n : ℕ) (h g : F) (q r : IntervalIndex D)
    (hc : CarriesAffinely h (familyInterval D q) (familyInterval D r))
    (hg : GlobalAdmissible D n g) (hhg : GlobalAdmissible D n (h * g)) :
    globalColor hD f n q g = globalColor hD f n r (h * g) := by
…
```
Mentions: OAI.ThompsonNonamenability.UnitBall, OAI.ThompsonNonamenability.F, OAI.ThompsonNonamenability.IntervalIndex, OAI.ThompsonNonamenability.CarriesAffinely, OAI.ThompsonNonamenability.familyInterval, OAI.ThompsonNonamenability.GlobalAdmissible, OAI.ThompsonNonamenability.globalColor
def OAI.ThompsonNonamenability.globalCorrelation line 110
Source documentation
A real correlation on all of the actual group.
```
def globalCorrelation (hD : 0 < D) (f : UnitBall E → UnitBall E)
    (n : ℕ) (q r : IntervalIndex D) (g : F) : ℝ :=
…
```
Mentions: OAI.ThompsonNonamenability.UnitBall, OAI.ThompsonNonamenability.IntervalIndex, OAI.ThompsonNonamenability.F
theorem OAI.ThompsonNonamenability.globalCorrelation_abs_le_one line 114
theorem OAI.ThompsonNonamenability.globalCorrelation_covariance line 120

theorem OAI.ThompsonNonamenability.globalCorrelation_translate_bound line 131

Source documentation

Exact affine covariance and global boundedness imply the finite comparison.

theorem globalCorrelation_translate_bound (hD : 0 < D)
    (f : UnitBall E → UnitBall E) (n : ℕ) (A : Finset F) (hA : A.Nonempty)
    (h : F) (q r q' r' : IntervalIndex D)
    (hq : CarriesAffinely h (familyInterval D q) (familyInterval D q'))
    (hr : CarriesAffinely h (familyInterval D r) (familyInterval D r'))
    (hg : ∀ g ∈ A, GlobalAdmissible D n g)
    (hhg : ∀ g ∈ A, GlobalAdmissible D n (h * g)) :
    |realAvg A (globalCorrelation hD f n q r) -
      realAvg A (globalCorrelation hD f n q' r')| ≤ boundaryRatio A h := by
…

Mentions: OAI.ThompsonNonamenability.UnitBall, OAI.ThompsonNonamenability.F, OAI.ThompsonNonamenability.IntervalIndex, OAI.ThompsonNonamenability.CarriesAffinely, OAI.ThompsonNonamenability.familyInterval, OAI.ThompsonNonamenability.GlobalAdmissible, OAI.ThompsonNonamenability.realAvg, OAI.ThompsonNonamenability.globalCorrelation, OAI.ThompsonNonamenability.boundaryRatio