forced_of_scalar_uniqueness

formal source

  18  ∃ G : ℝ → ℝ, ∀ x : Vec n, F x = G (aggregate α x)
  19
  20/-- Main forcing theorem: scalar uniqueness forces the `n`-dimensional lift. -/
  21theorem forced_of_scalar_uniqueness {n : ℕ}
  22    (F : Vec n → ℝ) (α : Vec n) (G : ℝ → ℝ)
  23    (hfactor : ∀ x : Vec n, F x = G (aggregate α x))
  24    (hscalar : ∀ {u : ℝ}, 0 < u → G u = Jcost u) :
  25    ∀ x : Vec n, F x = JcostN α x := by
  26  intro x
  27  calc
  28    F x = G (aggregate α x) := hfactor x
  29    _ = Jcost (aggregate α x) := hscalar (aggregate_pos α x)
  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