Pointed Gromov–Hausdorff convergence

DefinitionPointed Gromov–Hausdorff convergence#✓fully proved

Let \(X_0, X_1, \dots\) and \(Y\) be pseudometric spaces with base points \(p_n \in X_n\) and \(q \in Y\). The sequence \((X_n, p_n)\) converges to \((Y, q)\) in the pointed Gromov–Hausdorff sense if for all \(R > 0\) and \(\varepsilon > 0\) there is \(N\) such that for every \(n \ge N\) there is a map \(f\) from the open ball \(B(p_n, R)\) to \(Y\) with \(f(p_n) = q\), with \(|d(f(x), f(y)) - d(x, y)| \le \varepsilon\) for all \(x, y \in B(p_n, R)\), and such that every point of the open ball \(B(q, R - \varepsilon)\) is at distance less than \(\varepsilon\) from some point of the image of \(f\).

No measurability or continuity is required of \(f\), and the spaces need not be complete or separable, so this extends the metric part of the pointed measured Gromov–Hausdorff convergence of Gigli–Mondino–Savaré, who use Borel maps on complete separable spaces. Open balls are an implementation choice for their unspecified balls \(B_R\).

def PointedGHConverges (p : ∀ n, X n) (q : Y) : Prop :=
  ∀ (R : ℝ) (hR : 0 < R) (ε : ℝ) (_ : 0 < ε),
    ∀ᶠ n in Filter.atTop, ∃ f : ↥(Metric.ball (p n) R) → Y,
      f ⟨p n, Metric.mem_ball_self hR⟩ = q ∧
        (∀ x y, |dist (f x) (f y) - dist (x : X n) (y : X n)| ≤ ε) ∧
        Metric.ball q (R - ε) ⊆ Metric.thickening ε (Set.range f)

Used by 3

Used byConstant sequences converge in the pointed Gromov–Hausdorff sense · Pointed Gromov–Hausdorff convergence with strict distortion · Pointed Gromov–Hausdorff convergence with measurable maps

TheoremPointed Gromov–Hausdorff convergence with strict distortion#✓fully proved

Let \(X_0, X_1, \dots\) and \(Y\) be pseudometric spaces with base points \(p_n \in X_n\) and \(q \in Y\). Then \((X_n, p_n)\) converges to \((Y, q)\) in the pointed Gromov–Hausdorff sense if and only if for all \(R > 0\) and \(\varepsilon > 0\) there is \(N\) such that for every \(n \ge N\) there are a map \(f\) from the open ball \(B(p_n, R)\) to \(Y\) and a real number \(\delta < \varepsilon\) with \(f(p_n) = q\), with \(|d(f(x), f(y)) - d(x, y)| \le \delta\) for all \(x, y \in B(p_n, R)\), and such that every point of the open ball \(B(q, R - \varepsilon)\) is at distance less than \(\varepsilon\) from some point of the image of \(f\).

That is, the distortion of \(f\) may be required to be strictly less than \(\varepsilon\), as in arXiv:2602.04826, Def. 2.12.

theorem pointedGHConverges_iff_dis_lt (p : ∀ n, X n) (q : Y) :
    PointedGHConverges p q ↔
      ∀ (R : ℝ) (hR : 0 < R) (ε : ℝ) (_ : 0 < ε),
        ∀ᶠ n in Filter.atTop, ∃ f : ↥(Metric.ball (p n) R) → Y,
          f ⟨p n, Metric.mem_ball_self hR⟩ = q ∧
            (∃ δ, δ < ε ∧ ∀ x y,
              |dist (f x) (f y) - dist (x : X n) (y : X n)| ≤ δ) ∧
            Metric.ball q (R - ε) ⊆ Metric.thickening ε (Set.range f)

Uses 1

Statement usesPointed Gromov–Hausdorff convergence

TheoremConstant sequences converge in the pointed Gromov–Hausdorff sense#✓fully proved

For every pseudometric space \(Y\) and every point \(q \in Y\), the constant sequence \((X_n, p_n) = (Y, q)\) converges to \((Y, q)\) in the pointed Gromov–Hausdorff sense.

theorem pointedGHConverges_const (q : Y) :
    PointedGHConverges (X := fun _ => Y) (fun _ => q) q

Uses 1

Statement usesPointed Gromov–Hausdorff convergence

TheoremPointed Gromov–Hausdorff convergence with measurable maps#✓fully proved

Let \(X_0, X_1, \dots\) be separable pseudometric spaces, each with its Borel \(\sigma\)-algebra, with base points \(p_n \in X_n\), and let \(Y\) be a pseudometric space with any \(\sigma\)-algebra and a base point \(q \in Y\). Then \((X_n, p_n)\) converges to \((Y, q)\) in the pointed Gromov–Hausdorff sense if and only if for all \(R > 0\) and \(\varepsilon > 0\) there is \(N\) such that for every \(n \ge N\) there is a map \(f\) from the open ball \(B(p_n, R)\) to \(Y\), measurable for the subspace \(\sigma\)-algebra on the ball, with \(f(p_n) = q\), with \(|d(f(x), f(y)) - d(x, y)| \le \varepsilon\) for all \(x, y \in B(p_n, R)\), and such that every point of the open ball \(B(q, R - \varepsilon)\) is at distance less than \(\varepsilon\) from some point of the image of \(f\).

So for separable spaces the approximating maps can be taken Borel, as Gigli–Mondino–Savaré require.

theorem pointedGHConverges_iff_exists_measurable
    {X : ℕ → Type u} [∀ n, PseudoMetricSpace (X n)]
    [∀ n, TopologicalSpace.SeparableSpace (X n)] [∀ n, MeasurableSpace (X n)]
    [∀ n, BorelSpace (X n)] {Y : Type v} [PseudoMetricSpace Y]
    [MeasurableSpace Y] (p : ∀ n, X n) (q : Y) :
    PointedGHConverges p q ↔
      ∀ (R : ℝ) (hR : 0 < R) (ε : ℝ) (_ : 0 < ε),
        ∀ᶠ n in Filter.atTop, ∃ f : ↥(Metric.ball (p n) R) → Y,
          Measurable f ∧ f ⟨p n, Metric.mem_ball_self hR⟩ = q ∧
            (∀ x y, |dist (f x) (f y) - dist (x : X n) (y : X n)| ≤ ε) ∧
            Metric.ball q (R - ε) ⊆ Metric.thickening ε (Set.range f)

Uses 1

Statement usesPointed Gromov–Hausdorff convergence

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.