Jcost_n

formal source

  25open Cost
  26
  27/-- Multi-channel J-cost: sum of individual J-costs. -/
  28noncomputable def Jcost_n {n : ℕ} (x : Fin n → ℝ) (hx : ∀ i, 0 < x i) : ℝ :=
  29  ∑ i, Jcost (x i)
  30
  31/-- J_n ≥ 0. -/
  32theorem Jcost_n_nonneg {n : ℕ} (x : Fin n → ℝ) (hx : ∀ i, 0 < x i) :
  33    0 ≤ Jcost_n x hx := by
  34  unfold Jcost_n
  35  apply Finset.sum_nonneg
  36  intro i _
  37  by_cases h : x i = 1
  38  · simp [h, Jcost_unit0]
  39  · exact le_of_lt (Jcost_pos_of_ne_one (x i) (hx i) h)
  40
  41/-- The multi-channel fixed point is 1⃗. -/
  42theorem Jcost_n_at_ones {n : ℕ} :
  43    @Jcost_n n (fun _ => (1 : ℝ)) (fun _ => one_pos) = 0 := by
  44  unfold Jcost_n
  45  simp [Jcost_unit0]
  46
  47/-- J_n = 0 iff all channels at equilibrium. -/
  48theorem Jcost_n_zero_iff {n : ℕ} (x : Fin n → ℝ) (hx : ∀ i, 0 < x i) :
  49    Jcost_n x hx = 0 ↔ ∀ i, x i = 1 := by
  50  unfold Jcost_n
  51  constructor
  52  · intro h i
  53    by_contra hi
  54    have hnn : ∀ j : Fin n, 0 ≤ Jcost (x j) := fun j => by
  55      by_cases hj : x j = 1
  56      · rw [hj, Jcost_unit0]
  57      · exact le_of_lt (Jcost_pos_of_ne_one (x j) (hx j) hj)
  58    have hle : Jcost (x i) ≤ ∑ j : Fin n, Jcost (x j) :=