`P_uniqueness`

proved

show as: view math explainer →

module: IndisputableMonolith.Foundation.DAlembert.Unconditional
domain: Foundation
line: 215 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.DAlembert.Unconditional on GitHub at line 215.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

 212
 213/-- If any P satisfies the consistency equation with J, it must be the RCL.
 214    This rules out ALL alternatives, polynomial or not. -/
 215theorem P_uniqueness (P Q : ℝ → ℝ → ℝ)
 216    (hP : ∀ x y : ℝ, 0 < x → 0 < y →
 217      Cost.Jcost (x * y) + Cost.Jcost (x / y) = P (Cost.Jcost x) (Cost.Jcost y))
 218    (hQ : ∀ x y : ℝ, 0 < x → 0 < y →
 219      Cost.Jcost (x * y) + Cost.Jcost (x / y) = Q (Cost.Jcost x) (Cost.Jcost y)) :
 220    ∀ u v : ℝ, 0 ≤ u → 0 ≤ v → P u v = Q u v := by
 221  intro u v hu hv
 222  have hP' := rcl_unconditional P hP u v hu hv
 223  have hQ' := rcl_unconditional Q hQ u v hu hv
 224  rw [hP', hQ']
 225
 226end Unconditional
 227end DAlembert
 228end Foundation
 229end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.