 147-/
 148
 149/-- The functional equation in log coordinates. -/
 150def LogConsistency (G : ℝ → ℝ) (Q : ℝ → ℝ → ℝ) : Prop :=
 151  ∀ t u : ℝ, G (t + u) + G (t - u) = Q (G t) (G u)
 152
 153/-- From F-consistency to G-consistency in log coordinates. -/
 154theorem log_consistency_of_mult_consistency
 155    (F : ℝ → ℝ)
 156    (P : ℝ → ℝ → ℝ)
 157    (hCons : ∀ x y : ℝ, 0 < x → 0 < y → F (x * y) + F (x / y) = P (F x) (F y)) :
 158    LogConsistency (G F) P := by
 159  intro t u
 160  simp only [G]
 161  have hexp_t : 0 < Real.exp t := Real.exp_pos t
 162  have hexp_u : 0 < Real.exp u := Real.exp_pos u
 163  have h := hCons (Real.exp t) (Real.exp u) hexp_t hexp_u
 164  rw [← Real.exp_add, ← Real.exp_sub] at h
 165  exact h
 166
 167/-- **Key Lemma**: If G satisfies the RCL consistency, then H = G + 1 satisfies d'Alembert. -/
 168theorem H_dAlembert_of_G_RCL
 169    (G : ℝ → ℝ)
 170    (hG0 : G 0 = 0)
 171    (hRCL : ∀ t u : ℝ, G (t + u) + G (t - u) = 2 * G t * G u + 2 * G t + 2 * G u) :
 172    let H := fun t => G t + 1
 173    ∀ t u : ℝ, H (t + u) + H (t - u) = 2 * H t * H u := by
 174  intro H t u
 175  simp only [H]
 176  have h := hRCL t u
 177  -- G(t+u) + G(t-u) = 2*G(t)*G(u) + 2*G(t) + 2*G(u)
 178  -- (G(t+u) + 1) + (G(t-u) + 1) = 2*G(t)*G(u) + 2*G(t) + 2*G(u) + 2
 179  --                              = 2*(G(t)*G(u) + G(t) + G(u) + 1)
 180  --                              = 2*(G(t) + 1)*(G(u) + 1)

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.