OAI/NumberTheory/DukePrimeDegree/Geometry/CompactAction.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Compact observables under small group translations

A compactly supported continuous observable changes uniformly little under a group element tending to the identity. This remains true along arbitrary moving base points, including points leaving compact sets. It supplies the topological contraction step in the Hopf argument on a noncompact homogeneous space.

  1. theorem OAI.DukePrimeDegree.compact_observable_smul_tendstoUniformly line 28

    Source documentation

    Small translations act uniformly continuously on a compactly supported continuous real observable.

    theorem compact_observable_smul_tendstoUniformly
    (f : X → ℝ) (hf : Continuous f) (hc : HasCompactSupport f) :
    TendstoUniformly (fun a : G => fun x : X => f (a • x)) f (𝓝 1) := by
…
  2. theorem OAI.DukePrimeDegree.compact_observable_moving_smul_difference line 63

    Source documentation

    The base point may vary arbitrarily while the translating element tends to the identity.

    theorem compact_observable_moving_smul_difference
    (f : X → ℝ) (hf : Continuous f) (hc : HasCompactSupport f)
    {ι : Type*} {l : Filter ι} (x : ι → X) (a : ι → G)
    (ha : Tendsto a l (𝓝 1)) :
    Tendsto (fun n => |f (a n • x n) - f (x n)|) l (𝓝 0) := by
…