Entropy.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

The ergodic-component step for prime-degree torus packets

The entropy functional is a parameter whose restricted-mixture formula is the specialization of Rokhlin, Lectures on the entropy theory of measure-preserving transformations (1967), Theorem 9.8. The measurable probability kernel and its restricted-mixture formula are hypotheses; the decomposition theorem of Greschonig--Schmidt (2000), Theorem 5.2, gives such kernels for invariant probabilities.

In particular, a lower bound for the entropy of a measure alone is not used to infer positive entropy in almost every component. The lower bound must hold for every invariant probability dominated by a finite multiple of that measure.

def OAI.DukePrimeDegree.restrictedMixture line 32
Source documentation
The probability obtained by retaining a positive-measure collection of components and renormalizing.
```
noncomputable def restrictedMixture (τ : Measure Z) (κ : Z → Measure X)
    (s : Set Z) : Measure X :=
…
```
lemma OAI.DukePrimeDegree.restricted_bind_le line 36
lemma OAI.DukePrimeDegree.restrictedMixture_le line 45
lemma OAI.DukePrimeDegree.restrictedMixture_probability line 53

lemma OAI.DukePrimeDegree.map_bind_eq_of_component_invariant line 66

Source documentation

Taking mixtures commutes with a measurable transformation that fixes every component.

lemma map_bind_eq_of_component_invariant (τ : Measure Z) (κ : Z → Measure X)
    (hκ : Measurable κ) (T : X → X) (hT : Measurable T)
    (hinv : ∀ z, Measure.map T (κ z) = κ z) :
    Measure.map T (τ.bind κ) = τ.bind κ := by
…

lemma OAI.DukePrimeDegree.restrictedMixture_invariant line 78

theorem OAI.DukePrimeDegree.ae_positive_component_entropy line 94

Source documentation

The domination argument for the zero-entropy components.

hformula is only the restriction case of the published entropy integral formula. hpositive is the manuscript's preceding ball-to-entropy result, which has to be established separately. The proof constructs the normalized zero-entropy submixture, proves its domination and invariance, and obtains a contradiction.

theorem ae_positive_component_entropy
    (τ : Measure Z) [IsProbabilityMeasure τ]
    (κ : Z → Measure X) (hκ : Measurable κ)
    (hprob : ∀ z, IsProbabilityMeasure (κ z))
    (T : I → X → X) (hT : ∀ i, Measurable (T i))
    (hinv : ∀ i z, Measure.map (T i) (κ z) = κ z)
    (entropy : Measure X → ℝ≥0∞)
    (hentropy : Measurable (fun z => entropy (κ z)))
    (hformula : ∀ s, MeasurableSet s → τ s ≠ 0 →
      entropy (restrictedMixture τ κ s) =
        (τ s)⁻¹ * ∫⁻ z in s, entropy (κ z) ∂τ)
    (hpositive : ∀ ξ : Measure X, IsProbabilityMeasure ξ →
…

Mentions: OAI.DukePrimeDegree.restrictedMixture

theorem OAI.DukePrimeDegree.bind_eq_of_ae_eq line 132
Source documentation
A probability mixture of almost-everywhere identical components is that same probability. This is the final integration step after the prime-degree rigidity theorem identifies the ergodic components.
```
theorem bind_eq_of_ae_eq (τ : Measure Z) [IsProbabilityMeasure τ]
    (κ : Z → Measure X) (m : Measure X) (heq : ∀ᵐ z ∂τ, κ z = m) :
    τ.bind κ = m := by
…
```
theorem OAI.DukePrimeDegree.bind_eq_of_positive_entropy_rigidity line 141
Source documentation
Combine the preceding component argument with the application-specific rigidity implication. For torus packets, hrigid is supplied by Einsiedler--Katok--Lindenstrauss (2006), Theorem 1.3 and Corollary 1.4, after checking prime degree and ergodicity.
```
theorem bind_eq_of_positive_entropy_rigidity
    (τ : Measure Z) [IsProbabilityMeasure τ]
    (κ : Z → Measure X) (entropy : Measure X → ℝ≥0∞) (m : Measure X)
    (hpositive : ∀ᵐ z ∂τ, 0 < entropy (κ z))
    (hrigid : ∀ᵐ z ∂τ, 0 < entropy (κ z) → κ z = m) :
    τ.bind κ = m := by
…
```