AffineTransport.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Simultaneous affine transport of two separated basic intervals

Each of the three complementary gaps is partitioned and equalized separately. Consequently the selected source and target cells occupy matching positions in the two full ordered partitions. The interpolation theorem constructs an actual increasing dyadic PL homeomorphism on those partitions.

theorem OAI.ThompsonNonamenability.forall₂_after_prefix line 22

theorem OAI.ThompsonNonamenability.exists_pair_transport_of_partitions line 31

Source documentation

The selected positions are preserved because the three gap lengths are equalized independently. All partition data will be constructed below.

private theorem exists_pair_transport_of_partitions
    (I J I' J' : BasicInterval)
    (P₀ : DyadicGapPartition 0 I.left) (Q₀ : DyadicGapPartition 0 I'.left)
    (P₁ : DyadicGapPartition I.right J.left)
    (Q₁ : DyadicGapPartition I'.right J'.left)
    (P₂ : DyadicGapPartition J.right 1) (Q₂ : DyadicGapPartition J'.right 1)
    (hlen₀ : P₀.cells.length = Q₀.cells.length)
    (hlen₁ : P₁.cells.length = Q₁.cells.length)
    (hlen₂ : P₂.cells.length = Q₂.cells.length) :
    ∃ h : F, CarriesAffinely h I I' ∧ CarriesAffinely h J J' := by
…

Mentions: OAI.ThompsonNonamenability.BasicInterval, OAI.ThompsonNonamenability.DyadicGapPartition, OAI.ThompsonNonamenability.F, OAI.ThompsonNonamenability.CarriesAffinely

theorem OAI.ThompsonNonamenability.exists_affine_pair_transport line 62
Source documentation
Two strictly separated internal basic intervals can simultaneously be carried onto any other such pair by an actual element of standard Thompson F.
```
theorem exists_affine_pair_transport {I J I' J' : BasicInterval}
    (hI : I.Internal) (hJ : J.Internal)
    (hI' : I'.Internal) (hJ' : J'.Internal)
    (hIJ : I.Before J) (hIJ' : I'.Before J') :
    ∃ h : F, CarriesAffinely h I I' ∧ CarriesAffinely h J J' := by
…
```
Mentions: OAI.ThompsonNonamenability.BasicInterval, OAI.ThompsonNonamenability.F, OAI.ThompsonNonamenability.CarriesAffinely