pith. machine review for the scientific record. sign in
theorem proved term proof

substitutivity_from_ledger

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  23theorem substitutivity_from_ledger
  24    (L : ZeroParameterComparisonLedger)
  25    (x₁ x₂ y : ℝ) (hx₁ : 0 < x₁) (hx₂ : 0 < x₂)
  26    (hJ_eq : L.cost.J x₁ = L.cost.J x₂) (hy : 0 < y) :
  27    L.cost.J (x₁ * y) + L.cost.J (x₁ / y) =
  28    L.cost.J (x₂ * y) + L.cost.J (x₂ / y) :=

proof body

Term-mode proof.

  29  L.cost_sufficient x₁ x₂ y hx₁ hx₂ hJ_eq hy
  30
  31/-- `λ = 1` is the unique positive real satisfying `λ = λ⁻¹`. -/

depends on (9)

Lean names referenced from this declaration's body.