Reduction.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Conditional dynamical reduction for the prime-degree packet theorem

A ball cover with a dimension gap gives exponential tube decay. Entropy in almost every ergodic component, followed by prime-degree rigidity, then identifies the mixture with Haar probability.

The dynamical criteria are specialized as follows:

ELMV (2009), Corollary 3.3: a flow-invariant probability with compact-uniform two-sided tube bound exp(-2ηt) has entropy at least η.
Rokhlin (1967), Theorem 9.8: entropy of a normalized restriction of an invariant component decomposition is its component entropy integral.
EKL (2006), Theorem 1.3 and Corollary 1.4: a diagonal-invariant ergodic probability with positive entropy on the prime-degree lattice space is Haar probability.

def OAI.DukePrimeDegree.ELMVConstantSequenceCriterion line 35
Source documentation
The constant-sequence specialization of the published two-sided tube criterion. The application must use the source's actual flow and tubes.
```
def ELMVConstantSequenceCriterion (flow : ℝ → X → X)
    (tube : ℝ → X → Set X) : Prop :=
…
```
def OAI.DukePrimeDegree.RokhlinRestrictionFormula line 43
Source documentation
The restriction case of the published entropy integral formula.
```
def RokhlinRestrictionFormula (τ : Measure Z) (κ : Z → Measure X)
    (flow : ℝ → X → X) : Prop :=
…
```
def OAI.DukePrimeDegree.BallTubeCovers line 50
Source documentation
Covers by balls with mass exponent n and covering exponent n-1.
```
def BallTubeCovers (μ : Measure X) (tube : ℝ → X → Set X)
    (n : ℕ) (rate : ℝ) : Prop :=
…
```

theorem OAI.DukePrimeDegree.ae_positive_metricEntropy_of_ballTubeCovers line 62

Source documentation

Every component has positive entropy almost everywhere, using the actual Kolmogorov--Sinai entropy definition and precisely stated inputs.

theorem ae_positive_metricEntropy_of_ballTubeCovers
    (τ : Measure Z) [IsProbabilityMeasure τ]
    (κ : Z → Measure X) (hκ : Measurable κ)
    (hprob : ∀ z, IsProbabilityMeasure (κ z))
    (flow : ℝ → X → X) (hflow : ∀ t, Measurable (flow t))
    (hinv : ∀ t z, Measure.map (flow t) (κ z) = κ z)
    (tube : ℝ → X → Set X) (n : ℕ) (hn : 1 ≤ n)
    (rate : ℝ) (hrate : 0 < rate)
    (covers : BallTubeCovers (τ.bind κ) tube n rate)
    (hentropy : Measurable (fun z => metricEntropy (flow 1) (κ z)))
    (rokhlin : RokhlinRestrictionFormula τ κ flow)
    (elmv : ELMVConstantSequenceCriterion flow tube) :
…

Mentions: OAI.DukePrimeDegree.BallTubeCovers, OAI.DukePrimeDegree.metricEntropy, OAI.DukePrimeDegree.RokhlinRestrictionFormula, OAI.DukePrimeDegree.ELMVConstantSequenceCriterion

theorem OAI.DukePrimeDegree.mixture_eq_of_ballTubeCovers line 89

Source documentation

The final dynamical reduction: positive entropy in almost every component, followed by rigidity and integration, identifies the mixture. The group action and the EKL implication must be specialized to the prime-degree homogeneous lattice space before this applies to packets.

theorem mixture_eq_of_ballTubeCovers
    (G : Type*) [Group G] [MulAction G X]
    (τ : Measure Z) [IsProbabilityMeasure τ]
    (κ : Z → Measure X) (hκ : Measurable κ)
    (hprob : ∀ z, IsProbabilityMeasure (κ z))
    (hergodic : ∀ᵐ z ∂τ, ErgodicSMul G X (κ z))
    (flow : ℝ → X → X) (hflow : ∀ t, Measurable (flow t))
    (hinv : ∀ t z, Measure.map (flow t) (κ z) = κ z)
    (tube : ℝ → X → Set X) (n : ℕ) (hn : 1 ≤ n)
    (rate : ℝ) (hrate : 0 < rate)
    (covers : BallTubeCovers (τ.bind κ) tube n rate)
    (hentropy : Measurable (fun z => metricEntropy (flow 1) (κ z)))
…

Mentions: OAI.DukePrimeDegree.BallTubeCovers, OAI.DukePrimeDegree.metricEntropy