costFamily

formal source

 110    appearing in the broad cost category. On `ℝ_{>0}` this is the full
 111    continuous solution family to the calibrated d'Alembert law before
 112    imposing `κ = 1`. -/
 113noncomputable def costFamily (κ : ℝ) (x : ℝ) : ℝ :=
 114  (x ^ κ + x ^ (-κ)) / 2 - 1
 115
 116/-- The canonical `κ = 1` family recovers the J-cost on positive reals. -/
 117theorem costFamily_one_eq_J {x : ℝ} (hx : 0 < x) : costFamily 1 x = J x := by
 118  unfold costFamily CostAlgebra.J
 119  rw [Real.rpow_one, Real.rpow_neg (le_of_lt hx), Real.rpow_one]
 120  simp [IndisputableMonolith.Cost.Jcost]
 121
 122/-- The family is normalized at `x = 1`. -/
 123theorem costFamily_unit (κ : ℝ) : costFamily κ 1 = 0 := by
 124  unfold costFamily
 125  simp
 126
 127/-- The order-preserving power map on positive reals, written paper-style as
 128    `x ↦ x^α`. -/
 129noncomputable def powerMap (α : ℝ) (x : ℝ) : ℝ := x ^ α
 130
 131/-- The power map preserves positivity on `ℝ_{>0}`. -/
 132theorem powerMap_pos (α : ℝ) {x : ℝ} (hx : 0 < x) :
 133    0 < powerMap α x := by
 134  unfold powerMap
 135  exact Real.rpow_pos_of_pos hx α
 136
 137/-- The power map is multiplicative on positive reals. -/
 138theorem powerMap_mul (α : ℝ) {x y : ℝ} (hx : 0 < x) (hy : 0 < y) :
 139    powerMap α (x * y) = powerMap α x * powerMap α y := by
 140  unfold powerMap
 141  rw [Real.mul_rpow (le_of_lt hx) (le_of_lt hy)]
 142
 143/-- Composing the `κ`-family with the power map multiplies the parameter: