RecursiveColoring.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Recursive unit-ball colors of actual basic dyadic partitions

The recursion uses the number of actual cells. Restriction to any selected internal interval strictly decreases that number. The mean is bundled with its genuine unit-ball proof before it is supplied to the map.

def OAI.ThompsonNonamenability.partitionColor line 23
theorem OAI.ThompsonNonamenability.partitionColor_of_respects line 36
Source documentation
The recursive branch, with its actual restricted partitions.
```
theorem partitionColor_of_respects (I : Fin D → BasicInterval)
    (hI : ∀ i, (I i).Internal) (hD : 0 < D)
    (f : UnitBall E → UnitBall E) (T : BasicPartition)
    (h : ∀ i, T.Respects (I i)) :
    partitionColor I hI hD f T = f (ballMean hD (fun i =>
      partitionColor I hI hD f (T.restrict (I i) (h i)))) := by
…
```
Mentions: OAI.ThompsonNonamenability.BasicInterval, OAI.ThompsonNonamenability.UnitBall, OAI.ThompsonNonamenability.BasicPartition, OAI.ThompsonNonamenability.partitionColor, OAI.ThompsonNonamenability.ballMean
theorem OAI.ThompsonNonamenability.partitionColor_of_not_respects line 46
Source documentation
Partitions failing the simultaneous respect condition receive zero.
```
theorem partitionColor_of_not_respects (I : Fin D → BasicInterval)
    (hI : ∀ i, (I i).Internal) (hD : 0 < D)
    (f : UnitBall E → UnitBall E) (T : BasicPartition)
    (h : ¬∀ i, T.Respects (I i)) :
    partitionColor I hI hD f T = unitBallZero E := by
…
```
Mentions: OAI.ThompsonNonamenability.BasicInterval, OAI.ThompsonNonamenability.UnitBall, OAI.ThompsonNonamenability.BasicPartition, OAI.ThompsonNonamenability.partitionColor, OAI.ThompsonNonamenability.unitBallZero
theorem OAI.ThompsonNonamenability.partitionColor_norm_le line 54
theorem OAI.ThompsonNonamenability.partitionColor_restrict line 62
Source documentation
Applying the recursion to a parent restriction gives the actual child mean. The normalized two-step restriction is replaced by the proved composite one.
```
theorem partitionColor_restrict (I : Fin D → BasicInterval)
    (hI : ∀ i, (I i).Internal) (hD : 0 < D)
    (f : UnitBall E → UnitBall E) (T : BasicPartition) (i : Fin D)
    (hparent : T.Respects (I i))
    (hchild : ∀ j, T.Respects ((I i).comp (I j))) :
    partitionColor I hI hD f (T.restrict (I i) hparent) =
      f (ballMean hD (fun j => partitionColor I hI hD f
        (T.restrict ((I i).comp (I j)) (hchild j)))) := by
…
```
Mentions: OAI.ThompsonNonamenability.BasicInterval, OAI.ThompsonNonamenability.UnitBall, OAI.ThompsonNonamenability.BasicPartition, OAI.ThompsonNonamenability.partitionColor, OAI.ThompsonNonamenability.ballMean