CartanSampledBridge.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The contact bridge in the original sampled group frame

theorem OAI.PolycyclicRecognition.sampled_coneProbe_dist line 15

Source documentation

Translate both probes by the same sampled root element.

theorem sampled_coneProbe_dist
    {N G : Type*} [Group N] [Group G] [PseudoMetricSpace G]
    (ι : N →* G) (S : MulAut N) (u i sample q k : N) (x d : G) :
    dist (x * ι (sample * coneProbeSecond S u i k) * d)
      (x * ι (sample * coneProbeFirst S u i q) * d) =
    dist ((x * ι sample) * (ι (coneProbeFirst S u i q) * d))
      ((x * ι sample) * (ι (u * S i * S k) * d)) := by
…

Mentions: OAI.PolycyclicRecognition.coneProbeSecond, OAI.PolycyclicRecognition.coneProbeFirst

theorem OAI.PolycyclicRecognition.exists_sampled_contact_pivot_bridge line 35
Source documentation
The metric bridge joins the actual first and second probes after the same root translation used in the source count. The normalized inside letter is the inverse image of the original neighboring step.
```
theorem exists_sampled_contact_pivot_bridge
    (hExpG : IsGroupExponential ExpG)
    (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
…
```
Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput