How to prove a multiple integral is Integrable?

Stream: Is there code for X?

[Junqi Liu]

like

example : IntervalIntegrable
    (fun x ↦ ∫ (y : ℝ) (z : ℝ) in (0)..1, 1 / (1 - x * y * z)) MeasureTheory.volume 0 1 := by sorry

where $x$ can't be separated from the multiple integral.
note: we assume this multiple integral must be integrable, maybe it is not $\int_0^1 \int_0^1 \int_0^1 \frac{1}{1 - x * y * z}dx dy dz$.

[Yury G. Kudryashov]

Do you have an informal proof?

[Eric Wieser]

This statement looks risky to me; if the inner integral is not integrable, then mathlib defines it as zero and so the outer one ends up integrable anyway!

[Yury G. Kudryashov]

The inner integral is well defined for all $0 \le x < 1$, because the function is continuous on $[0, 1]\times [0, 1]$ in this case.

[Eric Wieser]

Right, in this case it's (presumably) true, but the statement is much weaker than the one that was intended.

[Junqi Liu]

:sob: My informal proof is that the triple integral is finite. But I don't know how to formal this proof.

[Junqi Liu]

Eric Wieser said:

This statement looks risky to me; if the inner integral is not integrable, then mathlib defines it as zero and so the outer one ends up integrable anyway!

yes! Actually I want to proof this MultiIntegral is positive. But if I want to use the lemma intervalIntegral.intervalIntegral_pos_of_pos_on. Then I need to show the Integral and MultiIntegral is Integrable.

[Yury G. Kudryashov]

Can you just compute the integral?

[Junqi Liu]

emmmmm. I can only compute a upper bound in informal space.

[Yury G. Kudryashov]

You can use docs#IntervalIntegrable.mono_fun'

[Junqi Liu]

ok! thanks~ let me have a try