Cost

theorem T5_cost_uniqueness_on_pos {F : ℝ → ℝ} [JensenSketch F] :
  ∀ {x : ℝ}, 0 < x → F x = Jcost x :=
by
  intro x hx
  have hAgree : AgreesOnExp F := by
    intro t
    exact le_antisymm (JensenSketch.axis_upper (F:=F) t) (JensenSketch.axis_lower (F:=F) t)
  exact (agree_on_exp_extends (F:=F) hAgree) hx

lemma Jcost_unit0 : Jcost 1 = 0 := by
  simp [Jcost]

lemma Jcost_symm {x : ℝ} (hx : 0 < x) : Jcost x = Jcost x⁻¹ := by
  have hx0 : x ≠ 0 := ne_of_gt hx
  rw [Jcost_eq_sq hx0, Jcost_eq_sq (inv_ne_zero hx0)]
  field_simp [hx0]
  ring

/-- J(x) ≥ 0 for positive x (AM-GM inequality) -/
lemma Jcost_nonneg {x : ℝ} (hx : 0 < x) : 0 ≤ Jcost x := by
  have hx0 : x ≠ 0 := hx.ne'
  rw [Jcost_eq_sq hx0]
  positivity

/-- From J(x) = 0 and x > 0, conclude x = 1. -/
lemma Jcost_zero_iff_one {x : ℝ} (hx : 0 < x) (h : Jcost x = 0) : x = 1 :=
  (Jcost_eq_zero_iff x hx).mp h

/-- J-cost is strictly increasing on `[1, ∞)`.

This root-module copy keeps downstream files from importing both
`IndisputableMonolith.Cost` and `IndisputableMonolith.Cost.JcostCore`, which
define overlapping names in the same namespace. -/
lemma Jcost_strict_mono_on_one_infty (x y : ℝ) (hx : 0 < x) (hy : 0 < y)
    (hx1 : 1 ≤ x) (hxy : x < y) :
    Jcost x < Jcost y := by
  have hx0 : x ≠ 0 := ne_of_gt hx
  have hy0 : y ≠ 0 := ne_of_gt hy
  rw [Jcost_eq_sq hx0, Jcost_eq_sq hy0]
  have h2x : 0 < 2 * x := by linarith
  have h2y : 0 < 2 * y := by linarith
  rw [div_lt_div_iff₀ h2x h2y]
  have hmain : (x - 1) ^ 2 * (2 * y) < (y - 1) ^ 2 * (2 * x) := by
    let f : ℝ → ℝ := fun t => (t - 1) ^ 2 / t
    have hf_mono : ∀ a b : ℝ, 1 ≤ a → a < b → f a < f b := by
      intro a b ha hab
      simp only [f]
      have ha0 : (0 : ℝ) < a := by linarith
      have hb0 : (0 : ℝ) < b := by linarith
      rw [div_lt_div_iff₀ ha0 hb0]
      have : (a - 1) ^ 2 * b - (b - 1) ^ 2 * a < 0 := by
        have hcalc : (a - 1) ^ 2 * b - (b - 1) ^ 2 * a = (a - b) * (a * b - 1) := by
          ring
        rw [hcalc]
        have h1 : a - b < 0 := by linarith
        have h2 : a * b - 1 > 0 := by nlinarith
        nlinarith
      linarith
    have := hf_mono x y hx1 hxy
    simp only [f] at this
    rw [div_lt_div_iff₀ hx hy] at this
    calc
      (x - 1) ^ 2 * (2 * y) = 2 * ((x - 1) ^ 2 * y) := by ring
      _ < 2 * ((y - 1) ^ 2 * x) := by nlinarith
      _ = (y - 1) ^ 2 * (2 * x) := by ring
  exact hmain

