LogBilinearIdentity

formal source

 319-/
 320
 321/-- Log-coordinate bilinear identity with coefficient `c`. -/
 322def LogBilinearIdentity (G : ℝ → ℝ) (c : ℝ) : Prop :=
 323  ∀ t u : ℝ,
 324    G (t + u) + G (t - u) = 2 * G t + 2 * G u + c * G t * G u
 325
 326/-- A classified log-coordinate cost: parabolic, hyperbolic, trigonometric,
 327or zero. This is the algebraic target left after the smoothness/affine-forcing
 328analysis has been done. -/
 329def ClassifiedLogCost (G : ℝ → ℝ) : Prop :=
 330  (∀ t, G t = 0) ∨
 331  (∃ α : ℝ, ∀ t, G t = α * t^2) ∨
 332  (∃ α : ℝ, ∀ t, G t = Real.cosh (α * t) - 1) ∨
 333  (∃ α : ℝ, ∀ t, G t = 1 - Real.cos (α * t))
 334
 335/-- The zero log-cost satisfies the bilinear identity with any coefficient. -/
 336theorem log_zero_bilinear_identity :
 337    LogBilinearIdentity (fun _ : ℝ => 0) 0 := by
 338  intro t u
 339  ring
 340
 341/-- The parabolic log-cost satisfies the additive (`c = 0`) bilinear identity. -/
 342theorem log_parabolic_bilinear_identity (α : ℝ) :
 343    LogBilinearIdentity (fun t : ℝ => α * t^2) 0 := by
 344  intro t u
 345  ring
 346
 347/-- The hyperbolic log-cost satisfies the RCL bilinear identity (`c = 2`). -/
 348theorem log_cosh_sub_one_bilinear_identity (α : ℝ) :
 349    LogBilinearIdentity (fun t : ℝ => Real.cosh (α * t) - 1) 2 := by
 350  intro t u
 351  simp only
 352  rw [show α * (t + u) = α * t + α * u by ring,