Furstenberg's times p, times q conjectures

Reference: arxiv/2303.01089 Around Furstenberg's times $p$, times $q$ conjecture: times $p$-invariant measures with some large Fourier coefficients by Catalin Badea, Sophie Grivaux

def Arxiv.id2303_01089.term𝕋 : Lean.ParserDescr

Equations

• Arxiv.id2303_01089.term𝕋 = Lean.ParserDescr.node `Arxiv.id2303_01089.term𝕋 1024 (Lean.ParserDescr.symbol "𝕋")

def Arxiv.id2303_01089.MultiplicativelyIndependent (p q : ℕ) : Prop

Two integers $p, q \ge 2$ are multiplicatively independent if $\log p / \log q$ is irrational.

Equations

• Arxiv.id2303_01089.MultiplicativelyIndependent p q = Irrational (Real.log ↑p / Real.log ↑q)

def Arxiv.id2303_01089.Tn (n : ℕ) (x : 𝕋) : 𝕋

The map $T_n$ sends $x$ to $nx \bmod 1$ on the additive circle.

Equations

• Arxiv.id2303_01089.Tn n x = n • x

theorem Arxiv.id2303_01089.Tn_continuous (n : ℕ) : Continuous (Tn n)

def Arxiv.id2303_01089.IsTnInvariant (n : ℕ) (F : Set 𝕋) : Prop

A set $F$ is $T_n$-invariant if $T_n(F) \subseteq F$.

Equations

• Arxiv.id2303_01089.IsTnInvariant n F = (Arxiv.id2303_01089.Tn n '' F ⊆ F)

def Arxiv.id2303_01089.MeasureTheory.IsAtom {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) (A : Set α) : Prop

A set $A$ is an atom if it has positive measure and for all $B \subseteq A$ measurable, either $\mu(B) = 0$ or $\mu(B) = \mu(A)$.

Equations

• Arxiv.id2303_01089.MeasureTheory.IsAtom μ A = (0 < μ A ∧ ∀ B ⊆ A, MeasurableSet B → μ B = 0 ∨ μ B = μ A)

class Arxiv.id2303_01089.MeasureTheory.IsAtomLess {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) : Prop

A measure is atomless if it has no atoms.

• NoAtoms (A : Set α) : MeasurableSet A → ¬IsAtom μ A

def Arxiv.id2303_01089.UnitAddCircle.ProbabilityMeasure : MeasureTheory.ProbabilityMeasure 𝕋

Equations

• Arxiv.id2303_01089.UnitAddCircle.ProbabilityMeasure = ⟨MeasureTheory.volume, Arxiv.id2303_01089.UnitAddCircle.ProbabilityMeasure._proof_2⟩

theorem Arxiv.id2303_01089.conjecture_1_3 {p q : ℕ} (hp : 2 ≤ p) (hq : 2 ≤ q) (hpq : MultiplicativelyIndependent p q) {μ : MeasureTheory.Measure 𝕋} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsAtomLess μ] (hmup : MeasureTheory.MeasurePreserving (Tn p) μ μ) (hmuq : MeasureTheory.MeasurePreserving (Tn q) μ μ) : μ = MeasureTheory.volume

Conjecture 1.3 (the $\times p, \times q$ conjecture): the only atomless Borel probability measure on $\mathbb{T}$ which is both $T_p$- and $T_q$-invariant is the Lebesgue measure.

theorem Arxiv.id2303_01089.conjecture_1_4 : False ↔ ∀ (p q : ℕ), 2 ≤ p → 2 ≤ q → MultiplicativelyIndependent p q → ∀ (μ : MeasureTheory.ProbabilityMeasure 𝕋), MeasureTheory.IsAtomLess ↑μ → MeasureTheory.MeasurePreserving (Tn p) ↑μ ↑μ → Filter.Tendsto (fun (n : ℕ) => μ.map ⋯) Filter.atTop (nhds UnitAddCircle.ProbabilityMeasure)

Conjecture 1.4: if $\mu$ is an atomless $T_p$-invariant Borel probability measure on $\mathbb{T}$, then $T_{q^n}\mu$ converges weak-star to Lebesgue measure. This paper disproves the conjecture.