theorem
Verification.lintegral_cross_le
{f g : ↑unitInterval → ENNReal}
(hf : Measurable f)
(hg : Measurable g)
(μ ν : MeasureTheory.Measure ↑unitInterval)
(h : ∀ᵐ (x : ↑unitInterval) ∂μ, ∀ᵐ (y : ↑unitInterval) ∂ν, f x * g y ≤ g x * f y)
:
(∫⁻ (x : ↑unitInterval), f x ∂μ) * ∫⁻ (y : ↑unitInterval), g y ∂ν ≤ (∫⁻ (x : ↑unitInterval), g x ∂μ) * ∫⁻ (y : ↑unitInterval), f y ∂ν
Integrating a pointwise cross-product inequality preserves its determinant sign.
theorem
Verification.tp2_rectangle_integrals
(f : ↑unitInterval → ↑unitInterval → ENNReal)
(hf : Measurable fun (p : ↑unitInterval × ↑unitInterval) => f p.1 p.2)
(S T U V : Set ↑unitInterval)
(hS : MeasurableSet S)
(hT : MeasurableSet T)
(hU : MeasurableSet U)
(hV : MeasurableSet V)
(h : ∀ a ∈ S, ∀ b ∈ T, ∀ u ∈ U, ∀ v ∈ V, f b u * f a v ≤ f a u * f b v)
:
(∫⁻ (a : ↑unitInterval) in S, ∫⁻ (v : ↑unitInterval) in V, f a v) * ∫⁻ (b : ↑unitInterval) in T, ∫⁻ (u : ↑unitInterval) in U, f b u ≤ (∫⁻ (a : ↑unitInterval) in S, ∫⁻ (u : ↑unitInterval) in U, f a u) * ∫⁻ (b : ↑unitInterval) in T, ∫⁻ (v : ↑unitInterval) in V, f b v
Integration over ordered rectangles preserves TP2, without section-integrability assumptions.