totalJcost

formal source

  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 ℝ) : ℝ :=
 110  Real.exp ((ns.map Real.log).sum / ns.length)
 111
 112/-- The geometric mean of positive reals is positive -/
 113theorem geometricMean_pos {ns : List ℝ} (hns : ∀ n ∈ ns, 0 < n) (hne : ns ≠ []) :
 114    0 < geometricMean ns := by
 115  unfold geometricMean
 116  exact Real.exp_pos _
 117
 118/-- **F1.3.2 (two-element case)**: For two positive reals, the geometric mean
 119    minimizes the total J-cost. We prove the key fact: at the geometric mean,
 120    the J-cost is symmetric in the two neighbors. -/
 121theorem totalJcost_at_geomean_symmetric {n₁ n₂ : ℝ} (hn₁ : 0 < n₁) (hn₂ : 0 < n₂) :
 122    let gm := Real.sqrt (n₁ * n₂)