OAI/MeasureTheory/SelfSimilar/Attractor.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.EntropyRateDimension.Extensions.attractor line 15

   Source documentation

   The actual coding attractor, including every address, not merely an a.e. carrier.

   def attractor (S : System ι) : Set ℝ := Set.range (Coding.point S)

   Mentions: OAI.EntropyRateDimension.System, OAI.EntropyRateDimension.Coding.point

2. theorem OAI.EntropyRateDimension.Extensions.point_continuous line 17
3. theorem OAI.EntropyRateDimension.Extensions.attractor_compact line 33
4. theorem OAI.EntropyRateDimension.Extensions.attractor_nonempty line 38
5. def OAI.EntropyRateDimension.Extensions.cylinderRatio line 41
6. theorem OAI.EntropyRateDimension.Extensions.affine_lipschitz line 44
7. theorem OAI.EntropyRateDimension.Extensions.wordMap_lipschitz line 52
8. theorem OAI.EntropyRateDimension.Extensions.cylinderRatio_le line 70
9. theorem OAI.EntropyRateDimension.Extensions.cylinderRatio_power_sum line 81

   Source documentation

   Exact finite-word partition function, valid whether or not cylinders overlap.

   theorem cylinderRatio_power_sum [Nonempty ι] (S : System ι) {s : ℝ} (hs : 0 ≤ s)
       (hroot : ∑ i, |S.ratio i| ^ s = 1) (n : ℕ) :
       ∑ w : Fin n → ι, (cylinderRatio S w : ℝ≥0∞) ^ s = 1 := by
   …

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

10. theorem OAI.EntropyRateDimension.Extensions.attractor_subset_cylinders line 103

    Source documentation

    At every depth the genuine finite-word cylinders cover every coding limit.

    theorem attractor_subset_cylinders [Nonempty ι] (S : System ι) (n : ℕ) :
        attractor S ⊆ ⋃ w : Fin n → ι, S.wordMap w '' attractor S := by
    …

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

11. theorem OAI.EntropyRateDimension.Extensions.attractor_hausdorffMeasure_le line 124

    Source documentation

    The cylinder cover proves finite Hausdorff measure at the similarity exponent. No separation hypothesis and no assumed covering estimate enter this theorem.

    theorem attractor_hausdorffMeasure_le [Nonempty ι] (S : System ι) {s : ℝ} (hs : 0 ≤ s)
        (hroot : ∑ i, |S.ratio i| ^ s = 1) :
        Measure.hausdorffMeasure s (attractor S) ≤ Metric.ediam (attractor S) ^ s := by
    …

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

12. theorem OAI.EntropyRateDimension.Extensions.attractor_dim_le_similarity line 164
13. theorem OAI.EntropyRateDimension.Extensions.attractor_dim_le_one line 174
14. theorem OAI.EntropyRateDimension.Extensions.attractor_dim_single_symbol line 178

    Source documentation

    The single-symbol boundary genuinely has a singleton coding image.

    theorem attractor_dim_single_symbol [Nonempty ι] [Subsingleton ι] (S : System ι) :
        dimH (attractor S) = 0 := by
    …

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