pith. machine review for the scientific record. sign in
theorem

washburn_uniqueness_aczel

proved
show as:
view math explainer →

Reciprocal-symmetric cost has one solution: J(x) = ½(x + x⁻¹) − 1.

module
IndisputableMonolith.Cost.FunctionalEquation
domain
Cost
line
1076 · github
papers citing
6004 papers (below)

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Cost.FunctionalEquation on GitHub at line 1076.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

Derivations using this theorem

depends on

used by

formal source

1073
1074    This version uses the global Aczél axiom internally and requires NO regularity
1075    hypothesis parameters from the caller. -/
1076theorem washburn_uniqueness_aczel (F : ℝ → ℝ)
1077    [AczelSmoothnessPackage]
1078    (hRecip : IsReciprocalCost F)
1079    (hNorm : IsNormalized F)
1080    (hComp : SatisfiesCompositionLaw F)
1081    (hCalib : IsCalibrated F)
1082    (hCont : ContinuousOn F (Set.Ioi 0)) :
1083    ∀ x : ℝ, 0 < x → F x = Cost.Jcost x := by
1084  intro x hx
1085  have hSymm : ∀ {y}, 0 < y → F y = F y⁻¹ := fun {y} hy => hRecip y hy
1086  have hCoshAdd : CoshAddIdentity F := composition_law_equiv_coshAdd F |>.mp hComp
1087  let Gf : ℝ → ℝ := G F
1088  let Hf : ℝ → ℝ := H F
1089  have h_G0 : Gf 0 = 0 := G_zero_of_unit F hNorm
1090  have h_H0 : Hf 0 = 1 := by
1091    show H F 0 = 1
1092    simp only [H, G, Real.exp_zero]
1093    rw [hNorm]; ring
1094  have h_G_cont : Continuous Gf := by
1095    have h := ContinuousOn.comp_continuous hCont continuous_exp
1096    have h' : Continuous (fun t => F (Real.exp t)) :=
1097      h (by intro t; exact Set.mem_Ioi.mpr (Real.exp_pos t))
1098    simp [Gf, G] at h'
1099    exact h'
1100  have h_H_cont : Continuous Hf := by
1101    simpa [Hf, H] using h_G_cont.add continuous_const
1102  have h_direct : DirectCoshAdd Gf := CoshAddIdentity_implies_DirectCoshAdd F hCoshAdd
1103  have h_dAlembert : ∀ t u, Hf (t + u) + Hf (t - u) = 2 * Hf t * Hf u := by
1104    intro t u
1105    have hG := h_direct t u
1106    have h_goal : (Gf (t + u) + 1) + (Gf (t - u) + 1) = 2 * (Gf t + 1) * (Gf u + 1) := by