theorem
Verification.real_continuous_density_minor_of_ae
(f : ℝ × ℝ → ℝ)
(hf : Measurable f)
(ha : ∀ᵐ (a : ℝ) (b : ℝ) (c : ℝ) (d : ℝ), a ≤ b → c ≤ d → 0 ≤ f (a, c) * f (b, d) - f (a, d) * f (b, c))
(a b c d : ℝ)
(hab : a < b)
(hcd : c < d)
(hac : ContinuousAt f (a, c))
(had : ContinuousAt f (a, d))
(hbc : ContinuousAt f (b, c))
(hbd : ContinuousAt f (b, d))
:
theorem
Verification.real_density_minor_of_tp2_ae
(f g : ℝ × ℝ → ℝ)
(hf : Measurable f)
(hg : Measurable g)
(he : f =ᵐ[MeasureTheory.volume] g)
(htp : ∀ (a b c d : ℝ), a ≤ b → c ≤ d → g (a, d) * g (b, c) ≤ g (a, c) * g (b, d))
(a b c d : ℝ)
(hab : a < b)
(hcd : c < d)
(hac : ContinuousAt f (a, c))
(had : ContinuousAt f (a, d))
(hbc : ContinuousAt f (b, c))
(hbd : ContinuousAt f (b, d))
: