PartitionColorFamily.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

The actual finite family of colors, including zero outside admissibility

A basic partition is admissible when it respects every chosen parent and child. Its family color is always defined and lies in the unit ball. The option extension also assigns zero to a non-basic image; the group-level construction will supply the actual partial image partition.

def OAI.ThompsonNonamenability.PartitionAdmissible line 25
Source documentation
One simultaneous condition for all actual parent and child intervals.
```
def PartitionAdmissible (D : ℕ) (T : BasicPartition) : Prop :=
…
```
Mentions: OAI.ThompsonNonamenability.BasicPartition
def OAI.ThompsonNonamenability.partitionFamilyColor line 29
Source documentation
The family color is zero whenever the actual partition is inadmissible.
```
def partitionFamilyColor (hD : 0 < D) (f : UnitBall E → UnitBall E)
    (T : BasicPartition) (q : IntervalIndex D) : UnitBall E := by
…
```
Mentions: OAI.ThompsonNonamenability.UnitBall, OAI.ThompsonNonamenability.BasicPartition, OAI.ThompsonNonamenability.IntervalIndex
theorem OAI.ThompsonNonamenability.partitionFamilyColor_of_admissible line 37
theorem OAI.ThompsonNonamenability.partitionFamilyColor_of_not_admissible line 45
theorem OAI.ThompsonNonamenability.partitionFamilyColor_norm_le line 51
theorem OAI.ThompsonNonamenability.partitionFamilyColor_parent line 57
Source documentation
A parent's color is the map applied to its actual child-color mean.
```
theorem partitionFamilyColor_parent (hD : 0 < D)
    (f : UnitBall E → UnitBall E) (T : BasicPartition)
    (h : PartitionAdmissible D T) (i : Fin D) :
    partitionFamilyColor hD f T (.inl i) =
      f (ballMean hD (fun j => partitionFamilyColor hD f T (.inr (i, j)))) := by
…
```
Mentions: OAI.ThompsonNonamenability.UnitBall, OAI.ThompsonNonamenability.BasicPartition, OAI.ThompsonNonamenability.PartitionAdmissible, OAI.ThompsonNonamenability.partitionFamilyColor, OAI.ThompsonNonamenability.ballMean
def OAI.ThompsonNonamenability.optionFamilyColor line 67
Source documentation
Total zero extension at a non-basic image as well as an inadmissible one.
```
def optionFamilyColor (hD : 0 < D) (f : UnitBall E → UnitBall E) :
    Option BasicPartition → IntervalIndex D → UnitBall E
  | none, _ => unitBallZero E
  | some T, q => partitionFamilyColor hD f T q
```
Mentions: OAI.ThompsonNonamenability.UnitBall, OAI.ThompsonNonamenability.BasicPartition, OAI.ThompsonNonamenability.IntervalIndex, OAI.ThompsonNonamenability.unitBallZero, OAI.ThompsonNonamenability.partitionFamilyColor
theorem OAI.ThompsonNonamenability.optionFamilyColor_none line 72
theorem OAI.ThompsonNonamenability.optionFamilyColor_some line 76
theorem OAI.ThompsonNonamenability.optionFamilyColor_norm_le line 80