lemma Jcost_small_strain_bound (ε : ℝ) (hε : |ε| ≤ (1 : ℝ) / 10) :
    |Jcost (1 + ε) - ε ^ 2 / 2| ≤ ε ^ 2 / 10 := by
  classical
  have hbounds := abs_le.mp hε
  have hpos : 0 < 1 + ε := by
    have : -(1 : ℝ) / 10 ≤ ε := by simpa [neg_div] using hbounds.1
    linarith
  have hne : 1 + ε ≠ 0 := ne_of_gt hpos
  have hform : Jcost (1 + ε) = ε ^ 2 / (2 * (1 + ε)) := by
    simpa [pow_two, add_comm, add_left_comm, add_assoc, sub_eq_add_neg]
      using (Jcost_eq_sq hne)
  have hden_pos : 0 < 2 * (1 + ε) := by nlinarith [hpos]
  -- Exact difference and absolute value
  have h1 : Jcost (1 + ε) - ε ^ 2 / 2
      = ε ^ 2 / (2 * (1 + ε)) - ε ^ 2 / 2 := by
    simp [hform]
  have hx : (2 : ℝ) * (1 + ε) ≠ 0 := mul_ne_zero two_ne_zero hne
  have h2 : ε ^ 2 / (2 * (1 + ε)) - ε ^ 2 / 2 = -ε ^ 3 / (2 * (1 + ε)) := by
    field_simp [hx]
    ring
  have hdiff : Jcost (1 + ε) - ε ^ 2 / 2 = -ε ^ 3 / (2 * (1 + ε)) := h1.trans h2
  have habs : |Jcost (1 + ε) - ε ^ 2 / 2| = |ε| ^ 3 / (2 * (1 + ε)) := by
    have hposden : 0 < 2 * (1 + ε) := hden_pos
    simpa [abs_div, abs_neg, abs_pow, abs_of_pos hposden] using
      congrArg (fun z => |z|) hdiff
  -- Now bound using |ε|/(2(1+ε)) ≤ 1/18 from below
  have hx_lower : (9 : ℝ) / 10 ≤ 1 + ε := by linarith [show -(1 : ℝ) / 10 ≤ ε from by simpa [neg_div] using hbounds.1]
  have hx_pos : 0 < (9 : ℝ) / 10 := by norm_num
  have hx_inv : 1 / (1 + ε) ≤ (10 : ℝ) / 9 := by
    have := one_div_le_one_div_of_le hx_pos hx_lower
    simpa using this
  have hrec_bound : 1 / (2 * (1 + ε)) ≤ (5 : ℝ) / 9 := by
    have hmul : (1 / 2 : ℝ) * (1 / (1 + ε)) ≤ (1 / 2) * ((10 : ℝ) / 9) :=
      mul_le_mul_of_nonneg_left hx_inv (by norm_num)
    have hleft : 1 / (2 * (1 + ε)) = (1 / 2) * (1 / (1 + ε)) := by
      simp [div_eq_mul_inv, mul_comm]
    have hright : (5 : ℝ) / 9 = (1 / 2) * ((10 : ℝ) / 9) := by norm_num
    simpa [hleft, hright] using hmul
  have hrec_nonneg : 0 ≤ 1 / (2 * (1 + ε)) := by
    have : 0 ≤ 2 * (1 + ε) := le_of_lt (by nlinarith [hpos])
    exact one_div_nonneg.mpr this
  have hA : |ε| / (2 * (1 + ε)) ≤ (1 : ℝ) / 10 * (1 / (2 * (1 + ε))) := by
    simpa [div_eq_mul_inv, mul_comm, mul_left_comm, mul_assoc]
      using mul_le_mul_of_nonneg_right hε hrec_nonneg
  have hB : (1 : ℝ) / 10 * (1 / (2 * (1 + ε))) ≤ (1 : ℝ) / 18 := by
    have hmul := mul_le_mul_of_nonneg_left hrec_bound (by norm_num : (0 : ℝ) ≤ (1 : ℝ) / 10)
    have hright : (1 : ℝ) / 18 = (1 : ℝ) / 10 * ((5 : ℝ) / 9) := by norm_num
    simpa [hright] using hmul
  have hfrac : |ε| / (2 * (1 + ε)) ≤ (1 : ℝ) / 18 := hA.trans hB
  -- Conclude
  have hineq : |Jcost (1 + ε) - ε ^ 2 / 2| ≤ |ε| ^ 2 / 18 := by
    have hnn : 0 ≤ |ε| ^ 2 := by
      have := sq_nonneg (|ε|); simpa [pow_two] using this
    have hmul := mul_le_mul_of_nonneg_left hfrac hnn
    calc
      |Jcost (1 + ε) - ε ^ 2 / 2| = |ε| ^ 3 / (2 * (1 + ε)) := by simp [habs]
      _ ≤ |ε| ^ 2 * (1 / 18) := by
        simpa [pow_succ, pow_two, mul_comm, mul_left_comm, mul_assoc, div_eq_mul_inv] using hmul
      _ = |ε| ^ 2 / 18 := by simp [div_eq_mul_inv]
  have hratio : (1 : ℝ) / 18 ≤ 1 / 10 := by norm_num
  have hsq : |ε| ^ 2 = ε ^ 2 := by
    have h1 : |ε| * |ε| = |ε * ε| := by simp [abs_mul]
    calc
      |ε| ^ 2 = |ε| * |ε| := by simp [pow_two]
      _ = |ε * ε| := h1
      _ = |ε ^ 2| := by simp [pow_two]
      _ = ε ^ 2 := by simp [abs_of_nonneg (sq_nonneg ε)]
  have hcompare : |ε| ^ 2 / 18 ≤ ε ^ 2 / 10 := by
    have := mul_le_mul_of_nonneg_left hratio (by exact sq_nonneg ε)
    simpa [hsq, pow_two] using this
  exact (hineq.trans hcompare)