jcost_squared_form

formal source

  76  simp [Jcost, Real.exp_neg]
  77
  78/-- **F1.1.8**: The squared form J(x) = (x−1)²/(2x) -/
  79theorem jcost_squared_form {x : ℝ} (hx : x ≠ 0) :
  80    Jcost x = (x - 1) ^ 2 / (2 * x) := Jcost_eq_sq hx
  81
  82/-! ## §2. Zero characterization and ratio interpretation -/
  83
  84/-- **F1.2.1**: J(v/n) = 0 ↔ v = n for v, n > 0 -/
  85theorem jcost_ratio_zero_iff {v n : ℝ} (hv : 0 < v) (hn : 0 < n) :
  86    Jcost (v / n) = 0 ↔ v = n := by
  87  have hvn : 0 < v / n := div_pos hv hn
  88  rw [jcost_eq_zero_iff hvn]
  89  exact div_eq_one_iff_eq (ne_of_gt hn)
  90
  91/-- **F1.2.3**: Total bond cost definition -/
  92noncomputable def totalJcost (v : ℝ) (neighbors : List ℝ) : ℝ :=
  93  (neighbors.map (fun n => Jcost (v / n))).sum
  94
  95/-- Total bond cost is non-negative when v > 0 and all neighbors positive -/
  96theorem totalJcost_nonneg {v : ℝ} {ns : List ℝ} (hv : 0 < v) (hns : ∀ n ∈ ns, 0 < n) :
  97    0 ≤ totalJcost v ns := by
  98  unfold totalJcost
  99  apply List.sum_nonneg
 100  intro x hx
 101  rw [List.mem_map] at hx
 102  obtain ⟨n, hn_mem, hn_eq⟩ := hx
 103  rw [← hn_eq]
 104  exact Jcost_nonneg (div_pos hv (hns n hn_mem))
 105
 106/-! ## §3. Geometric-mean optimality -/
 107
 108/-- **F1.3.2**: The geometric mean of a list of positive reals -/
 109noncomputable def geometricMean (ns : List ℝ) : ℝ :=