Integrability of powers of norm

Stream: Is there code for X?

[Moritz Doll]

Hi, do we have anything along the line of $\int_{\mathbb{R}^d} (1 + |x|)^{-s} dx < \infty$ for $s > d$ phrased of course in terms of integrable?

[Sebastien Gouezel]

I don't think we have it (not even the one-dimensional version).

[Kalle Kytölä]

From the one-dimensional case, I believe the easiest and most generalizable way to the $d$-dimensional case might be using layer cake formula docs#measure_theory.lintegral_eq_lintegral_meas_le : one should only need something like $\mu[B_r(0)] \sim r^d$ in $\R^d$ then, since for $f(x) = (1+\|x\|)^{-s}$, the preimages $f^{-1}[t,\infty)$ are balls. Unfortunately we don't have all the API I'd like about layer cakes, so it might be a little less convenient to use now than it should. (I intend to add some API once I get to think about some design choices in related things.)

Of course we also have change of variables formula by Sébastien, which allows to reduce to one-dimensional case. But I think it might be less direct and is moreover only convenient for strictly radial functions, whereas layer cake should be a good approach for not-exactly-radial variants, too.

In any case, I will be happy to see this result is in mathlib!

[Patrick Massot]

In any case it would certainly be very welcome news about concrete usability of integration to have this result.

[Moritz Doll]

I still have some other things to finish, but I hope I will get some time to work on the one-dimensional case soon.

[Moritz Doll]

Since the 1-dim case was essentially done by Bhavik, I wrote some stuff for the n-dim case. Is the measure of normed balls somewhere in mathlib already? I did not find it, but I think it should be somewhere in the Hausdorff measure stuff.

[Sebastien Gouezel]

The measure of balls is in docs#measure_theory.measure.add_haar_ball and lemmas around it.

[Moritz Doll]

perfect. thanks

[Moritz Doll]

Ok, I have only one crucial part missing and this is the following lemma, which I think should be correct and probably in mathlib (?), but library_search could not find it

