AttractorFormula.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

def OAI.CorSetReference.codingPoint line 15
Source documentation
All infinite addresses, not an almost-everywhere image.
Also declared: ComparatorChallenges/SelfSimilarCorollaries.lean:66 (same declaration text).
```
noncomputable def codingPoint (r t : ι → ℝ) (ω : ℕ → ι) : ℝ :=
…
```
def OAI.CorSetReference.attractor line 19
Source documentation
The manuscript explicitly identifies its compact attractor with coding limits.
Also declared: ComparatorChallenges/SelfSimilarCorollaries.lean:70 (same declaration text).
```
noncomputable def attractor (r t : ι → ℝ) : Set ℝ :=
…
```
def OAI.CorSetReference.word line 23
Source documentation
Full affine coefficients of the composition in address order.
Also declared: ComparatorChallenges/SelfSimilarCorollaries.lean:74 (same declaration text).
```
def word (r t : ι → ℝ) : List ι → ℝ × ℝ :=
…
```

theorem OAI.CorSetReference.cor_set line 32

Source documentation

The compact coding attractor and its similarity and Hausdorff dimensions.

Distinct definitions of this name: ComparatorChallenges/SelfSimilarCorollaries.lean:78 (same statement text; different proof or body). Qualify references as OAI.CorSetReference.cor_set@path.

theorem cor_set {ι : Type uι} [Fintype ι] [Nonempty ι]
    (r t : ι → ℝ) (hr0 : ∀ i, 0 < |r i|) (hr1 : ∀ i, |r i| < 1)
    (hno : ∀ u v : List ι, u ≠ [] → v ≠ [] →
      word r t u = word r t v → u = v) :
    IsCompact (attractor r t) ∧ (attractor r t).Nonempty ∧
    (∃! s : ℝ, 0 ≤ s ∧ ∑ i, |r i| ^ s = 1) ∧
    (∀ s : ℝ, 0 ≤ s → (∑ i, |r i| ^ s = 1) →
      dimH (attractor r t) = ENNReal.ofReal (min 1 s)) := by
…

Mentions: OAI.CorSetReference.word, OAI.CorSetReference.attractor