Jcost_n_zero_iff

formal source

  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) :=
  59      Finset.single_le_sum (fun j _ => hnn j) (Finset.mem_univ i)
  60    linarith [h ▸ hle, Jcost_pos_of_ne_one (x i) (hx i) hi]
  61  · intro hall
  62    have : ∀ i : Fin n, Jcost (x i) = 0 := fun i => by rw [hall i, Jcost_unit0]
  63    simp [this]
  64
  65/-- J_n is symmetric channel-wise. -/
  66theorem Jcost_n_symm {n : ℕ} (x : Fin n → ℝ) (hx : ∀ i, 0 < x i) :
  67    Jcost_n x hx = Jcost_n (fun i => (x i)⁻¹) (fun i => inv_pos.mpr (hx i)) := by
  68  unfold Jcost_n
  69  congr 1; ext i; exact Jcost_symm (hx i)
  70
  71structure MultiChannelJCostCert where
  72  nonneg : ∀ {n : ℕ} (x : Fin n → ℝ) (hx : ∀ i, 0 < x i), 0 ≤ Jcost_n x hx
  73  zero_iff : ∀ {n : ℕ} (x : Fin n → ℝ) (hx : ∀ i, 0 < x i),
  74    Jcost_n x hx = 0 ↔ ∀ i, x i = 1
  75  at_ones : ∀ (n : ℕ), Jcost_n (fun (_ : Fin n) => (1 : ℝ)) (fun _ => one_pos) = 0
  76  symm : ∀ {n : ℕ} (x : Fin n → ℝ) (hx : ∀ i, 0 < x i),
  77    Jcost_n x hx = Jcost_n (fun i => (x i)⁻¹) (fun i => inv_pos.mpr (hx i))
  78