Dimension functions for Hausdorff measures

StructureHausdorff dimension function#✓fully proved

A Hausdorff dimension function (gauge) is a continuous, non-decreasing function \(\psi : [0,\infty) \to [0,\infty)\) with \(\psi(0) = 0\) and \(\psi(r) > 0\) for every \(r > 0\). In particular \(\psi(r) \to 0\) as \(r \to 0^+\).

structure HausdorffDimensionFunction : Type extends (ℝ≥0 →Co ℝ≥0) where
  map_zero' : toFun 0 = 0
  map_pos' : ∀ {r : ℝ≥0}, 0 < r → 0 < toFun r

Sources

• Das and Simmons, arXiv:2305.11829v1, line 211; the source gauge on \((0,\infty)\) is extended by \(\psi(0) = 0\), and "increasing" is read as non-decreasing.

Used by 6

Used byContinuity of a Hausdorff dimension function · A Hausdorff dimension function vanishes only at zero · A Hausdorff dimension function is positive at positive radii · A Hausdorff dimension function vanishes at zero · Monotonicity of a Hausdorff dimension function · A Hausdorff dimension function tends to zero at zero

TheoremContinuity of a Hausdorff dimension function#✓fully proved

Every Hausdorff dimension function \(\psi : [0,\infty) \to [0,\infty)\) is continuous.

theorem continuous (ψ : HausdorffDimensionFunction) : Continuous (ψ : ℝ≥0 → ℝ≥0)

Uses 1 · Used by 1

Statement usesHausdorff dimension function

Used byA Hausdorff dimension function tends to zero at zero

TheoremMonotonicity of a Hausdorff dimension function#✓fully proved

Every Hausdorff dimension function \(\psi : [0,\infty) \to [0,\infty)\) is non-decreasing: if \(r \le s\) then \(\psi(r) \le \psi(s)\).

theorem monotone (ψ : HausdorffDimensionFunction) : Monotone (ψ : ℝ≥0 → ℝ≥0)

Uses 1

Statement usesHausdorff dimension function

TheoremA Hausdorff dimension function vanishes at zero#✓fully proved

Every Hausdorff dimension function \(\psi\) satisfies \(\psi(0) = 0\).

@[simp]
theorem map_zero (ψ : HausdorffDimensionFunction) : ψ (0 : ℝ≥0) = 0

Uses 1 · Used by 2

Statement usesHausdorff dimension function

Used byA Hausdorff dimension function vanishes only at zero · A Hausdorff dimension function tends to zero at zero

TheoremA Hausdorff dimension function is positive at positive radii#✓fully proved

If \(\psi\) is a Hausdorff dimension function and \(r > 0\) is a real number, then \(\psi(r) > 0\).

theorem map_pos (ψ : HausdorffDimensionFunction) {r : ℝ≥0} (hr : 0 < r) : 0 < ψ r

Uses 1 · Used by 1

Statement usesHausdorff dimension function

Used byA Hausdorff dimension function vanishes only at zero

TheoremA Hausdorff dimension function vanishes only at zero#✓fully proved

If \(\psi\) is a Hausdorff dimension function and \(r \ge 0\), then \(\psi(r) = 0\) if and only if \(r = 0\).

theorem map_eq_zero_iff (ψ : HausdorffDimensionFunction) {r : ℝ≥0} : ψ r = 0 ↔ r = 0

Uses 3

Statement usesHausdorff dimension function

Proof usesA Hausdorff dimension function is positive at positive radii · A Hausdorff dimension function vanishes at zero

TheoremA Hausdorff dimension function tends to zero at zero#✓fully proved

Every Hausdorff dimension function \(\psi\) satisfies \(\psi(r) \to 0\) as \(r \to 0^+\), that is, as \(r\) tends to \(0\) through positive values.

theorem tendsto_zero (ψ : HausdorffDimensionFunction) :
    Tendsto (ψ : ℝ≥0 → ℝ≥0) (𝓝[>] (0 : ℝ≥0)) (𝓝 0)

Uses 3

Statement usesHausdorff dimension function

Proof usesContinuity of a Hausdorff dimension function · A Hausdorff dimension function vanishes at zero

7 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.