Integration of symmetric functions over the two triangles of the unit square #
theorem
Verification.integral_symmetric_triangle_of_integrable
(f : ↑unitInterval × ↑unitInterval → ℝ)
(hi : MeasureTheory.Integrable f MeasureTheory.volume)
(hs : ∀ (p : ↑unitInterval × ↑unitInterval), f p.swap = f p)
:
∫ (u : ↑unitInterval) (v : ↑unitInterval), f (u, v) = 2 * ∫ (u : ↑unitInterval), ∫ (v : ↑unitInterval) in Set.Iic u, f (u, v)
theorem
Verification.integral_symmetric_triangle
(f : ↑unitInterval × ↑unitInterval → ℝ)
(hf : Measurable f)
(hb : ∀ (p : ↑unitInterval × ↑unitInterval), f p ∈ Set.Icc 0 1)
(hs : ∀ (p : ↑unitInterval × ↑unitInterval), f p.swap = f p)
:
∫ (u : ↑unitInterval) (v : ↑unitInterval), f (u, v) = 2 * ∫ (u : ↑unitInterval), ∫ (v : ↑unitInterval) in Set.Iic u, f (u, v)