• Weighted Sum over the Standard Simplex

• def stdSimplex.mix EconCSLib @ cef01c7, EconCSLib.Math.Simplex

  def stdSimplex.mix (α : 𝕜) (hα₀ : 0 ≤ α) (hα₁ : α ≤ 1)
      (x y : stdSimplex 𝕜 I) : stdSimplex 𝕜 I where
    val i := α * x.val i + (1 - α) * y.val i
    property := by
      refine ⟨fun i => ?_, ?_⟩
      · have hx := x.property.1 i
        have hy := y.property.1 i
        have hα' : 0 ≤ 1 - α := by linarith
        have h₁ : 0 ≤ α * x.val i := mul_nonneg hα₀ hx
        have h₂ : 0 ≤ (1 - α) * y.val i := mul_nonneg hα' hy
        linarith
      · have hxsum := x.property.2
        have hysum := y.property.2
        have : (∑ i, (α * x.val i + (1 - α) * y.val i))
            = α * (∑ i, x.val i) + (1 - α) * (∑ i, y.val i) := by
          rw [Finset.sum_add_distrib, ← Finset.mul_sum, ← Finset.mul_sum]
        rw [this, hxsum, hysum]; ring

• theorem stdSimplex.mix_apply EconCSLib @ cef01c7, EconCSLib.Math.Simplex

  theorem stdSimplex.mix_apply (α : 𝕜) (hα₀ : 0 ≤ α) (hα₁ : α ≤ 1)
      (x y : stdSimplex 𝕜 I) (i : I) :
      (stdSimplex.mix α hα₀ hα₁ x y).val i = α * x.val i + (1 - α) * y.val i

• theorem wsum_mix EconCSLib @ cef01c7, EconCSLib.Math.Simplex

  theorem wsum_mix (α : 𝕜) (hα₀ : 0 ≤ α) (hα₁ : α ≤ 1)
      (x y : stdSimplex 𝕜 I) (f : I → 𝕜) :
      wsum (stdSimplex.mix α hα₀ hα₁ x y) f =
        α * wsum x f + (1 - α) * wsum y f

• theorem linear_comb_gt_left EconCSLib @ cef01c7, EconCSLib.Math.Simplex

  If `x < y` and `α < 1`, then `α·x + (1-α)·y > x`.

  theorem linear_comb_gt_left {x y : 𝕜} (H : x < y) {α : 𝕜} (Hα : α < 1) :
      x < α * x + (1 - α) * y

• theorem linear_comb_gt_right EconCSLib @ cef01c7, EconCSLib.Math.Simplex

  If `y < x` and `0 < α`, then `α·x + (1-α)·y > y`.

  theorem linear_comb_gt_right {x y : 𝕜} (H : y < x) {α : 𝕜} (Hα : 0 < α) :
      y < α * x + (1 - α) * y

• theorem linear_comb_gt_of_ge_gt EconCSLib @ cef01c7, EconCSLib.Math.Simplex

  Convex combination of "≥ c" and "> c" stays "> c" (provided `α ≥ 0` and `α < 1`).

  theorem linear_comb_gt_of_ge_gt (x y c : 𝕜) (H1 : c ≤ x) (H2 : c < y)
      {α : 𝕜} (hα₀ : 0 ≤ α) (hα₁ : α < 1) :
      c < α * x + (1 - α) * y

• theorem linear_comb_lt_of_le_lt EconCSLib @ cef01c7, EconCSLib.Math.Simplex

  Convex combination of "≤ c" and "< c" stays "< c" (provided `α ≥ 0` and `α < 1`).

  theorem linear_comb_lt_of_le_lt (x y c : 𝕜) (H1 : x ≤ c) (H2 : y < c)
      {α : 𝕜} (hα₀ : 0 ≤ α) (hα₁ : α < 1) :
      α * x + (1 - α) * y < c

• theorem wsum_mix_gt_of_ge_gt EconCSLib @ cef01c7, EconCSLib.Math.Simplex

  `wsum` version of `linear_comb_gt_of_ge_gt`.

  theorem wsum_mix_gt_of_ge_gt {I : Type*} [Fintype I]
      (f : I → 𝕜) (x y : stdSimplex 𝕜 I) (c : 𝕜)
      (H1 : c ≤ wsum x f) (H2 : c < wsum y f)
      {t : 𝕜} (ht₀ : 0 ≤ t) (ht₁ : t ≤ 1) (Ht : t < 1) :
      c < wsum (stdSimplex.mix t ht₀ ht₁ x y) f

• theorem wsum_mix_lt_of_le_lt EconCSLib @ cef01c7, EconCSLib.Math.Simplex

  `wsum` version of `linear_comb_lt_of_le_lt`.

  theorem wsum_mix_lt_of_le_lt {I : Type*} [Fintype I]
      (f : I → 𝕜) (x y : stdSimplex 𝕜 I) (c : 𝕜)
      (H1 : wsum x f ≤ c) (H2 : wsum y f < c)
      {t : 𝕜} (ht₀ : 0 ≤ t) (ht₁ : t ≤ 1) (Ht : t < 1) :
      wsum (stdSimplex.mix t ht₀ ht₁ x y) f < c

• theorem mix_gt_of_gt_nbh EconCSLib @ cef01c7, EconCSLib.Math.Simplex

  theorem mix_gt_of_gt_nbh (x y c : 𝕜) (H : c < x) :
      ∃ t : 𝕜, 0 < t ∧ t < 1 ∧ c < t * x + (1 - t) * y

• theorem mix_lt_of_lt_nbh EconCSLib @ cef01c7, EconCSLib.Math.Simplex

  theorem mix_lt_of_lt_nbh (x y c : 𝕜) (H : x < c) :
      ∃ t : 𝕜, 0 < t ∧ t < 1 ∧ t * x + (1 - t) * y < c

Modules: EconCSLib.Math.Simplex