BoundedMoments.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.LittlewoodFiniteFlatness.bounded_rpow_threshold line 14

Source documentation

A threshold estimate, including exponents strictly between zero and one.

lemma bounded_rpow_threshold {x δ p : ℝ} {k : ℕ}
    (hx : 0 ≤ x) (hx1 : x ≤ 1) (hδ : 0 < δ) (hp : 0 < p) :
    x ^ p ≤ δ ^ p + x ^ k / δ ^ k := by
…

theorem OAI.LittlewoodFiniteFlatness.tendsto_integral_rpow_of_bounded_moment line 29

Source documentation

Bounded measurable functions: convergence of any positive integer moment implies convergence of every positive real moment. No pointwise convergence is assumed.

theorem tendsto_integral_rpow_of_bounded_moment
    {α : Type*} [MeasurableSpace α] (μ : Measure α) [IsProbabilityMeasure μ]
    (g : ℕ → α → ℝ) (hg : ∀ n, Measurable (g n))
    (hb : ∀ᶠ n in atTop, ∀ x, 0 ≤ g n x ∧ g n x ≤ 1)
    (k : ℕ) (_hk : 0 < k)
    (hmoment : Tendsto (fun n => ∫ x, g n x ^ k ∂μ) atTop (𝓝 0))
    (p : ℝ) (hp : 0 < p) :
    Tendsto (fun n => ∫ x, g n x ^ p ∂μ) atTop (𝓝 0) := by
…

theorem OAI.LittlewoodFiniteFlatness.tendsto_integral_abs_sub_one_rpow line 75

Source documentation

The interface used by the normalized Littlewood family.

theorem tendsto_integral_abs_sub_one_rpow
    {α : Type*} [MeasurableSpace α] (μ : Measure α) [IsProbabilityMeasure μ]
    (f : ℕ → α → ℝ) (hf : ∀ n, Measurable (f n))
    (h0 : ∀ n x, 0 ≤ f n x)
    (h2 : ∀ᶠ n in atTop, ∀ x, f n x ≤ 2)
    (hmoment : Tendsto (fun n => ∫ x, (f n x - 1) ^ (2 : ℕ) ∂μ) atTop (𝓝 0))
    (p : ℝ) (hp : 0 < p) :
    Tendsto (fun n => ∫ x, |f n x - 1| ^ p ∂μ) atTop (𝓝 0) := by
…

theorem OAI.LittlewoodFiniteFlatness.tendsto_integral_abs_sub_one_rpow_of_fourth line 91

Source documentation

Fourth-moment variant with exactly the same boundedness hypotheses.

theorem tendsto_integral_abs_sub_one_rpow_of_fourth
    {α : Type*} [MeasurableSpace α] (μ : Measure α) [IsProbabilityMeasure μ]
    (f : ℕ → α → ℝ) (hf : ∀ n, Measurable (f n))
    (h0 : ∀ n x, 0 ≤ f n x)
    (h2 : ∀ᶠ n in atTop, ∀ x, f n x ≤ 2)
    (hmoment : Tendsto (fun n => ∫ x, (f n x - 1) ^ (4 : ℕ) ∂μ) atTop (𝓝 0))
    (p : ℝ) (hp : 0 < p) :
    Tendsto (fun n => ∫ x, |f n x - 1| ^ p ∂μ) atTop (𝓝 0) := by
…