Hausdorff dimension of self-similar sets

DefinitionAttractor of an iterated function system#✓fully proved

Let \(X\) be a topological space and let \((f_i)_{i < n}\) be a finite family of maps \(X \to X\). A set \(S \subseteq X\) is an attractor of the family if it is nonempty and compact and is fixed by the Hutchinson operator, that is, \(S = \bigcup_{i < n} f_i(S)\).

def IsAttractor {X : Type*} [TopologicalSpace X] {n : ℕ}
    (f : Fin n → X → X) (S : Set X) : Prop :=
  IsCompact S ∧ S.Nonempty ∧ S = ⋃ i, f i '' S

Used by 1

Used byMoran's equality for affine-symmetric iterated function systems

DefinitionAffine-symmetric iterated function system#✓fully proved

Let \((f_i)_{i < n}\) be a finite family of maps \(f_i \colon \mathbb{R}^d \to \mathbb{R}^d\) on Euclidean space. The family is affine-symmetric with common contraction factor \(\lambda\) if \(0 < \lambda < 1\) and there are linear isometries \(A_i \colon \mathbb{R}^d \to \mathbb{R}^d\) (orthogonal transformations) and vectors \(\beta_i \in \mathbb{R}^d\) such that \(f_i(x) = \lambda A_i(x) + \beta_i\) for every \(i < n\) and every \(x \in \mathbb{R}^d\).

def IsAffineSymmetricIFS {d n : ℕ}
    (f : Fin n → EuclideanSpace ℝ (Fin d) → EuclideanSpace ℝ (Fin d)) (lam : ℝ) :
    Prop :=
  0 < lam ∧ lam < 1 ∧
  ∃ A : Fin n → (EuclideanSpace ℝ (Fin d) →ₗᵢ[ℝ] EuclideanSpace ℝ (Fin d)),
    ∃ β : Fin n → EuclideanSpace ℝ (Fin d),
      ∀ i x, f i x = lam • A i x + β i

Used by 1

Used byMoran's equality for affine-symmetric iterated function systems

DefinitionOpen set condition#✓fully proved

A finite family of maps \(f_i \colon \mathbb{R}^d \to \mathbb{R}^d\), \(i < n\), satisfies the open set condition if there is a nonempty open set \(G \subseteq \mathbb{R}^d\) such that \(f_i(G) \subseteq G\) for every \(i < n\) and the images \(f_i(G)\) and \(f_j(G)\) are disjoint whenever \(i \neq j\).

def OpenSetCondition {d n : ℕ}
    (f : Fin n → EuclideanSpace ℝ (Fin d) → EuclideanSpace ℝ (Fin d)) : Prop :=
  ∃ G : Set (EuclideanSpace ℝ (Fin d)), IsOpen G ∧ G.Nonempty ∧
    (∀ i, f i '' G ⊆ G) ∧
    (∀ i j : Fin n, i ≠ j → Disjoint (f i '' G) (f j '' G))

Used by 1

Used byMoran's equality for affine-symmetric iterated function systems

TheoremMoran's equality for affine-symmetric iterated function systems#●ready to prove

Let \(n \ge 1\) and let \((f_i)_{i < n}\) be an affine-symmetric iterated function system on \(\mathbb{R}^d\) with common contraction factor \(\lambda \in (0,1)\) that satisfies the open set condition. Then every attractor \(S \subseteq \mathbb{R}^d\) of the system has Hausdorff dimension

\[\dim_H S = -\frac{\log n}{\log \lambda}.\]

public theorem_wanted moran_equality_affine
    {d n : ℕ} (hn : 1 ≤ n)
    (f : Fin n → EuclideanSpace ℝ (Fin d) → EuclideanSpace ℝ (Fin d)) (lam : ℝ)
    (h_aff : IsAffineSymmetricIFS f lam)
    (h_osc : OpenSetCondition f)
    {S : Set (EuclideanSpace ℝ (Fin d))} (hS : IsAttractor f S) :
    dimH S = ENNReal.ofReal (- Real.log n / Real.log lam)

Sources

• P. A. P. Moran, Additive functions of intervals and Hausdorff measure, Proc. Cambridge Philos. Soc. 42 (1946); J. E. Hutchinson, Fractals and self similarity, Indiana Univ. Math. J. 30 (1981). Knill, Some fundamental theorems in mathematics, §105. Problem moran_equality_affine of the lean-eval benchmark.

Uses 3

Statement usesAffine-symmetric iterated function system · Attractor of an iterated function system · Open set condition

3 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.