Theorems · Theorem · measure theory

dimH_image_le_of_locally_holder_on

∀ {X : Type u_2} {Y : Type u_3} [inst : EMetricSpace X] [inst_1 : EMetricSpace Y] [SecondCountableTopology X]
  {r : NNReal} {f : X → Y},
  0 < r → ∀ {s : Set X}, (∀ x ∈ s, ∃ C, ∃ t ∈ nhdsWithin x s, HolderOnWith C r f t) → dimH (f '' s) ≤ dimH s / ↑r

If s is a set in a space X with second countable topology and f : X → Y is Hölder continuous in a neighborhood within s of every point x ∈ s with the same positive exponent r but possibly different coefficients, then the Hausdorff dimension of the image f '' s is at most the Hausdorff dimension of s divided by r.

Defined in

Mathlib.Topology.MetricSpace.HausdorffDimension

Cited by

2 results in Mathlib

Foundations

Depth 212 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

EMetricSpaceEMetricSpaceSecondCountableTopology