Gquad

formal source

  36
  37/-! ## The quadratic log-cost -/
  38
  39noncomputable def Gquad (t : ℝ) : ℝ := t ^ 2 / 2
  40
  41noncomputable def Fquad : ℝ → ℝ := Cost.F_ofLog Gquad
  42
  43noncomputable def Padd (u v : ℝ) : ℝ := 2 * u + 2 * v
  44
  45lemma Fquad_on_exp (t : ℝ) : Fquad (Real.exp t) = Gquad t := by
  46  -- log(exp t) = t
  47  simp [Fquad, Cost.F_ofLog, Gquad]
  48
  49lemma Fquad_unit0 : Fquad 1 = 0 := by
  50  simp [Fquad, Cost.F_ofLog, Gquad]
  51
  52lemma Fquad_symm {x : ℝ} (hx : 0 < x) : Fquad x = Fquad x⁻¹ := by
  53  -- log(x⁻¹) = -log x for x>0
  54  simp [Fquad, Cost.F_ofLog, Gquad, Real.log_inv, hx.ne']
  55
  56/-! ## The weak consistency holds with an additive combiner -/
  57
  58lemma Fquad_consistency :
  59    ∀ x y : ℝ, 0 < x → 0 < y →
  60      Fquad (x * y) + Fquad (x / y) = Padd (Fquad x) (Fquad y) := by
  61  intro x y hx hy
  62  -- Work in log-coordinates: let t = log x, u = log y
  63  have hx0 : x ≠ 0 := hx.ne'
  64  have hy0 : y ≠ 0 := hy.ne'
  65  have hlog_mul : Real.log (x * y) = Real.log x + Real.log y := by
  66    simpa using Real.log_mul hx.ne' hy.ne'
  67  have hlog_div : Real.log (x / y) = Real.log x - Real.log y := by
  68    simpa [div_eq_mul_inv, Real.log_mul, Real.log_inv, hy0] using Real.log_div hx.ne' hy.ne'
  69  -- Now compute