Lean: free joint measurability for kernels constant on dyadic cells, then Fubini

If a kernel K x y depends only on (index j x, index j y), where index j x : ι → ℤ is the dyadic cell index, then Measurable (Function.uncurry K) comes for free. Rewrite uncurry K as (fun p => K (corner p.1) (corner p.2)) ∘ fun p => (index j p.1, index j p.2), close with (measurable_of_countable _).comp ((hidx.comp measurable_fst).prodMk (hidx.comp measurable_snd)), and use the cell property to prove the funext. For Fubini on Q × Q, integral_integral_swap needs Integrable (uncurry f) ((μ.restrict Q).prod (μ.restrict Q)). Get the integrability from (integrable_const c).mul_prod hφ.integrableOn.norm with .mono', and the measurability of p ↦ φ p.2 from hφ.integrableOn.1.comp_snd (μ := volume.restrict Q). Gotcha: integrable_const on volume.restrict Q needs a local have : IsFiniteMeasure (volume.restrict Q) := ⟨by rw [Measure.restrict_apply_univ]; exact hQ.lt_top⟩.