Pointwise ergodic theorems for non-conventional bilinear polynomial averages

Problem statement

Notes: Unavailable.

Source: B. Krause, M. Mirek, and T. Tao, `Pointwise ergodic theorems for non-conventional bilinear polynomial averages`, Annals of Math, 195 (3) 2022. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge (v1.0.0, e32eb14), AnnalsChallenge/AnnalsOfMathematics/2022-195-3-PointwiseErgodicTheorems.lean

Informal solution: Unavailable.

/--
Statement of Theorem 1.17(i) (Mean ergodic theorem):

The averages `A T N X P f g` converge as `N → ∞` in `Lᵖ(X)` norm.
-/
theorem declaration uses `sorry`theorem_1_17_i {f g : 𝓧 → ℂ} (hf : MemLp f p₁ μ) (hg : MemLp g p₂ μ) :
    ∃ h : 𝓧 → ℂ, MemLp h p μ ∧
    Tendsto (fun N ↦ eLpNorm (A T N (X : ℤ[X]) P f g - h) p μ) atTop (𝓝 0) := by𝓧:Type u_1σX:MeasurableSpace 𝓧μ:Measure 𝓧inst✝:SigmaFinite μT:𝓧 ≃ᵐ 𝓧hT:MeasurePreserving (⇑T) μ μP:ℤ[X]hP:P.degree ≥ 2p₁:ℝ≥0∞p₂:ℝ≥0∞p:ℝ≥0∞h₁p₁:1 < p₁h₁p₂:1 < p₂h₂p₁:p₁ < ∞h₂p₂:p₂ < ∞hp₁p₂p:p₁⁻¹ + p₂⁻¹ = p⁻¹hp:p⁻¹ ≤ 1f:𝓧 → ℂg:𝓧 → ℂhf:MemLp f p₁ μhg:MemLp g p₂ μ⊢ ∃ h, MemLp h p μ ∧ Tendsto (fun N => eLpNorm (A T N X P f g - h) p μ) atTop (𝓝 0)
  sorryAll goals completed! 🐙

/--
Statement of Theorem 1.16(ii) (Pointwise ergodic theorem):

The averages `A T N X P f g` converge as `N → ∞` pointwise almost everywhere.
-/
theorem declaration uses `sorry`theorem_1_17_ii {f g : 𝓧 → ℂ} (hf : MemLp f p₁ μ) (hg : MemLp g p₂ μ) :
    ∃ h : 𝓧 → ℂ, MemLp h p μ ∧
    ∀ᵐ x ∂μ, Tendsto (fun N ↦ A T N (X : ℤ[X]) P f g x) atTop (𝓝 (h x)) := by𝓧:Type u_1σX:MeasurableSpace 𝓧μ:Measure 𝓧inst✝:SigmaFinite μT:𝓧 ≃ᵐ 𝓧hT:MeasurePreserving (⇑T) μ μP:ℤ[X]hP:P.degree ≥ 2p₁:ℝ≥0∞p₂:ℝ≥0∞p:ℝ≥0∞h₁p₁:1 < p₁h₁p₂:1 < p₂h₂p₁:p₁ < ∞h₂p₂:p₂ < ∞hp₁p₂p:p₁⁻¹ + p₂⁻¹ = p⁻¹hp:p⁻¹ ≤ 1f:𝓧 → ℂg:𝓧 → ℂhf:MemLp f p₁ μhg:MemLp g p₂ μ⊢ ∃ h, MemLp h p μ ∧ ∀ᵐ (x : 𝓧) ∂μ, Tendsto (fun N => A T N X P f g x) atTop (𝓝 (h x))
  sorryAll goals completed! 🐙

/-- The constant of Theorem 1.17 (iii). -/
noncomputable def declaration uses `sorry`Cᵢᵢᵢ (P : ℤ[X]) (p₁ p₂ : ℝ≥0∞) : ℝ≥0 := sorry

/--
Statement of Theorem 1.17(iii) (Maximal ergodic theorem):

