G_of

formal source

  44/-! ## Log-Coordinate Setup -/
  45
  46/-- The log-lift of a cost function. -/
  47noncomputable def G_of (F : ℝ → ℝ) (t : ℝ) : ℝ := F (Real.exp t)
  48
  49/-- The shifted log-lift (for d'Alembert). -/
  50noncomputable def H_of (F : ℝ → ℝ) (t : ℝ) : ℝ := G_of F t + 1
  51
  52/-! ## Consistency in Log-Coordinates -/
  53
  54/-- If F has multiplicative consistency, then G has additive consistency. -/
  55theorem log_consistency (F : ℝ → ℝ) (P : ℝ → ℝ → ℝ)
  56    (hCons : ∀ x y : ℝ, 0 < x → 0 < y → F (x * y) + F (x / y) = P (F x) (F y)) :
  57    ∀ t u : ℝ, G_of F (t + u) + G_of F (t - u) = P (G_of F t) (G_of F u) := by
  58  intro t u
  59  simp only [G_of]
  60  have hpos_t : 0 < Real.exp t := Real.exp_pos t
  61  have hpos_u : 0 < Real.exp u := Real.exp_pos u
  62  have h := hCons (Real.exp t) (Real.exp u) hpos_t hpos_u
  63  simp only [Real.exp_add, Real.exp_sub] at h
  64  convert h using 2
  65  · rw [Real.exp_add]
  66  · rw [Real.exp_sub]
  67
  68/-! ## Boundary Conditions on Q (= P) -/
  69
  70/-- From normalization F(1) = 0, we get G(0) = 0. -/
  71theorem G_zero (F : ℝ → ℝ) (hNorm : F 1 = 0) : G_of F 0 = 0 := by
  72  simp only [G_of, Real.exp_zero, hNorm]
  73
  74/-- From consistency at u = 0: G(t) + G(t) = Q(G(t), 0), so Q(a, 0) = 2a. -/
  75theorem Q_boundary_v (F : ℝ → ℝ) (P : ℝ → ℝ → ℝ)
  76    (hNorm : F 1 = 0)
  77    (hCons : ∀ x y : ℝ, 0 < x → 0 < y → F (x * y) + F (x / y) = P (F x) (F y)) :