P_at_zero_left

formal source

  93/-! ## Part 2: P(u, 0) = 2u from Normalization -/
  94
  95/-- If F(1) = 0 and the consistency equation holds, then P(u, 0) = 2u on the range of F. -/
  96theorem P_at_zero_left
  97    (F : ℝ → ℝ)
  98    (P : ℝ → ℝ → ℝ)
  99    (hUnit : F 1 = 0)
 100    (hCons : ∀ x y : ℝ, 0 < x → 0 < y → F (x * y) + F (x / y) = P (F x) (F y)) :
 101    ∀ x : ℝ, 0 < x → P (F x) 0 = 2 * F x := by
 102  intro x hx
 103  -- Set y = 1 in the consistency equation
 104  have h := hCons x 1 hx one_pos
 105  simp only [mul_one, div_one] at h
 106  rw [hUnit] at h
 107  -- h : F x + F x = P (F x) 0
 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 -/