G_zero

formal source

  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
  86
  87/-- Similarly, Q(0, b) = 2b by symmetry (if F is symmetric). -/
  88theorem Q_boundary_u (F : ℝ → ℝ) (P : ℝ → ℝ → ℝ)
  89    (hNorm : F 1 = 0)
  90    (hSymm : ∀ x : ℝ, 0 < x → F x = F x⁻¹)
  91    (hCons : ∀ x y : ℝ, 0 < x → 0 < y → F (x * y) + F (x / y) = P (F x) (F y)) :
  92    ∀ b : ℝ, (∃ u, G_of F u = b) → P 0 b = 2 * b := by
  93  intro b ⟨u, hu⟩
  94  have hlog := log_consistency F P hCons 0 u
  95  simp only [zero_add, zero_sub] at hlog
  96  -- G(-u) = G(u) by symmetry of F
  97  have hGeven : G_of F (-u) = G_of F u := by
  98    simp only [G_of]
  99    rw [Real.exp_neg]
 100    -- F (exp(u)⁻¹) = F (exp(u)) by symmetry
 101    have hsym := hSymm (Real.exp u) (Real.exp_pos u)