theorem
proved
H_at_one
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Algebra.CostAlgebra on GitHub at line 191.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
188noncomputable def H (x : ℝ) : ℝ := J x + 1
189
190/-- H at identity equals 1. -/
191theorem H_at_one : H 1 = 1 := by
192 unfold H; rw [J_at_one]; ring
193
194/-- **THEOREM: H satisfies the standard d'Alembert equation.**
195 H(xy) + H(x/y) = 2·H(x)·H(y)
196
197 This is the canonical form of the multiplicative d'Alembert
198 functional equation, whose unique continuous solution is cosh. -/
199theorem H_dAlembert (x y : ℝ) (hx : 0 < x) (hy : 0 < y) :
200 H (x * y) + H (x / y) = 2 * H x * H y := by
201 unfold H J
202 have rcl := RCL_holds x y hx hy
203 have hsum :
204 Jcost (x * y) + Jcost (x / y) + 2 =
205 2 * Jcost x * Jcost y + 2 * Jcost x + 2 * Jcost y + 2 := by
206 have h' := congrArg (fun z : ℝ => z + 2) rcl
207 simpa [add_assoc, add_left_comm, add_comm] using h'
208 have hmul :
209 2 * (Jcost x + 1) * (Jcost y + 1) =
210 2 * Jcost x * Jcost y + 2 * Jcost x + 2 * Jcost y + 2 := by
211 ring
212 calc
213 Jcost (x * y) + 1 + (Jcost (x / y) + 1)
214 = Jcost (x * y) + Jcost (x / y) + 2 := by ring
215 _ = 2 * Jcost x * Jcost y + 2 * Jcost x + 2 * Jcost y + 2 := hsum
216 _ = 2 * (Jcost x + 1) * (Jcost y + 1) := hmul.symm
217
218/-! ## §4a. The Shifted Monoid on `[1/2, ∞)` -/
219
220/-- The carrier of the shifted monoid from Theorem 2.7:
221 real values bounded below by `1/2`. -/