measure_theory.integrable uncurry f

Stream: Is there code for X?

[rtertr (Sonia)]

Hello, I am trying to use the theorem measure_theory.integral_integral_swap .
My function is (f : ℝ → ℝ → ℂ). I have to prove measure_theory.integrable (function.uncurry f) (measure_theory.measure_space.volume.prod measure_theory.measure_space.volume).
What conditions should I put on f and what relevant theorems are there to transform this statement? :)
Kind regards,

[Moritz Doll]

this is really hard to answer without any information about f. The question you should answer first is 'what is the pen&paper proof?'. nevertheless I would think that docs#measure_theory.integrable_prod_iff or the primed version could be helpful

[rtertr (Sonia)]

Okay, thank you! I will try! I think the function might just be infinitely continuously differentiable :)

[rtertr (Sonia)]

Hello again,
Was able to prove most things I wanted, but I need to prove continuous (function.uncurry f) , and I was wondering if there could be a version of continuous_uncurry_of_discrete_topology where α does not have to a discrete_topology? :)
Kind regarrds,

[Moritz Doll]

there is docs#continuous_map.continuous_uncurry_of_continuous