log_consistency

formal source

  52/-! ## Consistency in Log-Coordinates -/
  53
  54/-- If F has multiplicative consistency, then G has additive consistency. -/
  55theorem log_consistency (F : ℝ → ℝ) (P : ℝ → ℝ → ℝ)
  56    (hCons : ∀ x y : ℝ, 0 < x → 0 < y → F (x * y) + F (x / y) = P (F x) (F y)) :
  57    ∀ t u : ℝ, G_of F (t + u) + G_of F (t - u) = P (G_of F t) (G_of F u) := by
  58  intro t u
  59  simp only [G_of]
  60  have hpos_t : 0 < Real.exp t := Real.exp_pos t
  61  have hpos_u : 0 < Real.exp u := Real.exp_pos u
  62  have h := hCons (Real.exp t) (Real.exp u) hpos_t hpos_u
  63  simp only [Real.exp_add, Real.exp_sub] at h
  64  convert h using 2
  65  · rw [Real.exp_add]
  66  · rw [Real.exp_sub]
  67
  68/-! ## Boundary Conditions on Q (= P) -/
  69
  70/-- From normalization F(1) = 0, we get G(0) = 0. -/
  71theorem G_zero (F : ℝ → ℝ) (hNorm : F 1 = 0) : G_of F 0 = 0 := by
  72  simp only [G_of, Real.exp_zero, hNorm]
  73
  74/-- From consistency at u = 0: G(t) + G(t) = Q(G(t), 0), so Q(a, 0) = 2a. -/
  75theorem Q_boundary_v (F : ℝ → ℝ) (P : ℝ → ℝ → ℝ)
  76    (hNorm : F 1 = 0)
  77    (hCons : ∀ x y : ℝ, 0 < x → 0 < y → F (x * y) + F (x / y) = P (F x) (F y)) :
  78    ∀ a : ℝ, (∃ t, G_of F t = a) → P a 0 = 2 * a := by
  79  intro a ⟨t, ht⟩
  80  have hlog := log_consistency F P hCons t 0
  81  simp only [add_zero, sub_zero] at hlog
  82  rw [G_zero F hNorm] at hlog
  83  -- hlog : G_of F t + G_of F t = P (G_of F t) 0
  84  rw [← ht]
  85  linarith