P_diagonal

formal source

 126/-! ## Part 3: The Duplication Formula -/
 127
 128/-- Setting x = y gives the duplication formula: F(x²) + F(1) = P(F(x), F(x)) -/
 129theorem P_diagonal
 130    (F : ℝ → ℝ)
 131    (P : ℝ → ℝ → ℝ)
 132    (hUnit : F 1 = 0)
 133    (hCons : ∀ x y : ℝ, 0 < x → 0 < y → F (x * y) + F (x / y) = P (F x) (F y)) :
 134    ∀ x : ℝ, 0 < x → P (F x) (F x) = F (x * x) := by
 135  intro x hx
 136  have h := hCons x x hx hx
 137  simp only [div_self (ne_of_gt hx)] at h
 138  rw [hUnit] at h
 139  linarith
 140
 141/-! ## Part 4: Differential Constraints from Functional Equation
 142
 143The key insight: even without knowing P's form, we can derive that G satisfies
 144the d'Alembert equation, which implies the ODE G'' = G (after shifting).
 145
 146This follows from the *structure* of the equation G(t+u) + G(t-u) = Q(G(t), G(u)).
 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