UnweightedAttractor.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

def OAI.EntropyRateDimension.Extensions.uniformSystem line 16
Source documentation
Every nonempty finite family of strict nonzero similarities admits positive normalized weights. The uniform choice is bookkeeping, not a geometric hypothesis.
```
noncomputable def uniformSystem (r t : ι → ℝ)
    (hr0 : ∀ i, 0 < |r i|) (hr1 : ∀ i, |r i| < 1) : System ι where
…
```
Mentions: OAI.EntropyRateDimension.System
def OAI.EntropyRateDimension.Extensions.unweightedAttractor line 31
Source documentation
Literal set of all coding limits for the unweighted similarity family.
```
def unweightedAttractor (r t : ι → ℝ)
    (hr0 : ∀ i, 0 < |r i|) (hr1 : ∀ i, |r i| < 1) : Set ℝ :=
…
```
theorem OAI.EntropyRateDimension.Extensions.unweightedAttractor_compact line 35

theorem OAI.EntropyRateDimension.Extensions.unweighted_existsUnique_similarityDimension line 41

Source documentation

The similarity exponent exists uniquely even for a one-symbol family.

theorem unweighted_existsUnique_similarityDimension (r t : ι → ℝ)
    (hr0 : ∀ i, 0 < |r i|) (hr1 : ∀ i, |r i| < 1) :
    ∃! s : ℝ, 0 ≤ s ∧ ∑ i, |r i| ^ s = 1 := by
…

theorem OAI.EntropyRateDimension.Extensions.unweighted_no_exact_overlaps_attractor_dimension_of_root line 50
Source documentation
Source cor:set for arbitrary unweighted finite similarities. The overlap hypothesis uses the manuscript's distinct nonempty finite-word convention, and the exponent is characterized by its literal normalization equation.
```
theorem unweighted_no_exact_overlaps_attractor_dimension_of_root
    (r t : ι → ℝ) (hr0 : ∀ i, 0 < |r i|) (hr1 : ∀ i, |r i| < 1)
    (s : ℝ) (hs : 0 ≤ s) (hroot : ∑ i, |r i| ^ s = 1)
    (hno : ∀ u v : List ι, u ≠ [] → v ≠ [] →
      (uniformSystem r t hr0 hr1).wordAffine u =
        (uniformSystem r t hr0 hr1).wordAffine v → u = v) :
    dimH (unweightedAttractor r t hr0 hr1) = ENNReal.ofReal (min 1 s) := by
…
```
Mentions: OAI.EntropyRateDimension.Extensions.uniformSystem, OAI.EntropyRateDimension.Extensions.unweightedAttractor

theorem OAI.EntropyRateDimension.Extensions.unweighted_no_exact_overlaps_attractor_dimension line 61

Source documentation

The same statement with the uniquely selected similarity exponent.

theorem unweighted_no_exact_overlaps_attractor_dimension
    (r t : ι → ℝ) (hr0 : ∀ i, 0 < |r i|) (hr1 : ∀ i, |r i| < 1)
    (hno : ∀ u v : List ι, u ≠ [] → v ≠ [] →
      (uniformSystem r t hr0 hr1).wordAffine u =
        (uniformSystem r t hr0 hr1).wordAffine v → u = v) :
    dimH (unweightedAttractor r t hr0 hr1) =
      ENNReal.ofReal (min 1 (similarityDimension (uniformSystem r t hr0 hr1))) := by
…

Mentions: OAI.EntropyRateDimension.Extensions.uniformSystem, OAI.EntropyRateDimension.Extensions.unweightedAttractor, OAI.EntropyRateDimension.Extensions.similarityDimension

theorem OAI.EntropyRateDimension.Extensions.unweighted_overlap_lengths line 72

Source documentation

Unweighted source lem:overlap-lengths; no probability data are inputs.

theorem unweighted_overlap_lengths
    (r t : ι → ℝ) (hr0 : ∀ i, 0 < |r i|) (hr1 : ∀ i, |r i| < 1)
    {u v : List ι} (hu : u ≠ []) (hv : v ≠ []) (hne : u ≠ v)
    (he : (uniformSystem r t hr0 hr1).wordAffine u =
      (uniformSystem r t hr0 hr1).wordAffine v) :
    ∃ a b : List ι, a ≠ [] ∧ b ≠ [] ∧ a.length = b.length ∧ a ≠ b ∧
      (uniformSystem r t hr0 hr1).wordAffine a =
        (uniformSystem r t hr0 hr1).wordAffine b :=
…

Mentions: OAI.EntropyRateDimension.Extensions.uniformSystem