How to prove this integral is integrableOn?

Stream: new members

[Junqi Liu]

import Mathlib

example (n : ℕ): MeasureTheory.IntegrableOn
    (fun (xyz : ℝ × ℝ × ℝ) ↦
      1 / ((1 - (1 - xyz.2.2) * xyz.1) * (1 - xyz.2.1 * xyz.2.2)))
    (Set.Ioo 0 1 ×ˢ Set.Ioo 0 1 ×ˢ Set.Ioo 0 1)
    (MeasureTheory.volume.prod (MeasureTheory.volume.prod MeasureTheory.volume)) := by
  sorry

[Junqi Liu]

I have proved it is AEStronglyMeasurable, but I don't know how to prove it is finite because it has singular point. For math proof, its value can be calculated by DCT.

[Bjørn Kjos-Hanssen]

You can set up DCT like this:

import Mathlib.MeasureTheory.Integral.Lebesgue
import Mathlib.MeasureTheory.MeasurableSpace.Defs
import Mathlib

example (n : ℕ): MeasureTheory.IntegrableOn
    (fun ((x,y,z) : ℝ × ℝ × ℝ) ↦
      1 / ((1 - (1 - z) * x) * (1 - y * z)))
    (Set.Ioo 0 1 ×ˢ Set.Ioo 0 1 ×ˢ Set.Ioo 0 1)
    (MeasureTheory.volume.prod (MeasureTheory.volume.prod MeasureTheory.volume)) := by
  have Q := @MeasureTheory.tendsto_lintegral_of_dominated_convergence ℝ Real.measurableSpace MeasureTheory.volume
  sorry

[Bjørn Kjos-Hanssen]

Then if you inspect Q you can provide the dominating function, whatever it is...

[Junqi Liu]

Is there characteristic function in Mathlib4? The function sequence which I want is that $\chi_{(\frac{1}{n},1- \frac{1}{n})}$ (fun _ => _)

[Bjørn Kjos-Hanssen]

docs#Set.indicator

[Junqi Liu]

thanks! I'll have a try