theorem
proved
term proof
log_bilinear_positive_cost_bilinear
show as:
view Lean formalization →
formal statement (Lean)
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
proof body
Term-mode proof.
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
483combiner-side analysis inputs named below. -/
484
485/-- **Named analysis input 1a: finite-order mollifier derivative control.**
486
487For every finite differentiability order, the mollifier route gives a
488`C^n` bound/limit certificate for the log-coordinate derived cost
489`G(t) = F(exp t)`. This is the precise analytic estimate left in Piece 1:
490the bump family exists and converges pointwise by theorem above; what remains
491is controlling derivatives on compact intervals strongly enough to pass the
492limit back to `G`. -/