Integral with two variables

Stream: mathlib4

[Jihoon Hyun]

I believe this is not common, but how can I solve an integral with two variables? Specifically:

import Mathlib

example {f : (ℝ × ℝ) → ℝ} :
    ∫ (x : ℝ) (y : ℝ), f (x, y) = ∫ z, f z := by
  sorry

[Rémy Degenne]

import Mathlib
open MeasureTheory

example {f : (ℝ × ℝ) → ℝ} (hf : Integrable f) :
    ∫ (x : ℝ) (y : ℝ), f (x, y) = ∫ z, f z := by
  rw [Measure.volume_eq_prod, integral_prod _ hf]

I added an integrability hypothesis for f.
To write the proof, I knew I wanted to rewrite the integral over a product space, so something like integral_prod. That lemma did not work directly because the volume over the product is not written as a product of volumes, so I found Measure.volume_eq_prod to rewrite it in that form.
It's a bit tricky because the volume measures that I am rewriting are invisible in the integrals.

[Rémy Degenne]

I don't think we have a specialized lemma like integral_prod for the case of volume.

[Jihoon Hyun]

But I believe the equality holds even without the assumption Integrable f. Can you somehow remove that assumption, or is that necessary?

[Rémy Degenne]

Without the integrability hypothesis the right hand side is zero by definition of our integral. Can we find a function such that the left hand side is non-zero, because it's integrable in one coordinate for some values of the other coordinate?

[Jihoon Hyun]

I don't think so. If f is not integrable, then won't both sides be zero?

[Rémy Degenne]

Take f (x, y) equal to 1 if x < 0 or x > 1 and to some nonnegative g y otherwise, with ∫ y, g y = 1. Then for a given x, the integral ∫ y, f (x, y) is 0 outside of [0,1] because it's not integrable, and 1 inside of [0,1]. So it's the indicator of [0,1]. We then integrate over x and get 1.

[Jihoon Hyun]

I don't understand. Is ∫ (x : ℝ) (y : ℝ) equivalent to ∫ (x : ℝ), ∫ (y : ℝ)?

[Rémy Degenne]

yes it is

[Jihoon Hyun]

Oh.

[Rémy Degenne]

import Mathlib

example {f : (ℝ × ℝ) → ℝ} :
    ∫ (x : ℝ) (y : ℝ), f (x, y) = ∫ (x : ℝ), ∫ (y : ℝ), f (x, y)  := rfl

[Jihoon Hyun]

Thanks a lot. I hope I knew that earlier..

[Rémy Degenne]

(that's the first thing I checked in your example, because I actually did not know that we could write it with only one integral sign).