lemma integrable_on.lintegral_lt_top {f : ℝ → ℝ} {s : set ℝ}
  (hf : integrable_on f s) (hf' : ∀ (x : ℝ) (hx : x ∈ s), 0 ≤ f x) :
  ∫⁻ (x : ℝ) in s, ennreal.of_real (f x) < ⊤ := sorry

[Kalle Kytölä]

I couldn't find it directly either!

I think the following are helpful:

• stating for general measures (not just volume on reals)
• assuming nonnegativity only a.e.
• getting the case of restriction to a set and integrable_on from a corresponding integrable on a whole space.

I thought I'd find it, but ended up just writing a terrible reduction to yet another ennreal coercion lemma that I didn't get automatically... If no direct proof is found, maybe this can nevertheless be of help to someone interested in golfing?

import measure_theory.integral.integrable_on
import measure_theory.measure.haar_lebesgue

open_locale ennreal

open measure_theory

lemma why_cant_I_find_this {x : ℝ} (x_nn : 0 ≤ x) :
  ennreal.of_real x = real.to_nnreal x :=
sorry

lemma integrable.lintegral_lt_top_of_nn {X : Type*} [measurable_space X]
  (μ : measure X) {f : X → ℝ}
  (hf : integrable f μ) (hf' : ∀ x, 0 ≤ f x) :
  ∫⁻ x, ennreal.of_real (f x) ∂μ < ⊤ :=
begin
  convert hf.2,
  funext x,
  rw [why_cant_I_find_this (hf' x), ← nnreal.nnnorm_eq (f x).to_nnreal],
  simp only [hf' x, real.coe_to_nnreal', max_eq_left],
end

lemma integrable.lintegral_lt_top {X : Type*} [measurable_space X]
  (μ : measure X) {f : X → ℝ}
  (hf : integrable f μ) (hf' : ∀ᵐ x ∂μ, 0 ≤ f x) :
  ∫⁻ x, ennreal.of_real (f x) ∂μ < ⊤ :=
begin
  set g := λ x, max (f x) 0 with def_g,
  have g_nn : ∀ x, 0 ≤ g x, from λ x, by simp only [le_max_iff, le_refl, or_true],
  have f_eq_g : f =ᵐ[μ] g,
  { filter_upwards [hf'] with x fx_nn,
    simp only [def_g, fx_nn, max_eq_left], },
  rw lintegral_congr_ae (filter.eventually_eq.fun_comp f_eq_g ennreal.of_real),
  exact integrable.lintegral_lt_top_of_nn μ (integrable.congr hf f_eq_g) g_nn,
end

lemma integrable_on.lintegral_lt_top_general {X : Type*} [measurable_space X]
  (μ : measure X) {s : set X} {f : X → ℝ}
  (hf : integrable_on f s μ) (hf' : ∀ᵐ x ∂(μ.restrict s), 0 ≤ f x) :
  ∫⁻ x in s, ennreal.of_real (f x) ∂μ < ⊤ :=
integrable.lintegral_lt_top (μ.restrict s) hf hf'

lemma integrable_on.lintegral_lt_top' {f : ℝ → ℝ} {s : set ℝ}
  (s_mble : measurable_set s)
  (hf : integrable_on f s) (hf' : ∀ᵐ x ∂volume.restrict s, 0 ≤ f x) :
  ∫⁻ (x : ℝ) in s, ennreal.of_real (f x) < ⊤ :=
integrable_on.lintegral_lt_top_general _ hf hf'

[Rémy Degenne]

Your lemma is not far from the integrability condition: it suffices to replace the function with its norm, which can be done since it's nonnegative. Here are two lemmas which are each not quite the one you asked for. The first one replaces the nonnegativity condition by 0 ≤ᵐ[μ.restrict s] f, which may not be a consequence of ∀ x, x ∈ s → 0 ≤ f x if the set is not measurable. The second one assumes that the set is measurable but otherwise uses your hypotheses (or weaker).

lemma integrable_on.lintegral_lt_top' {f : ℝ → ℝ} {s : set ℝ} {μ : measure ℝ}
  (hf : integrable_on f s μ) (h_nonneg : 0 ≤ᵐ[μ.restrict s] f) :
  ∫⁻ x in s, ennreal.of_real (f x) ∂μ < ⊤ :=
begin
  suffices : ∫⁻ x in s, ennreal.of_real (f x) ∂μ = ∫⁻ x in s, ↑∥f x∥₊ ∂μ,
  { rw this,
    exact hf.2, },
  refine lintegral_congr_ae _,
  filter_upwards [h_nonneg] with x hx,
  rw [← of_real_norm_eq_coe_nnnorm, real.norm_of_nonneg hx],
end

lemma integrable_on.lintegral_lt_top {f : ℝ → ℝ} {s : set ℝ} {μ : measure ℝ}
  (hf : integrable_on f s μ) (hf' : ∀ᵐ x ∂μ, x ∈ s → 0 ≤ f x) (hs : measurable_set s) :
  ∫⁻ x in s, ennreal.of_real (f x) ∂μ < ⊤ :=
begin
  suffices : ∫⁻ x in s, ennreal.of_real (f x) ∂μ = ∫⁻ x in s, ↑∥f x∥₊ ∂μ,
  { rw this,
    exact hf.2, },
  refine lintegral_congr_ae _,
  have h_nonneg : 0 ≤ᵐ[μ.restrict s] f,
  { rwa [filter.eventually_le, ae_restrict_iff' hs], },
  filter_upwards [h_nonneg] with x hx,
  rw [← of_real_norm_eq_coe_nnnorm, real.norm_of_nonneg hx],
end

[Sebastien Gouezel]

In fact you don't need the set s to be measurable:

import measure_theory.integral.set_integral

open measure_theory

lemma integrable_on.lintegral_lt_top' {f : ℝ → ℝ} {s : set ℝ} {μ : measure ℝ}
  (hf : integrable_on f s μ) (h_nonneg : 0 ≤ᵐ[μ.restrict s] f) :
  ∫⁻ x in s, ennreal.of_real (f x) ∂μ < ⊤ :=
begin
  suffices : ∫⁻ x in s, ennreal.of_real (f x) ∂μ = ∫⁻ x in s, ↑∥f x∥₊ ∂μ,
  { rw this,
    exact hf.2, },
  refine lintegral_congr_ae _,
  filter_upwards [h_nonneg] with x hx,
  rw [← of_real_norm_eq_coe_nnnorm, real.norm_of_nonneg hx],
end

lemma integrable_on.lintegral_lt_top {f : ℝ → ℝ} {s : set ℝ} {μ : measure ℝ}
  (hf : integrable_on f s μ) (hf' : ∀ᵐ x ∂μ, x ∈ s → 0 ≤ f x) :
  ∫⁻ x in s, ennreal.of_real (f x) ∂μ < ⊤ :=
begin
  let g := hf.1.mk _,
  have : ∫⁻ x in s, ennreal.of_real (f x) ∂μ = ∫⁻ x in s, ennreal.of_real (g x) ∂μ,
  { apply lintegral_congr_ae,
    filter_upwards [hf.1.ae_eq_mk] with x hx,
    rw hx },
  rw this,
  apply integrable_on.lintegral_lt_top' (hf.congr hf.1.ae_eq_mk),
  apply (ae_restrict_iff (measurable_set_le measurable_zero (hf.1.measurable_mk))).2,
  filter_upwards [hf', ae_imp_of_ae_restrict hf.1.ae_eq_mk] with x hx h'x,
  assume xs,
  rw ← h'x xs,
  exact hx xs,
end

[Moritz Doll]

thanks so much everyone. @Sebastien Gouezel do you want to PR that yourself or should I do it? How do you feel about including the version with ∀ x : ℝ, x ∈ s → 0 ≤ f x? Some lemmas in the integration library have both lemmas and some do not and I don't know which is preferred.

[Moritz Doll]

after all it is just a matter of applying ae_of_all, but on the other hand it makes the code in the applications a bit nicer

[Moritz Doll]

and with that the integrability of (1+||x||)^-(n+ε) is sorry-free, but it is still a huge mess. literally all lemmas have foo in the name, I now have to think of a good name for the integrant, probably one_add_rpow or something

[Sebastien Gouezel]

I would definitely include the one with ∀ x : ℝ, x ∈ s → 0 ≤ f x, because in most applications I guess it will be the easiest to apply. I'll let you PR it, because you can adapt it exactly to your needs.