log_bilinear_positive_cost_bilinear

formal source

 449
 450/-- A log-coordinate bilinear identity lifts back to a bilinear combiner on
 451positive ratios. This is the final algebraic assembly step for axiom 2. -/
 452theorem log_bilinear_positive_cost_bilinear
 453    (F : ℝ → ℝ)
 454    (hLog : ∃ c : ℝ, LogBilinearIdentity (fun t : ℝ => F (Real.exp t)) c) :
 455    ∃ (P : ℝ → ℝ → ℝ) (c : ℝ),
 456      (∀ x y : ℝ, 0 < x → 0 < y →
 457        F (x * y) + F (x / y) = P (F x) (F y)) ∧
 458      (∀ u v, P u v = 2*u + 2*v + c*u*v) := by
 459  obtain ⟨c, hbil⟩ := hLog
 460  refine ⟨fun u v => 2*u + 2*v + c*u*v, c, ?_, ?_⟩
 461  · intro x y hx hy
 462    have hx_exp : Real.exp (Real.log x) = x := Real.exp_log hx
 463    have hy_exp : Real.exp (Real.log y) = y := Real.exp_log hy
 464    have h := hbil (Real.log x) (Real.log y)
 465    dsimp only at h
 466    rw [← hx_exp, ← hy_exp]
 467    rw [← Real.exp_add, ← Real.exp_sub]
 468    exact h
 469  · intro u v
 470    rfl
 471
 472/-! ## 4. Continuous version of `bilinear_family_forced`
 473
 474Under continuity of the combiner, the Aczél–Kannappan classification
 475forces the same bilinear conclusion as the polynomial case. We obtain
 476the continuous-case Translation Theorem.
 477
 478The argument matches the polynomial-case argument up to the point at
 479which the d'Alembert equation is recovered on the cosh-add identity.
 480At that point, the polynomial-case derivation used the
 481polynomial-form lemma; the continuous-case derivation uses the named
 482Aczél–Kannappan classification theorem above plus the two residual