TerminalTupleProjection.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Projecting a thickened increment tuple at its terminal coordinate

The right correction to the Cartan lift is retained explicitly. This identity does not require uniqueness of Cartan factorization.

theorem OAI.PolycyclicRecognition.prefixCoordinateEquiv_terminal line 21
theorem OAI.PolycyclicRecognition.terminal_thickening_projection line 28
theorem OAI.PolycyclicRecognition.terminal_thickening_dist line 40
theorem OAI.PolycyclicRecognition.terminal_tuple_product_cover line 56

theorem OAI.PolycyclicRecognition.terminal_tuple_product_cover_pos line 85

Source documentation

The terminal-cover statement for an arbitrary positive tuple length, including the even length of a chronological alternating product.

theorem terminal_tuple_product_cover_pos {h : ℕ} (hh : 0 < h)
    [MetricSpace G] [IsIsometricSMul G G]
    (ι : N →* G) (κ : D →* G) (φ : D →* MulAut N)
    (hconj : ∀ d n, ι (φ d n) = κ d * ι n * (κ d)⁻¹)
    (s : Finset (Fin h → G))
    (p : (Fin h → G) → (Fin h → N) × (Fin h → D))
    (U : Set ((Fin h → N) × (Fin h → D)))
    (I : Set (Fin h → N)) (C : Set N) (A : Set D) (t : Finset G)
    (hp : ∀ x ∈ s, ∀ i, ι ((p x).1 i) * κ ((p x).2 i) = x i)
    (hI : ∀ u ∈ I, ∃ x ∈ s, ∃ z ∈ U,
      prefixCoordinateEquiv h u = fun i => (p x).1 i * φ ((p x).2 i) (z.1 i))
    {ρ R : ℝ}
…

Mentions: OAI.PolycyclicRecognition.prefixCoordinateEquiv