P_at_zero_right

formal source

 108  linarith
 109
 110/-- Similarly, P(0, v) = 2v on the range of F. -/
 111theorem P_at_zero_right
 112    (F : ℝ → ℝ)
 113    (P : ℝ → ℝ → ℝ)
 114    (hUnit : F 1 = 0)
 115    (hSymm : ∀ x : ℝ, 0 < x → F x = F x⁻¹)
 116    (hCons : ∀ x y : ℝ, 0 < x → 0 < y → F (x * y) + F (x / y) = P (F x) (F y)) :
 117    ∀ y : ℝ, 0 < y → P 0 (F y) = 2 * F y := by
 118  intro y hy
 119  -- Use symmetry of P
 120  have hP_symm := P_symmetric_of_F_symmetric F P hSymm hCons 1 y one_pos hy
 121  rw [hUnit] at hP_symm
 122  have h := P_at_zero_left F P hUnit hCons y hy
 123  rw [hP_symm]
 124  exact h
 125
 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