NoOverlaps.lean`

23 declarations, 0 contain sorry, 0 declared as axioms

def OAI.EntropyRateDimension.Extensions.NoExactOverlaps line 15
Source documentation
Absence of equality between complete affine maps of distinct finite words.
Also declared: ComparatorChallenges/SelfSimilarCorollaries.lean:44 (same declaration text).
```
def NoExactOverlaps (S : System ι) : Prop := Function.Injective S.wordAffine
```
Mentions: OAI.EntropyRateDimension.System
def OAI.EntropyRateDimension.Extensions.symbolEntropy line 17
Also declared: ComparatorChallenges/SelfSimilarCorollaries.lean:46 (same declaration text).
def OAI.EntropyRateDimension.Extensions.SameLengthNoExactOverlaps line 21
Source documentation
The equivalent fixed-length convention for exact overlaps.
```
def SameLengthNoExactOverlaps (S : System ι) : Prop :=
…
```
Mentions: OAI.EntropyRateDimension.System
def OAI.EntropyRateDimension.Extensions.naturalLyapunov line 24
theorem OAI.EntropyRateDimension.Extensions.wordAffine_slope_pos line 27
theorem OAI.EntropyRateDimension.Extensions.wordAffine_slope_le_one line 34
theorem OAI.EntropyRateDimension.Extensions.wordAffine_slope_lt_one line 42
theorem OAI.EntropyRateDimension.Extensions.equal_map_prefix line 55
Source documentation
An equal prefix map cannot have a nonempty residual contraction.
```
theorem equal_map_prefix (S : System ι) (u w : List ι)
    (he : S.wordAffine u = S.wordAffine (u ++ w)) : w = [] := by
…
```
Mentions: OAI.EntropyRateDimension.System
theorem OAI.EntropyRateDimension.Extensions.prefix_comparison line 69
Source documentation
Prefix comparison extracted directly from equality of concatenations.
```
theorem prefix_comparison {α : Type uα} (u v x y : List α)
    (h : u ++ x = v ++ y) :
    (∃ w, v = u ++ w) ∨ (∃ w, u = v ++ w) := by
…
```

theorem OAI.EntropyRateDimension.Extensions.overlap_lengths line 85

Source documentation

Source lemma lem:overlap-lengths, with complete signed affine maps.

theorem overlap_lengths (S : System ι) {u v : List ι}
    (_hu : u ≠ []) (_hv : v ≠ []) (hne : u ≠ v)
    (he : S.wordAffine u = S.wordAffine v) :
    ∃ a b : List ι, a ≠ [] ∧ b ≠ [] ∧ a.length = b.length ∧
      a ≠ b ∧ S.wordAffine a = S.wordAffine b := by
…

Mentions: OAI.EntropyRateDimension.System

theorem OAI.EntropyRateDimension.Extensions.noExactOverlaps_sameLength line 106
theorem OAI.EntropyRateDimension.Extensions.sameLength_list_injective line 112
theorem OAI.EntropyRateDimension.Extensions.noExactOverlaps_iff_nonempty line 124
Source documentation
Adding the empty word does not strengthen the usual overlap assumption.
```
theorem noExactOverlaps_iff_nonempty (S : System ι) :
    NoExactOverlaps S ↔ ∀ u v : List ι, u ≠ [] → v ≠ [] →
      S.wordAffine u = S.wordAffine v → u = v := by
…
```
Mentions: OAI.EntropyRateDimension.System, OAI.EntropyRateDimension.Extensions.NoExactOverlaps
theorem OAI.EntropyRateDimension.Extensions.noExactOverlaps_iff_sameLength line 140
theorem OAI.EntropyRateDimension.Extensions.word_entropy line 151
Source documentation
Native product entropy of the symbol word; no random-walk entropy hypothesis.
```
theorem word_entropy (S : System ι) (n : ℕ) :
    FiniteEntropy.entropy Finset.univ (S.wordWeight (n := n)) =
…
```
Mentions: OAI.EntropyRateDimension.System, OAI.EntropyRateDimension.FiniteEntropy.entropy
theorem OAI.EntropyRateDimension.Extensions.walkEntropy_eq_symbolEntropy line 170
theorem OAI.EntropyRateDimension.Extensions.entropyRate_eq_symbolEntropy line 183
theorem OAI.EntropyRateDimension.Extensions.lyapunov_eq_naturalLyapunov line 195
theorem OAI.EntropyRateDimension.Extensions.no_exact_overlaps_dimension line 200
theorem OAI.EntropyRateDimension.Extensions.homogeneous_naturalLyapunov line 226
theorem OAI.EntropyRateDimension.Extensions.homogeneous_dimension line 231
def OAI.EntropyRateDimension.Extensions.threeMapSystem line 240
Source documentation
The three named translations, with all positivity and normalization supplied explicitly.
```
noncomputable def threeMapSystem (lam t : ℝ) (hlam : 0 < lam) (hlam1 : lam < 1)
    (p : Fin 3 → ℝ) (hp : ∀ i, 0 < p i) (hp1 : ∑ i, p i = 1) : System (Fin 3) where
…
```
Mentions: OAI.EntropyRateDimension.System
theorem OAI.EntropyRateDimension.Extensions.three_maps_dimension line 250