← Mathematical handbook

noncomputable def Verification.spectralTail {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (X Y : Ω → ℝ) (x y : ℝ) : ℝ

Equations

• Verification.spectralTail μ X Y x y = ∫ (ω : Ω), max (x * X ω) (y * Y ω) ∂μ

theorem Verification.spectralTail_integrable {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (X Y : Ω → ℝ) (hX : MeasureTheory.Integrable X μ) (hY : MeasureTheory.Integrable Y μ) (x y : ℝ) : MeasureTheory.Integrable (fun (ω : Ω) => max (x * X ω) (y * Y ω)) μ

theorem Verification.spectralTail_nonneg {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (X Y : Ω → ℝ) (hX : ∀ (ω : Ω), 0 ≤ X ω) {x y : ℝ} (hx : 0 ≤ x) : 0 ≤ spectralTail μ X Y x y

theorem Verification.spectralTail_mono {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (X Y : Ω → ℝ) (hXi : MeasureTheory.Integrable X μ) (hYi : MeasureTheory.Integrable Y μ) (hX : ∀ (ω : Ω), 0 ≤ X ω) (hY : ∀ (ω : Ω), 0 ≤ Y ω) {x₁ x₂ y₁ y₂ : ℝ} (hx : x₁ ≤ x₂) (hy : y₁ ≤ y₂) : spectralTail μ X Y x₁ y₁ ≤ spectralTail μ X Y x₂ y₂

theorem Verification.max_four_point {a b c d : ℝ} (hab : a ≤ b) (hcd : c ≤ d) : max a c + max b d ≤ max a d + max b c

theorem Verification.spectralTail_submodular {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (X Y : Ω → ℝ) (hXi : MeasureTheory.Integrable X μ) (hYi : MeasureTheory.Integrable Y μ) (hX : ∀ (ω : Ω), 0 ≤ X ω) (hY : ∀ (ω : Ω), 0 ≤ Y ω) {x₁ x₂ y₁ y₂ : ℝ} (hx : x₁ ≤ x₂) (hy : y₁ ≤ y₂) : spectralTail μ X Y x₁ y₁ + spectralTail μ X Y x₂ y₂ ≤ spectralTail μ X Y x₁ y₂ + spectralTail μ X Y x₂ y₁

theorem Verification.spectralTail_zero_right {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (X Y : Ω → ℝ) (hX : ∀ (ω : Ω), 0 ≤ X ω) (hXm : ∫ (ω : Ω), X ω ∂μ = 1) {x : ℝ} (hx : 0 ≤ x) : spectralTail μ X Y x 0 = x

theorem Verification.spectralTail_zero_left {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (X Y : Ω → ℝ) (hY : ∀ (ω : Ω), 0 ≤ Y ω) (hYm : ∫ (ω : Ω), Y ω ∂μ = 1) {y : ℝ} (hy : 0 ≤ y) : spectralTail μ X Y 0 y = y

theorem Verification.spectralTail_homogeneous {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (X Y : Ω → ℝ) (x y c : ℝ) (hc : 0 ≤ c) : spectralTail μ X Y (c * x) (c * y) = c * spectralTail μ X Y x y