Formal target: Corpus.Arxiv230301089FurstenbergTimesPTimesQ.conjecture_1_3

**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.

Exact formal statement

∀ {p q : Nat},
  LE.le.{0} 2 p →
    LE.le.{0} 2 q →
      Corpus.Arxiv230301089FurstenbergTimesPTimesQ.MultiplicativelyIndependent p q →
        ∀ {μ : MeasureTheory.Measure.{0} UnitAddCircle} [MeasureTheory.IsProbabilityMeasure.{0} μ]
          [Corpus.Arxiv230301089FurstenbergTimesPTimesQ.MeasureTheory.IsAtomLess.{0} μ],
          MeasureTheory.MeasurePreserving.{0, 0} (Corpus.Arxiv230301089FurstenbergTimesPTimesQ.Tn p) μ μ →
            MeasureTheory.MeasurePreserving.{0, 0} (Corpus.Arxiv230301089FurstenbergTimesPTimesQ.Tn q) μ μ →
              Eq.{1} μ MeasureTheory.MeasureSpace.volume.{0}

This target is a formal statement, not a proof of the problem.

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record