Multiplicative recurrence along Pythagorean pairs

DefinitionPythagorean-pair recurrence problem (AMR-047-0034)#✓fully proved

The proposition that for every probability space \((X, \mu)\) and every family \((T_a)_{a \ge 1}\), indexed by the positive integers, of measurable bijections of \(X\) with measurable inverses that preserve \(\mu\), such that \(T_1\) is the identity and \(T_{ab} = T_a \circ T_b\) for all positive integers \(a, b\), every measurable set \(A \subseteq X\) with \(\mu(A) > 0\) admits positive integers \(m > n\) with

\[\mu\bigl(T_{2mn}(A) \cap T_{(m-n)(m+n)}(A)\bigr) > 0.\]

def conjecture : Prop :=
  ∀ (X : Type u) [MeasurableSpace X] (μ : MeasureTheory.Measure X)
    [MeasureTheory.IsProbabilityMeasure μ]
    (T : ℕ+ → (X ≃ᵐ X)),
    T 1 = MeasurableEquiv.refl X →
    (∀ a b : ℕ+, (T (a * b)).toEquiv = (T a).toEquiv * (T b).toEquiv) →
    (∀ a, MeasureTheory.MeasurePreserving (T a : X → X) μ μ) →
    ∀ A : Set X, MeasurableSet A → 0 < μ A →
      ∃ m n : ℕ+, n < m ∧
        0 < μ (⇑(T (2 * m * n)) '' A ∩
          ⇑(T ((m - n) * (m + n))) '' A)

Used by 1

Used byMultiplicative recurrence along Pythagorean pairs

TheoremMultiplicative recurrence along Pythagorean pairs#●ready to prove

Let \((X, \mu)\) be a probability space and let \((T_a)_{a \ge 1}\), indexed by the positive integers, be measurable bijections of \(X\) with measurable inverses that preserve \(\mu\), such that \(T_1\) is the identity and \(T_{ab} = T_a \circ T_b\) for all positive integers \(a, b\). Then for every measurable set \(A \subseteq X\) with \(\mu(A) > 0\) there exist positive integers \(m > n\) such that

\[\mu\bigl(T_{2mn}(A) \cap T_{(m-n)(m+n)}(A)\bigr) > 0.\]

Resolved true: Resolved by Frantzikinakis-Klurman-Moreira, Partition Regularity of Pythagorean Pairs (arXiv:2309.10636), Theorem 2.1(i): applied with coefficients 1 and 2 to the inverse family, it yields the two forward-image indices of AMR-047-0034. The statement is retained as a resolved target. Source: Frantzikinakis, Klurman, Moreira, Partition Regularity of Pythagorean Pairs, arXiv:2309.10636, Theorem 2.1(i), https://arxiv.org/abs/2309.10636. Moved from OpenConjectures/Dynamics/MultStructureRecurrence.

public theorem_wanted conjecture_holds : conjecture

Uses 1

Statement usesPythagorean-pair recurrence problem (AMR-047-0034)

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.