TransportFamily.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

A fixed finite family of actual affine transports

The set of transports depends only on the branching parameter. Each ordered separated pair in the actual parent/child family is carried onto the reference pair. After this set is fixed, one partition level is selected for the given finite group set and all of its translates by these transports.

def OAI.ThompsonNonamenability.orderedIntervalPairs line 29
Source documentation
The ordered separated pairs of actual interval occurrences.
```
def orderedIntervalPairs (D : ℕ) : Finset (IntervalIndex D × IntervalIndex D) := by
…
```
Mentions: OAI.ThompsonNonamenability.IntervalIndex
theorem OAI.ThompsonNonamenability.mem_orderedIntervalPairs line 34
def OAI.ThompsonNonamenability.pairTransport line 41
Source documentation
An actual Thompson-group witness, chosen only for a genuinely separated pair.
```
def pairTransport (hD : 2 ≤ D) (p : {p // p ∈ orderedIntervalPairs D}) : F :=
…
```
Mentions: OAI.ThompsonNonamenability.orderedIntervalPairs, OAI.ThompsonNonamenability.F
theorem OAI.ThompsonNonamenability.pairTransport_spec line 49
def OAI.ThompsonNonamenability.fixedTransportSet line 62
Source documentation
This actual finite subset of F is fixed before any averaging set.
```
def fixedTransportSet (hD : 2 ≤ D) : Finset F :=
…
```
Mentions: OAI.ThompsonNonamenability.F
theorem OAI.ThompsonNonamenability.transport_of_before line 65
theorem OAI.ThompsonNonamenability.fixedTransportSet_nonempty line 77
def OAI.ThompsonNonamenability.transportClosure line 84
Source documentation
The one finite set used to select a common partition level.
```
def transportClosure (S A : Finset F) : Finset F :=
…
```
Mentions: OAI.ThompsonNonamenability.F
theorem OAI.ThompsonNonamenability.mem_transportClosure_self line 87
theorem OAI.ThompsonNonamenability.mem_transportClosure_mul line 90
theorem OAI.ThompsonNonamenability.exists_transport_admissible line 96
Source documentation
A single level works simultaneously on A and on every hA for h in fixed S.
```
theorem exists_transport_admissible (hD : 2 ≤ D) (A : Finset F) :
    ∃ n, (∀ g ∈ A, GlobalAdmissible D n g) ∧
      ∀ h ∈ fixedTransportSet hD, ∀ g ∈ A, GlobalAdmissible D n (h * g) := by
…
```
Mentions: OAI.ThompsonNonamenability.F, OAI.ThompsonNonamenability.GlobalAdmissible, OAI.ThompsonNonamenability.fixedTransportSet
theorem OAI.ThompsonNonamenability.globalCorrelation_comm line 108
Source documentation
Symmetry is used only to orient a separated pair; it introduces no sign assumption on its real inner product.
```
theorem globalCorrelation_comm (hD : 0 < D) (f : UnitBall E → UnitBall E)
    (n : ℕ) (q r : IntervalIndex D) (g : F) :
    globalCorrelation hD f n q r g = globalCorrelation hD f n r q g := by
…
```
Mentions: OAI.ThompsonNonamenability.UnitBall, OAI.ThompsonNonamenability.IntervalIndex, OAI.ThompsonNonamenability.F, OAI.ThompsonNonamenability.globalCorrelation
theorem OAI.ThompsonNonamenability.separated_correlation_bound line 115
Source documentation
All separated correlations are compared with one reference correlation using only the maximum boundary over the previously fixed finite set.
```
theorem separated_correlation_bound (hD : 2 ≤ D) (f : UnitBall E → UnitBall E)
    (n : ℕ) (A : Finset F) (hA : A.Nonempty)
    (hg : ∀ g ∈ A, GlobalAdmissible D n g)
    (hhg : ∀ h ∈ fixedTransportSet hD, ∀ g ∈ A, GlobalAdmissible D n (h * g))
    (q r : IntervalIndex D)
    (hqr : StrictlySeparated (familyInterval D q) (familyInterval D r)) :
    |realAvg A (globalCorrelation (lt_of_lt_of_le (by decide : 0 < 2) hD) f n q r) -
      realAvg A (globalCorrelation (lt_of_lt_of_le (by decide : 0 < 2) hD) f n
        (.inl (firstIndex hD)) (.inl (secondIndex hD)))| ≤
      boundaryMax (fixedTransportSet hD) (fixedTransportSet_nonempty hD) A := by
…
```
Mentions: OAI.ThompsonNonamenability.UnitBall, OAI.ThompsonNonamenability.F, OAI.ThompsonNonamenability.GlobalAdmissible, OAI.ThompsonNonamenability.fixedTransportSet, OAI.ThompsonNonamenability.IntervalIndex, OAI.ThompsonNonamenability.StrictlySeparated, OAI.ThompsonNonamenability.familyInterval, OAI.ThompsonNonamenability.realAvg, OAI.ThompsonNonamenability.globalCorrelation, OAI.ThompsonNonamenability.firstIndex, OAI.ThompsonNonamenability.secondIndex, OAI.ThompsonNonamenability.boundaryMax, OAI.ThompsonNonamenability.fixedTransportSet_nonempty