lintegral_coe_eq_coe_integral

Stream: Is there code for X?

[Kalle Kytölä]

We have docs#measure_theory.lintegral_coe_eq_integral:

lemma lintegral_coe_eq_integral (f : α → ℝ≥0) (hfi : integrable (λ x, (f x : ℝ)) μ) :
  ∫⁻ a, f a ∂μ = ennreal.of_real ∫ a, f a ∂μ := sorry

I don't find the following variant (real-valued functions assumed to be nonnegative instead of nnreal-valued functions), which I nevertheless end up needing often:

lemma lintegral_coe_eq_coe_integral {f : α → ℝ} (hfi : integrable f μ) (f_nn : 0 ≤ f) :
  ∫⁻ x, ennreal.of_real (f x) ∂μ = ennreal.of_real (∫ x, f x ∂μ) := sorry

Does it exist and do others agree it is worth having as a rewrite lemma?

[Yaël Dillies]

Just noting that you call itcoe but the function is named of_real.

[Kalle Kytölä]

Given docs#lintegral_coe_eq_integral, the essence of the proof is just coercions between reals, nnreal, and ennreals. I did not find a much shorter proof than the following, so consider this also an invitation to golfers:

import measure_theory.integral.bochner

open measure_theory
open_locale nnreal ennreal

variables {α : Type*} [measurable_space α] {μ : measure α}

lemma coe_comp_to_nnreal_comp {f : α → ℝ} (f_nn : 0 ≤ f) :
  (coe : ℝ≥0 → ℝ) ∘ real.to_nnreal ∘ f = f :=
by { ext x, exact real.coe_to_nnreal _ (f_nn x), }

lemma ennreal_coe_comp_to_nnreal_comp {f : α → ℝ} (f_nn : 0 ≤ f) :
  (coe : ℝ≥0 → ℝ≥0∞) ∘ real.to_nnreal ∘ f = ennreal.of_real ∘ f :=
begin
  funext x,
  simp only [ennreal.of_real_eq_coe_nnreal (f_nn x), function.comp_app, ennreal.coe_eq_coe],
  apply subtype.coe_injective,
  exact max_eq_left_iff.mpr (f_nn x),
end

lemma lintegral_coe_eq_coe_integral {f : α → ℝ} (hfi : integrable f μ) (f_nn : 0 ≤ f) :
  ∫⁻ x, ennreal.of_real (f x) ∂μ = ennreal.of_real (∫ x, f x ∂μ) :=
begin
  set g := real.to_nnreal ∘ f with def_g,
  have coe_g : (λ x, (g x : ℝ)) = f, from coe_comp_to_nnreal_comp f_nn,
  have of_real_g : (λ x, (g x : ℝ≥0∞)) = (λ x, ennreal.of_real (f x)),
  from ennreal_coe_comp_to_nnreal_comp f_nn,
  have g_intble : integrable (λ x, (g x : ℝ)) μ, by rwa ←coe_g at hfi,
  rw [←coe_g, ←lintegral_coe_eq_integral g g_intble, of_real_g, coe_g],
end

[Yaël Dillies]

With this, you might be able to golf docs#measure_theory.of_real_integral_norm_eq_lintegral_nnnorm

[Kalle Kytölä]

Yaël Dillies said:

Just noting that you call itcoe but the function is named of_real.

True, the naming could be improved --- I mainly wanted to emphasize the analogy to the existing named lemma.

[Kalle Kytölä]

Yaël Dillies said:

With this, you might be able to golf docs#measure_theory.of_real_integral_norm_eq_lintegral_nnnorm

nnnorm still lands in nnreal, whereas I want real values.

[Kalle Kytölä]

#13701

I hope others agree this is a rewrite lemma worth having; I plan to soon use it in two separate PRs. Following Yaël's remark, I changed the naming. I also switched the two sides of the equality, because at least in my opinion the new RHS (old LHS) is simpler, since it makes mathematical sense without integrability assumptions and lintegralnaturally yields ennreal anyway.

Golfing is still welcome! :wink: