← Mathematical handbook

Fubini for lower orthants of the bivariate unit cube

theorem Verification.integral_cube_Iic_iterated {f : (Fin 2 → ↑unitInterval) → ℝ} (hf : MeasureTheory.Integrable f MeasureTheory.volume) (u v : ↑unitInterval) : ∫ (x : Fin (Nat.succ 0).succ → ↑unitInterval) in Set.Iic ![u, v], f x = ∫ (s : ↑unitInterval) in Set.Iic u, ∫ (t : ↑unitInterval) in Set.Iic v, f ![s, t]

theorem Verification.integral_cube_Ioc_two_real (F : ℝ → ℝ → ℝ) (a b c d : ↑unitInterval) (hab : a ≤ b) (hcd : c ≤ d) (hF : MeasureTheory.IntegrableOn (fun (x : Fin 2 → ↑unitInterval) => F ↑(x 0) ↑(x 1)) (Set.univ.pi fun (i : Fin 2) => Set.Ioc (![a, c] i) (![b, d] i)) MeasureTheory.volume) : ∫ (x : Fin 2 → ↑unitInterval) in Set.univ.pi fun (i : Fin 2) => Set.Ioc (![a, c] i) (![b, d] i), F ↑(x 0) ↑(x 1) = ∫ (u : ℝ) in ↑a..↑b, ∫ (v : ℝ) in ↑c..↑d, F u v