Fquad_unit0

formal source

  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
  70  simp [Fquad, Cost.F_ofLog, Gquad, Padd, hlog_mul, hlog_div]
  71  ring
  72
  73/-! ## Calibration holds on the log-lift -/
  74
  75lemma calib_Fquad : deriv (deriv (fun t : ℝ => Fquad (Real.exp t))) 0 = 1 := by
  76  -- Fquad(exp t) = t^2/2
  77  have hfun : (fun t : ℝ => Fquad (Real.exp t)) = fun t => t ^ 2 / 2 := by
  78    funext t
  79    simp [Fquad_on_exp, Gquad]