RestrictionCovariance.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Exact covariance under actual affine transport

Every source image cell and its target image cell retain the same original uniform-grid index. The affine chart equality therefore identifies the normalized restrictions pointwise, including their closed endpoints.

theorem OAI.ThompsonNonamenability.CarriesAffinely.chart_value_eq_iff line 19
theorem OAI.ThompsonNonamenability.CarriesAffinely.left_value_eq_iff line 32
theorem OAI.ThompsonNonamenability.CarriesAffinely.right_value_eq_iff line 38
theorem OAI.ThompsonNonamenability.imageCell_transport_iff line 48
Source documentation
Corresponding actual image cells have exactly the affinely transported endpoints. No admissibility of any other interval is assumed here.
```
theorem imageCell_transport_iff (h g : F) (n : ℕ)
    (I I' : BasicInterval) (hc : CarriesAffinely h I I')
    (hg : ImageBasic g n) (hhg : ImageBasic (h * g) n) (k : Fin (2 ^ n)) :
    imageCell (h * g) n hhg k = I' ↔ imageCell g n hg k = I := by
…
```
Mentions: OAI.ThompsonNonamenability.F, OAI.ThompsonNonamenability.BasicInterval, OAI.ThompsonNonamenability.CarriesAffinely, OAI.ThompsonNonamenability.ImageBasic, OAI.ThompsonNonamenability.imageCell

theorem OAI.ThompsonNonamenability.image_restrict_covariance line 75

Source documentation

Exact normalized restriction covariance for multiplication h * g = h ∘ g.

theorem image_restrict_covariance
    (h g : F) (n : ℕ) (I I' : BasicInterval)
    (hc : CarriesAffinely h I I')
    (hg : ImageBasic g n) (hhg : ImageBasic (h * g) n)
    (hr : (imagePartition g n hg).Respects I)
    (hr' : (imagePartition (h * g) n hhg).Respects I') :
    (imagePartition (h * g) n hhg).restrict I' hr' =
      (imagePartition g n hg).restrict I hr := by
…

Mentions: OAI.ThompsonNonamenability.F, OAI.ThompsonNonamenability.BasicInterval, OAI.ThompsonNonamenability.CarriesAffinely, OAI.ThompsonNonamenability.ImageBasic, OAI.ThompsonNonamenability.imagePartition