DistortedHomomorphisms.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Averaged homomorphisms vanish on logarithmically distorted flows

A continuous homomorphism is linear on each one-parameter subgroup. A linear metric bound and logarithmic distortion force that linear value to vanish. In particular, the stationary mean kills the actual root flows.

theorem OAI.PolycyclicRecognition.hom_flow_eq_smul line 29

Source documentation

The image of a continuous one-parameter subgroup under a continuous homomorphism is a real-linear one-parameter subgroup.

theorem hom_flow_eq_smul
    (d : ℝ → G) (hd : Continuous d) (hd₀ : d 0 = 1)
    (hdadd : ∀ s t, d (s + t) = d s * d t)
    (l : G →* Multiplicative W) (hl : Continuous fun g => (l g).toAdd) (t : ℝ) :
    (l (d t)).toAdd = t • (l (d 1)).toAdd := by
…

theorem OAI.PolycyclicRecognition.hom_eq_one_of_logarithmic_flow line 46

Source documentation

Linear metric control precludes a nonzero homomorphism on a flow of logarithmic ambient size.

theorem hom_eq_one_of_logarithmic_flow
    (d : ℝ → G) (hd : Continuous d) (hd₀ : d 0 = 1)
    (hdadd : ∀ s t, d (s + t) = d s * d t)
    (l : G →* Multiplicative W) (hl : Continuous fun g => (l g).toAdd)
    {L D B : ℝ} (hL : 0 ≤ L) (hB : 0 < B)
    (hbound : ∀ g, ‖(l g).toAdd‖ ≤ L * dist 1 g)
    (hdist : ∀ t, dist 1 (d t) ≤ D * Real.log (2 + B * |t|)) :
    ∀ t, l (d t) = 1 := by
…

theorem OAI.PolycyclicRecognition.hom_eq_one_on_root_exp line 94

Source documentation

Every continuous homomorphism with linear metric control kills the root exponentials, using their logarithmic distortion.

theorem hom_eq_one_on_root_exp
    {a : ℕ} (T : TriangularAdjoint (GroupLieAlgebra (𝓘(ℝ, EG)) G) a)
    (H : LieSubalgebra ℝ (GroupLieAlgebra (𝓘(ℝ, EG)) G)) [H.IsCartanSubalgebra]
    (χ : LieModule.Weight ℝ H (GroupLieAlgebra (𝓘(ℝ, EG)) G)) (hχ : χ.IsNonZero)
    (Exp : GroupLieAlgebra (𝓘(ℝ, EG)) G → G) (hExp : IsGroupExponential Exp)
    (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
…

Mentions: OAI.PolycyclicRecognition.TriangularAdjoint, OAI.PolycyclicRecognition.ExponentialLinearRealizationInput