Almost everywhere convergence

TheoremUnbounded multipliers preserving almost-everywhere convergence to zero#●ready to prove

Let \((f_n)_{n \in \mathbb{N}}\) be a sequence of Borel measurable functions \(f_n : \mathbb{R} \to \mathbb{R}\) such that \(f_n(x) \to 0\) for almost every \(x \in [0, 1]\). Then there is a sequence of real numbers \((c_n)_{n \in \mathbb{N}}\) with \(|c_n| \to \infty\) such that \(c_n f_n(x) \to 0\) for almost every \(x \in [0, 1]\).

public theorem_wanted exists_tendsto_abs_atTop_and_ae_tendsto_mul_zero (f : ℕ → ℝ → ℝ)
    (hf_meas : ∀ n, Measurable (f n))
    (hf_ae : ∀ᵐ x ∂(volume.restrict (Set.Icc (0 : ℝ) 1)),
      Filter.Tendsto (fun n => f n x) Filter.atTop (nhds 0)) :
    ∃ c : ℕ → ℝ,
      Filter.Tendsto (fun n => |c n|) Filter.atTop Filter.atTop ∧
      (∀ᵐ x ∂(volume.restrict (Set.Icc (0 : ℝ) 1)),
        Filter.Tendsto (fun n => c n * f n x) Filter.atTop (nhds 0))

Sources

• MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level II (Measure and integration; Classical measure theory), problem ma_proofbench_l2_38.

TheoremDecay of dilates of an integrable function#●ready to prove

Let \(f : \mathbb{R} \to \mathbb{R}\) be Lebesgue integrable and let \(\lambda > 0\). Then for almost every \(x \in \mathbb{R}\), \(n^{-\lambda} f(nx) \to 0\) as \(n \to \infty\) through the positive integers.

public theorem_wanted ae_tendsto_rpow_neg_mul_comp_mul_zero
  (f : ℝ → ℝ)
  (hf : MeasureTheory.MemLp f 1 MeasureTheory.volume)
  (lam : ℝ)
  (hlam : 0 < lam) :
  ∀ᵐ x ∂MeasureTheory.volume,
    Filter.Tendsto (fun n : ℕ => (n + 1 : ℝ) ^ (-lam) * f ((n + 1) * x))
      Filter.atTop (nhds 0)

Sources

• MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level II (Measure and integration; Classical measure theory), problem ma_proofbench_l2_37.

2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.