HomogeneousDimension.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.EntropyRateDimension.Extensions.homogeneous_exponent_lower_direct line 12

Source documentation

Constant ratios need only one type in the entropy-gap contradiction.

theorem homogeneous_exponent_lower_direct {ι : Type uι} [Fintype ι] [Nonempty ι]
    (S : System ι) {lam : ℝ} (hr : ∀ i, S.ratio i = lam)
    (μ : Measure ℝ) [IsProbabilityMeasure μ] (hμ : S.SelfSimilar μ) :
    min 1 (S.entropyRate / S.lyapunov) ≤ Coding.exponent S := by
…

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

theorem OAI.EntropyRateDimension.Extensions.homogeneous_dimension_direct line 34
Source documentation
Same hypotheses and conclusion as homogeneous_dimension; independent proof branch.
Distinct definitions of this name: ComparatorChallenges/SelfSimilarCorollaries.lean:49 (same statement text; different proof or body). Qualify references as OAI.EntropyRateDimension.Extensions.homogeneous_dimension_direct@path.
```
theorem homogeneous_dimension_direct {ι : Type uι} [Fintype ι] [Nonempty ι] (S : System ι)
    {lam : ℝ} (hlam : 0 < lam) (hr : ∀ i, S.ratio i = lam)
    (μ : Measure ℝ) [IsProbabilityMeasure μ] (hμ : S.SelfSimilar μ)
    (h : NoExactOverlaps S) :
    lowerHausdorffDimension μ =
      ENNReal.ofReal (min 1 (symbolEntropy S / Real.log (1/lam))) := by
…
```
Mentions: OAI.EntropyRateDimension.System, OAI.EntropyRateDimension.Extensions.NoExactOverlaps, OAI.EntropyRateDimension.Extensions.symbolEntropy