RayCompactCollapse.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Compact sets collapse along a negative quotient ray

theorem OAI.PolycyclicRecognition.CartanWordModel.ray_compact_sequence_tendsto_one line 21

Source documentation

The ray contraction holds for an arbitrary sequence of points in a fixed compact set. This is the compact-shadow limit needed for the inverse boundary identity.

theorem ray_compact_sequence_tendsto_one
    (α : H →ₗ[ℝ] ℝ)
    (Q : NilpotentLieModel ((cartanRootIdeal H) ⧸ M.coneWordIdeal (positiveWeightRay α)))
    (Exp : GroupLieAlgebra (𝓘(ℝ, Q.modelSpace)) Q.carrier → Q.carrier)
    (hExp : IsGroupExponential Exp) (hbij : Function.Bijective Exp)
    (chart : GroupLieAlgebra (𝓘(ℝ, Q.modelSpace)) Q.carrier ≃ₜ Q.carrier)
    (hchart : ∀ v, chart v = Exp v)
    (v : H) (hv : α v < 0) (K : Set Q.carrier) (hK : IsCompact K)
    (q : ℕ → Q.carrier) (hq : ∀ n, q n ∈ K) :
    Tendsto (fun n : ℕ => exponentialConjugate Q.equiv Exp hbij
      (M.coneAdjointAutomorphism T (positiveWeightRay α) (positiveWeightRay_add α)
        ((n : ℝ) • v)) (q n)) atTop (𝓝 (1 : Q.carrier)) := by
…

Mentions: OAI.PolycyclicRecognition.NilpotentLieModel, OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.positiveWeightRay, OAI.PolycyclicRecognition.exponentialConjugate, OAI.PolycyclicRecognition.positiveWeightRay_add

theorem OAI.PolycyclicRecognition.CartanWordModel.eq_of_mem_all_ray_compact_shadows line 73

Source documentation

Membership in every translated contracting compact shadow determines the boundary point uniquely. This is the final limit step in the inverse boundary-map argument.

theorem eq_of_mem_all_ray_compact_shadows
    (α : H →ₗ[ℝ] ℝ)
    (Q : NilpotentLieModel ((cartanRootIdeal H) ⧸ M.coneWordIdeal (positiveWeightRay α)))
    (Exp : GroupLieAlgebra (𝓘(ℝ, Q.modelSpace)) Q.carrier → Q.carrier)
    (hExp : IsGroupExponential Exp) (hbij : Function.Bijective Exp)
    (chart : GroupLieAlgebra (𝓘(ℝ, Q.modelSpace)) Q.carrier ≃ₜ Q.carrier)
    (hchart : ∀ v, chart v = Exp v)
    (v : H) (hv : α v < 0) (K : Set Q.carrier) (hK : IsCompact K)
    (e : Q.carrier → Q.carrier) (he : Continuous e) (z : Q.carrier)
    (hshadow : ∀ n : ℕ, ∃ q ∈ K, z = e (exponentialConjugate Q.equiv Exp hbij
      (M.coneAdjointAutomorphism T (positiveWeightRay α) (positiveWeightRay_add α)
        ((n : ℝ) • v)) q)) : z = e 1 := by
…