← Mathematical handbook

Ordered density minors, with a null-set invariant convention

The sign +1 gives TP2 and -1 gives RR2. The four coordinates are quantified almost everywhere with respect to uniform measure, so changing a density on a null set cannot change this property.

def Verification.HasAEOrderedMinors (s : ℝ) (f : ↑unitInterval → ↑unitInterval → ℝ) : Prop

Equations

• Verification.HasAEOrderedMinors s f = ∀ᵐ (u₁ : ↑unitInterval) (u₂ : ↑unitInterval) (v₁ : ↑unitInterval) (v₂ : ↑unitInterval), u₁ ≤ u₂ → v₁ ≤ v₂ → 0 ≤ s * (f u₁ v₁ * f u₂ v₂ - f u₁ v₂ * f u₂ v₁)

theorem Verification.HasAEOrderedMinors.congr {s : ℝ} {f g : ↑unitInterval → ↑unitInterval → ℝ} (hf : HasAEOrderedMinors s f) (he : ∀ᵐ (u : ↑unitInterval) (v : ↑unitInterval), f u v = g u v) : HasAEOrderedMinors s g

theorem Verification.aeOrderedMinors_congr {s : ℝ} {f g : ↑unitInterval → ↑unitInterval → ℝ} (he : ∀ᵐ (u : ↑unitInterval) (v : ↑unitInterval), f u v = g u v) : HasAEOrderedMinors s f ↔ HasAEOrderedMinors s g

theorem Verification.exists_mem_Ioo_of_ae {a b : ↑unitInterval} (hab : a < b) {p : ↑unitInterval → Prop} (hp : ∀ᵐ (u : ↑unitInterval), p u) : ∃ u ∈ Set.Ioo a b, p u

theorem Verification.medianSign_antitone : Antitone medianSign

theorem Verification.stepDensity_minor (d : ↑unitInterval → ℝ) (u₁ u₂ v₁ v₂ : ↑unitInterval) : (1 + medianSign u₁ * d v₁) * (1 + medianSign u₂ * d v₂) - (1 + medianSign u₁ * d v₂) * (1 + medianSign u₂ * d v₁) = (medianSign u₁ - medianSign u₂) * (d v₁ - d v₂)

theorem Verification.stepDensity_ordered_minors {s : ℝ} {d : ↑unitInterval → ℝ} (hd : Antitone fun (v : ↑unitInterval) => s * d v) (u₁ u₂ v₁ v₂ : ↑unitInterval) (hu : u₁ ≤ u₂) (hv : v₁ ≤ v₂) : 0 ≤ s * ((1 + medianSign u₁ * d v₁) * (1 + medianSign u₂ * d v₂) - (1 + medianSign u₁ * d v₂) * (1 + medianSign u₂ * d v₁))

theorem Verification.stepDensity_ae_minors_iff (s : ℝ) (d : ↑unitInterval → ℝ) : (HasAEOrderedMinors s fun (u v : ↑unitInterval) => 1 + medianSign u * d v) ↔ ∀ᵐ (v₁ : ↑unitInterval) (v₂ : ↑unitInterval), v₁ ≤ v₂ → s * d v₂ ≤ s * d v₁

def Verification.IsRR2 (f : ↑unitInterval → ↑unitInterval → ℝ) : Prop

Reverse regularity on ordered rectangles; equality of coordinates is allowed.

Equations

• Verification.IsRR2 f = ∀ (u₁ u₂ v₁ v₂ : ↑unitInterval), u₁ ≤ u₂ → v₁ ≤ v₂ → f u₁ v₁ * f u₂ v₂ ≤ f u₁ v₂ * f u₂ v₁

def Verification.HasRR2Density (C : ProbabilityTheory.Copula 2) : Prop

Equations

• One or more equations did not get rendered due to their size.

theorem Verification.aeOrderedMinors_of_tp2 {f : ↑unitInterval → ↑unitInterval → ℝ} (h : ProbabilityTheory.IsTP2 f) : HasAEOrderedMinors 1 f

theorem Verification.aeOrderedMinors_of_rr2 {f : ↑unitInterval → ↑unitInterval → ℝ} (h : IsRR2 f) : HasAEOrderedMinors (-1) f

theorem Verification.ae_curry_of_ae_eq {f g : (Fin 2 → ↑unitInterval) → ℝ} (he : f =ᵐ[MeasureTheory.volume] g) : ∀ᵐ (u : ↑unitInterval) (v : ↑unitInterval), f ![u, v] = g ![u, v]

theorem Verification.density_ae_eq {f g : (Fin 2 → ↑unitInterval) → ℝ} (hf : Measurable f) (hg : Measurable g) (hnf : ∀ (x : Fin 2 → ↑unitInterval), 0 ≤ f x) (hng : ∀ (x : Fin 2 → ↑unitInterval), 0 ≤ g x) (he : (MeasureTheory.volume.withDensity fun (x : Fin 2 → ↑unitInterval) => ENNReal.ofReal (f x)) = MeasureTheory.volume.withDensity fun (x : Fin 2 → ↑unitInterval) => ENNReal.ofReal (g x)) : f =ᵐ[MeasureTheory.volume] g