HasMultiplicativeConsistency

formal source

  69    ∀ u v, P u v = a + b*u + c*v + d*u*v + e*u^2 + f*v^2
  70
  71/-- Multiplicative consistency: F(xy) + F(x/y) = P(F(x), F(y)) -/
  72def HasMultiplicativeConsistency (F : ℝ → ℝ) (P : ℝ → ℝ → ℝ) : Prop :=
  73  ∀ x y : ℝ, 0 < x → 0 < y → F (x * y) + F (x / y) = P (F x) (F y)
  74
  75/-! ## Derived Reciprocity (P-symmetry ⇒ F(x) = F(1/x)) -/
  76
  77/-- If the combiner `P` is symmetric and `F` is multiplicatively consistent with `P`,
  78then `F(x/y) = F(y/x)` for all `x,y>0`. -/
  79theorem F_div_swap_of_P_symmetric (F : ℝ → ℝ) (P : ℝ → ℝ → ℝ)
  80    (hCons : HasMultiplicativeConsistency F P)
  81    (hSymP : ∀ u v, P u v = P v u) :
  82    ∀ x y : ℝ, 0 < x → 0 < y → F (x / y) = F (y / x) := by
  83  intro x y hx hy
  84  have hxy := hCons x y hx hy
  85  have hyx := hCons y x hy hx
  86  have hyx' : F (x * y) + F (y / x) = P (F x) (F y) := by
  87    -- rewrite y*x = x*y and use symmetry of P on the RHS
  88    simpa [mul_comm, hSymP (F y) (F x)] using hyx
  89  -- Compare the two consistency equations (same LHS first term and same RHS)
  90  linarith [hxy, hyx']
  91
  92/-- If the combiner `P` is symmetric and `F` is multiplicatively consistent with `P`,
  93then `F` is reciprocal-symmetric: `F(x) = F(1/x)` for all `x>0`. -/
  94theorem F_symmetric_of_P_symmetric (F : ℝ → ℝ) (P : ℝ → ℝ → ℝ)
  95    (hCons : HasMultiplicativeConsistency F P)
  96    (hSymP : ∀ u v, P u v = P v u) :
  97    IsSymmetric F := by
  98  intro x hx
  99  have h := F_div_swap_of_P_symmetric F P hCons hSymP x 1 hx one_pos
 100  simpa [div_one] using h
 101
 102/-! ## Step 1: Normalization Constrains P -/