pith. machine review for the scientific record. sign in
theorem proved term proof

Jcost_n_zero_iff

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  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

proof body

Term-mode proof.

  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. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (10)

Lean names referenced from this declaration's body.