OAI/MeasureTheory/SelfSimilar/AttractorDimension.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.EntropyRateDimension.Extensions.similaritySum line 15
  2. theorem OAI.EntropyRateDimension.Extensions.similaritySum_strictAnti line 17
  3. theorem OAI.EntropyRateDimension.Extensions.existsUnique_similarityDimension line 23

    Source documentation

    Includes the one-symbol boundary: no assumption of at least two symbols.

    theorem existsUnique_similarityDimension (S : System ι) :
    ∃! s : ℝ, 0 ≤ s ∧ similaritySum S s = 1 := by
…

    Mentions: OAI.EntropyRateDimension.System, OAI.EntropyRateDimension.Extensions.similaritySum

  4. def OAI.EntropyRateDimension.Extensions.similarityDimension line 48
  5. theorem OAI.EntropyRateDimension.Extensions.similarityDimension_nonneg line 51
  6. theorem OAI.EntropyRateDimension.Extensions.similarityDimension_equation line 54
  7. theorem OAI.EntropyRateDimension.Extensions.similarityDimension_single_symbol line 58
  8. def OAI.EntropyRateDimension.Extensions.similaritySystem line 64
  9. theorem OAI.EntropyRateDimension.Extensions.similaritySystem_attractor line 75
  10. theorem OAI.EntropyRateDimension.Extensions.similaritySystem_noExactOverlaps line 80
  11. theorem OAI.EntropyRateDimension.Extensions.similaritySystem_entropy line 96
  12. theorem OAI.EntropyRateDimension.Extensions.naturalLyapunov_pos line 106
  13. theorem OAI.EntropyRateDimension.Extensions.coding_law_attractor_mass line 112
  14. theorem OAI.EntropyRateDimension.Extensions.coding_law_dimension_le_attractor line 121
  15. theorem OAI.EntropyRateDimension.Extensions.no_exact_overlaps_attractor_dimension_of_root line 127

    Source documentation

    The set-dimension corollary for an arbitrary normalized similarity exponent.

    theorem no_exact_overlaps_attractor_dimension_of_root (S : System ι) {s : ℝ}
    (hs : 0 ≤ s) (hroot : ∑ i, |S.ratio i| ^ s = 1) (h : NoExactOverlaps S) :
    dimH (attractor S) = ENNReal.ofReal (min 1 s) := by
…

    Mentions: OAI.EntropyRateDimension.System, OAI.EntropyRateDimension.Extensions.NoExactOverlaps, OAI.EntropyRateDimension.Extensions.attractor

  16. theorem OAI.EntropyRateDimension.Extensions.no_exact_overlaps_attractor_dimension line 145

    Source documentation

    Source corollary cor:set, with the genuine compact coding attractor and the uniquely constructed similarity dimension; the one-map case is included.

    theorem no_exact_overlaps_attractor_dimension (S : System ι) (h : NoExactOverlaps S) :
    dimH (attractor S) = ENNReal.ofReal (min 1 (similarityDimension S)) :=
…

    Mentions: OAI.EntropyRateDimension.System, OAI.EntropyRateDimension.Extensions.NoExactOverlaps, OAI.EntropyRateDimension.Extensions.attractor, OAI.EntropyRateDimension.Extensions.similarityDimension