Documentation

LeanPool.BollobasNikiforov.TN.Convex

Convex vanishing at zero and total nonnegativity #

Lemma lem:convex of docs/sol.tex: if f : [0, ∞) → [0, ∞) is convex and f 0 = 0, then for 0 < t₁ ≤ ⋯ ≤ tₖ the matrix with rows (1, tᵢ, f tᵢ) is totally nonnegative.

TN14: monotonicity of f and of f t / t #

source
theorem BollobasNikiforov.convexOn_Ici_zero_div_monotoneOn {f : ℝ → ℝ} (hf : ConvexOn ℝ (Set.Ici 0) f) (hf0 : f 0 = 0) :
MonotoneOn (fun (t : ℝ) => f t / t) (Set.Ioi 0)

Convexity on [0, ∞) together with f 0 = 0 makes t ↦ f t / t nondecreasing on (0, ∞).

source
theorem BollobasNikiforov.convexOn_Ici_zero_monotoneOn {f : ℝ → ℝ} (hf : ConvexOn ℝ (Set.Ici 0) f) (hf0 : f 0 = 0) (hfnn : ∀ (x : ℝ), 0 ≤ x → 0 ≤ f x) :
MonotoneOn f (Set.Ici 0)

A nonnegative convex function on [0, ∞) with f 0 = 0 is nondecreasing there.

TN15: size-one and size-two minors of rows (1, t, f t) #

source
def BollobasNikiforov.row3 (f : ℝ → ℝ) (t : ℝ) :
Fin 3 → ℝ

The feature row (1, t, f t).

Equations
Instances For
    source
    @[simp]
    theorem BollobasNikiforov.row3_zero (f : ℝ → ℝ) (t : ℝ) :
    row3 f t 0 = 1
    source
    @[simp]
    theorem BollobasNikiforov.row3_one (f : ℝ → ℝ) (t : ℝ) :
    row3 f t 1 = t
    source
    @[simp]
    theorem BollobasNikiforov.row3_two (f : ℝ → ℝ) (t : ℝ) :
    row3 f t 2 = f t
    source
    def BollobasNikiforov.convexRowMatrix {ι : Type u_1} (f : ℝ → ℝ) (t : ι → ℝ) :
    Matrix ι (Fin 3) ℝ

    The ι × 3 matrix whose ith row is (1, t i, f (t i)).

    Equations
    Instances For
      source
      theorem BollobasNikiforov.row3_nonneg {f : ℝ → ℝ} (hfnn : ∀ (x : ℝ), 0 ≤ x → 0 ≤ f x) {t : ℝ} (ht : 0 < t) (j : Fin 3) :
      0 ≤ row3 f t j
      source
      theorem BollobasNikiforov.row3_one_two_minors_nonneg {f : ℝ → ℝ} (hf : ConvexOn ℝ (Set.Ici 0) f) (hf0 : f 0 = 0) (hfnn : ∀ (x : ℝ), 0 ≤ x → 0 ≤ f x) {t u : ℝ} (ht : 0 < t) (htu : t ≤ u) :
      (∀ (j : Fin 3), 0 ≤ row3 f t j) ∧ 0 ≤ u - t ∧ 0 ≤ f u - f t ∧ 0 ≤ t * f u - u * f t

      Every 1 × 1 and 2 × 2 minor of two increasing rows (1, t, f t), (1, u, f u) is nonnegative.

      TN16: the 3 × 3 minor #

      source
      theorem BollobasNikiforov.convex_three_slope {f : ℝ → ℝ} (hf : ConvexOn ℝ (Set.Ici 0) f) {t u v : ℝ} (ht : 0 < t) (htu : t < u) (huv : u < v) :
      0 ≤ (u - t) * (f v - f t) - (v - t) * (f u - f t)

      Three-slope comparison: for 0 < t < u < v the displayed 3 × 3 minor expression is nonnegative.

      source
      def BollobasNikiforov.row3Triple {f : ℝ → ℝ} (t u v : ℝ) :
      Matrix (Fin 3) (Fin 3) ℝ

      Three rows (1, t, f t), (1, u, f u), (1, v, f v).

      Equations
      Instances For
        source
        def BollobasNikiforov.row3Pair {f : ℝ → ℝ} (t u : ℝ) (J : Fin 2 → Fin 3) :
        Matrix (Fin 2) (Fin 2) ℝ

        Two rows (1, t, f t), (1, u, f u) on a pair of columns J.

        Equations
        Instances For
          source
          theorem BollobasNikiforov.det_row3Triple {f : ℝ → ℝ} (t u v : ℝ) :
          (row3Triple t u v).det = (u - t) * (f v - f t) - (v - t) * (f u - f t)

          TN17: lem:convex #

          source
          theorem BollobasNikiforov.det_convexRowMatrix_two {f : ℝ → ℝ} (hf : ConvexOn ℝ (Set.Ici 0) f) (hf0 : f 0 = 0) (hfnn : ∀ (x : ℝ), 0 ≤ x → 0 ≤ f x) {t u : ℝ} (ht : 0 < t) (htu : t ≤ u) {J : Fin 2 → Fin 3} (hJ : StrictMono J) :
          0 ≤ (row3Pair t u J).det
          source
          theorem BollobasNikiforov.det_convexRowMatrix_three {f : ℝ → ℝ} (hf : ConvexOn ℝ (Set.Ici 0) f) {t u v : ℝ} (ht : 0 < t) (htu : t ≤ u) (huv : u ≤ v) :
          0 ≤ (row3Triple t u v).det
          source
          theorem BollobasNikiforov.isTotallyNonneg_convexRowMatrix {f : ℝ → ℝ} (hf : ConvexOn ℝ (Set.Ici 0) f) (hf0 : f 0 = 0) (hfnn : ∀ (x : ℝ), 0 ≤ x → 0 ≤ f x) {k : ℕ} {t : Fin k → ℝ} (htmono : Monotone t) (htpos : ∀ (i : Fin k), 0 < t i) :
          IsTotallyNonneg (convexRowMatrix f t)

          Lemma lem:convex: rows (1, tᵢ, f tᵢ) of a nonnegative convex f vanishing at 0 form a totally nonnegative matrix, for 0 < t₁ ≤ ⋯ ≤ tₖ.