`forced_of_factorization`

proved

show as: view math explainer →

module: IndisputableMonolith.Cost.Ndim.Uniqueness
domain: Cost
line: 33 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Cost.Ndim.Uniqueness on GitHub at line 33.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  30    _ = JcostN α x := by simp [JcostN_eq_Jcost_aggregate]
  31
  32/-- Existential version of the forcing theorem. -/
  33theorem forced_of_factorization {n : ℕ}
  34    (F : Vec n → ℝ) (α : Vec n)
  35    (hfac : FactorsThrough F α)
  36    (hscalar_unique : ∀ G : ℝ → ℝ,
  37      (∀ x : Vec n, F x = G (aggregate α x)) →
  38      (∀ {u : ℝ}, 0 < u → G u = Jcost u)) :
  39    ∀ x : Vec n, F x = JcostN α x := by
  40  rcases hfac with ⟨G, hG⟩
  41  exact forced_of_scalar_uniqueness F α G hG (hscalar_unique G hG)
  42
  43end Ndim
  44end Cost
  45end IndisputableMonolith

papers checked against this theorem

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