pith. machine review for the scientific record. sign in
lemma proved tactic proof

Fquad_consistency

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  58lemma Fquad_consistency :
  59    ∀ x y : ℝ, 0 < x → 0 < y →
  60      Fquad (x * y) + Fquad (x / y) = Padd (Fquad x) (Fquad y) := by

proof body

Tactic-mode proof.

  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

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (10)

Lean names referenced from this declaration's body.