RayTangentContraction.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Ray contraction in the actual tangent coordinate basis

theorem OAI.PolycyclicRecognition.mapped_basis_exponentialLog line 18

theorem OAI.PolycyclicRecognition.exists_compact_contraction_pullback line 38

Source documentation

Pull back a compact-set contraction estimate along actual factor coordinates. The coordinate identity is retained pointwise.

theorem exists_compact_contraction_pullback
    {V D Q E J : Type*} [TopologicalSpace Q]
    [AddCommGroup E] [Module ℝ E] [Fintype J]
    (log : D → V) (size height : V → ℝ) (coords : Q → E)
    (action : V → Q → Q) (actual : D → Q → Q)
    (he : ∀ d q, actual d q = action (log d) q)
    (hb : ∃ (b : Basis J ℝ E) (p : ℕ) (rate : ℝ), 0 < rate ∧
      ∀ K : Set Q, IsCompact K → ∃ A : ℝ, 0 ≤ A ∧
        ∀ v, height v ≤ 0 → ∀ q ∈ K, ‖b.equivFun (coords (action v q))‖ ≤
          A * (1 + size v) ^ p * Real.exp (rate * height v)) :
    ∃ (b : Basis J ℝ E) (p : ℕ) (rate : ℝ), 0 < rate ∧
      ∀ K : Set Q, IsCompact K → ∃ A : ℝ, 0 ≤ A ∧
…

theorem OAI.PolycyclicRecognition.CartanWordModel.coneAdjoint_projection line 66
theorem OAI.PolycyclicRecognition.CartanWordModel.exists_ray_tangent_compact_contraction line 72