ClassifiedLogCost

formal source

 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,
 353      show α * (t - u) = α * t - α * u by ring,
 354      Real.cosh_add, Real.cosh_sub]
 355  ring
 356
 357/-- The trigonometric log-cost satisfies the bilinear identity with `c = -2`. -/
 358theorem log_one_sub_cos_bilinear_identity (α : ℝ) :
 359    LogBilinearIdentity (fun t : ℝ => 1 - Real.cos (α * t)) (-2) := by