There exists a constant `C ≥ 0` such that for any `f ∈ Lᵖ₁(X)` and `g ∈ Lᵖ₂(X)`,
`‖A T (N : ℕ+) X P f g‖_{Lᵖ(X;ℓ∞)} ≤ C ‖f‖_{Lᵖ₁(X)} ‖g‖_{Lᵖ₂(X)}`.
-/
theorem declaration uses `sorry`theorem_1_17_iii {f g : 𝓧 → ℂ} (hf : MemLp f p₁ μ) (hg : MemLp g p₂ μ) :
    eLpNorm (fun x ↦ ⨆ (N : ℕ+), ‖A T N (X : ℤ[X]) P f g x‖ₑ) p μ ≤
      Cᵢᵢᵢ P p₁ p₂ * ‖hf.toLp‖ₑ * ‖hg.toLp‖ₑ := by𝓧:Type u_1σX:MeasurableSpace 𝓧μ:Measure 𝓧inst✝:SigmaFinite μT:𝓧 ≃ᵐ 𝓧hT:MeasurePreserving (⇑T) μ μP:ℤ[X]hP:P.degree ≥ 2p₁:ℝ≥0∞p₂:ℝ≥0∞p:ℝ≥0∞h₁p₁:1 < p₁h₁p₂:1 < p₂h₂p₁:p₁ < ∞h₂p₂:p₂ < ∞hp₁p₂p:p₁⁻¹ + p₂⁻¹ = p⁻¹hp:p⁻¹ ≤ 1f:𝓧 → ℂg:𝓧 → ℂhf:MemLp f p₁ μhg:MemLp g p₂ μ⊢ eLpNorm (fun x => ⨆ N, ‖A T (↑↑N) X P f g x‖ₑ) p μ ≤ ↑(Cᵢᵢᵢ P p₁ p₂) * ‖MemLp.toLp f hf‖ₑ * ‖MemLp.toLp g hg‖ₑ
  sorryAll goals completed! 🐙

/-- The constant of Theorem 1.17 (iv). -/
noncomputable def declaration uses `sorry`Cᵢᵥ (P : ℤ[X]) (p₁ p₂ : ℝ≥0∞) (r Λ : ℝ≥0) : ℝ≥0 := sorry

/--
Statement of Theorem 1.17(iv) (Long variational ergodic theorem):

For any `r > 2` and `Λ > 1`, there exists a constant `C ≥ 0` such that for any `f ∈ Lᵖ₁(X)`,
`g ∈ Lᵖ₂(X)` and `Λ`-lacunary sequence `a` such that `1 ≤ a n` for all `n ∈ ℕ`,
`‖A T (a n) X P f g‖_{Lᵖ(X;Vʳ)} ≤ C ‖f‖_{Lᵖ₁(X)} ‖g‖_{Lᵖ₂(X)}`.
-/
theorem declaration uses `sorry`theorem_1_17_iv (r Λ : ℝ≥0) (hr : r > 2) (hΛ : Λ > 1) {f g : 𝓧 → ℂ}
    (hf : MemLp f p₁ μ) (hg : MemLp g p₂ μ) (a : ℕ → ℝ≥0) (ha : Lacunary Λ a) (ha' : ∀ n, 1 ≤ a n) :
    eLpNorm (fun x ↦ variationalNorm r fun n ↦ A T (a n) X P f g x) p μ ≤
      Cᵢᵥ P p₁ p₂ r Λ * ‖hf.toLp‖ₑ * ‖hg.toLp‖ₑ := by𝓧:Type u_1σX:MeasurableSpace 𝓧μ:Measure 𝓧inst✝:SigmaFinite μT:𝓧 ≃ᵐ 𝓧hT:MeasurePreserving (⇑T) μ μP:ℤ[X]hP:P.degree ≥ 2p₁:ℝ≥0∞p₂:ℝ≥0∞p:ℝ≥0∞h₁p₁:1 < p₁h₁p₂:1 < p₂h₂p₁:p₁ < ∞h₂p₂:p₂ < ∞hp₁p₂p:p₁⁻¹ + p₂⁻¹ = p⁻¹hp:p⁻¹ ≤ 1r:ℝ≥0Λ:ℝ≥0hr:r > 2hΛ:Λ > 1f:𝓧 → ℂg:𝓧 → ℂhf:MemLp f p₁ μhg:MemLp g p₂ μa:ℕ → ℝ≥0ha:Lacunary Λ aha':∀ (n : ℕ), 1 ≤ a n⊢ eLpNorm (fun x => variationalNorm r fun n => A T (a n) X P f g x) p μ ≤
  ↑(Cᵢᵥ P p₁ p₂ r Λ) * ‖MemLp.toLp f hf‖ₑ * ‖MemLp.toLp g hg‖ₑ
  sorryAll goals completed! 🐙