theorem MathlibNt.Analysis.integral_indicator_moving_Ioc_section (s : Set ℝ) (l r : ℝ → ℝ) (f : ℝ × ℝ → ℝ) (u : ℝ) : ∫ (v : ℝ), {x : ℝ × ℝ | x.1 ∈ s ∧ x.2 ∈ Set.Ioc (l x.1) (r x.1)}.indicator f (u, v) = s.indicator (fun (u : ℝ) => ∫ (v : ℝ) in Set.Ioc (l u) (r u), f (u, v)) u

Integrating a section of a moving half-open interval region retains the outer indicator, including empty and reversed inner intervals.

theorem MathlibNt.Analysis.setIntegral_moving_Ioc_eq_iterated (s : Set ℝ) (l r : ℝ → ℝ) (f : ℝ × ℝ → ℝ) (hs : MeasurableSet s) (hregion : MeasurableSet {x : ℝ × ℝ | x.1 ∈ s ∧ x.2 ∈ Set.Ioc (l x.1) (r x.1)}) (hf : MeasureTheory.IntegrableOn f {x : ℝ × ℝ | x.1 ∈ s ∧ x.2 ∈ Set.Ioc (l x.1) (r x.1)} MeasureTheory.volume) : ∫ (x : ℝ × ℝ) in {x : ℝ × ℝ | x.1 ∈ s ∧ x.2 ∈ Set.Ioc (l x.1) (r x.1)}, f x = ∫ (u : ℝ) in s, ∫ (v : ℝ) in Set.Ioc (l u) (r u), f (u, v)

Fubini for an integrable kernel on an actual moving half-open interval region. No continuity or ordering of the endpoint functions is assumed.