ComparatorChallenges/Rokhlin.lean

GitHub source file

5 declarations, 1 contain sorry, 0 declared as axioms

1. def OAI.Rokhlin.timeMap Challenge statement: Rokhlin’s multiple-mixing problem line 12

   L4DEL explanation

   Rokhlin's multiple-mixing problem asks whether ordinary mixing of one invertible probability-preserving transformation implies mixing of every finite order. The formalization proves this implication. For each $k\ge3$ and every $k$ measurable sets, the measure of their translated intersection tends to the product of their measures as all successive time gaps tend to infinity.

   1. This is an exact comparator target linked by the pinned repository's formalization note for this result.
   2. The repository's comparator configuration selects OAI.Dynamics.MultipleMixing.Main as the released solution module checked against this declaration.

   Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)

   Also declared: OAI/Dynamics/MultipleMixing/HilbertCodes.lean:20 (same declaration text).

   def timeMap (T : Ω ≃ᵐ Ω) (n : ℤ) : Ω → Ω :=
   …

2. def OAI.Rokhlin.IsMixing Challenge statement: Rokhlin’s multiple-mixing problem line 15

   L4DEL explanation

   Rokhlin's multiple-mixing problem asks whether ordinary mixing of one invertible probability-preserving transformation implies mixing of every finite order. The formalization proves this implication. For each $k\ge3$ and every $k$ measurable sets, the measure of their translated intersection tends to the product of their measures as all successive time gaps tend to infinity.

   1. This is an exact comparator target linked by the pinned repository's formalization note for this result.
   2. The repository's comparator configuration selects OAI.Dynamics.MultipleMixing.Main as the released solution module checked against this declaration.

   Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)

   Also declared: OAI/Dynamics/MultipleMixing/HilbertCodes.lean:23 (same declaration text).

   def IsMixing (μ : Measure Ω) (T : Ω ≃ᵐ Ω) : Prop :=
   …

3. def OAI.Rokhlin.layoutTime Challenge statement: Rokhlin’s multiple-mixing problem line 20

   L4DEL explanation

   Rokhlin's multiple-mixing problem asks whether ordinary mixing of one invertible probability-preserving transformation implies mixing of every finite order. The formalization proves this implication. For each $k\ge3$ and every $k$ measurable sets, the measure of their translated intersection tends to the product of their measures as all successive time gaps tend to infinity.

   1. This is an exact comparator target linked by the pinned repository's formalization note for this result.
   2. The repository's comparator configuration selects OAI.Dynamics.MultipleMixing.Main as the released solution module checked against this declaration.

   Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)

   Also declared: OAI/Dynamics/MultipleMixing/HilbertCodes.lean:28 (same declaration text).

   def layoutTime {k : ℕ} (gaps : Fin (k - 1) → ℕ+) (i : Fin k) : ℕ :=
   …

4. def OAI.Rokhlin.MixingOfOrder Challenge statement: Rokhlin’s multiple-mixing problem line 23

   L4DEL explanation

   Rokhlin's multiple-mixing problem asks whether ordinary mixing of one invertible probability-preserving transformation implies mixing of every finite order. The formalization proves this implication. For each $k\ge3$ and every $k$ measurable sets, the measure of their translated intersection tends to the product of their measures as all successive time gaps tend to infinity.

   1. This is an exact comparator target linked by the pinned repository's formalization note for this result.
   2. The repository's comparator configuration selects OAI.Dynamics.MultipleMixing.Main as the released solution module checked against this declaration.

   Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)

   Also declared: OAI/Dynamics/MultipleMixing/HilbertCodes.lean:31 (same declaration text).

   def MixingOfOrder (μ : Measure Ω) (T : Ω ≃ᵐ Ω) (k : ℕ) : Prop :=
   …

5. theorem OAI.Rokhlin.mixing_all_finite_orders Challenge statement: Ordinary mixing implies mixing of every finite order sorry line 30

   L4DEL explanation

   Every invertible mixing probability-preserving transformation is mixing of every finite order

   Rohlin asked in 1949 whether 2-fold mixing implies 3-fold mixing for a stationary process indexed by Z

   Every invertible probability-preserving transformation that is mixing for pairs of measurable sets is mixing for every finite number of sets when all successive time gaps diverge.

   1. IsMixing says μ(A ∩ T⁻ⁿB) tends to μ(A)μ(B) as the absolute integer time tends to infinity, for every measurable pair A,B.
   2. layoutTime builds ordered observation times from positive gaps. MixingOfOrder k asks the measure of the intersection of all k translated sets to converge to the product of their measures as the entire gap vector tends to infinity.
   3. The theorem assumes an arbitrary probability measure, an invertible measurable equivalence preserving that measure, and ordinary mixing. It concludes MixingOfOrder k for every k≥3; no standardness or countable-generation hypothesis appears in the Lean statement.
   4. De la Rue's 2006 paper records the twofold-to-threefold question as still open at that time. The comparator body here is sorry, paired with OAI.Dynamics.MultipleMixing.Main; the linked manuscript supplies the claimed affirmative proof exposition.

   Sources and attribution: Pinned Lean source (fd4aeeb2ee4f), OpenAI Rokhlin multiple-mixing manuscript (abstract), Pinned OpenAI formalization note 145, Thierry de la Rue (2006), arXiv v1 abstract

   Distinct definitions of this name: OAI/Dynamics/MultipleMixing/Main.lean:317 (same statement text; different proof or body). Qualify references as OAI.Rokhlin.mixing_all_finite_orders@path.

   mixing of order k: asymptotic factorization of every k-fold translated intersection when all consecutive time gaps diverge

   theorem mixing_all_finite_orders (μ : Measure Ω) [IsProbabilityMeasure μ]
       (T : Ω ≃ᵐ Ω) (h_pres : MeasurePreserving T μ μ) (h_mix : IsMixing μ T) :
       ∀ k : ℕ, 3 ≤ k → MixingOfOrder μ T k := by
   …

   Mentions: OAI.Rokhlin.IsMixing, OAI.Rokhlin.MixingOfOrder