theorem
Verification.continuousAt_nonneg_of_ae_imp
{X : Type u_1}
[TopologicalSpace X]
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
[μ.IsOpenPosMeasure]
{f : X → ℝ}
{x : X}
{s : Set X}
(hf : ContinuousAt f x)
(hs : s ∈ nhds x)
(ha : ∀ᵐ (y : X) ∂μ, y ∈ s → 0 ≤ f y)
:
theorem
Verification.continuous_density_minor_of_ae
(f : ↑unitInterval × ↑unitInterval → ℝ)
(hf : Measurable f)
(ha : HasAEOrderedMinors 1 fun (u v : ↑unitInterval) => f (u, v))
(a b c d : ↑unitInterval)
(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.copula_continuous_density_minor
{C : ProbabilityTheory.Copula 2}
(hC : C.HasMTP2Density)
(f : (Fin 2 → ↑unitInterval) → ℝ)
(hf : Measurable f)
(hn : ∀ (x : Fin 2 → ↑unitInterval), 0 ≤ f x)
(hd : C.toMeasure = MeasureTheory.volume.withDensity fun (x : Fin 2 → ↑unitInterval) => ENNReal.ofReal (f x))
(a b c d : ↑unitInterval)
(hab : a < b)
(hcd : c < d)
(hac : ContinuousAt (fun (p : ↑unitInterval × ↑unitInterval) => f ![p.1, p.2]) (a, c))
(had : ContinuousAt (fun (p : ↑unitInterval × ↑unitInterval) => f ![p.1, p.2]) (a, d))
(hbc : ContinuousAt (fun (p : ↑unitInterval × ↑unitInterval) => f ![p.1, p.2]) (b, c))
(hbd : ContinuousAt (fun (p : ↑unitInterval × ↑unitInterval) => f ![p.1, p.2]) (b, d))
:
A continuous representative of a density inherits the ordered minors of any TP2 density of the same copula, at every strict rectangle of continuity.