yieldGapCost_at_potential

formal source

  34def yieldGapCost (actual_yield potential_yield : ℝ) : ℝ :=
  35  Jcost (actual_yield / potential_yield)
  36
  37theorem yieldGapCost_at_potential (y : ℝ) (h : y ≠ 0) :
  38    yieldGapCost y y = 0 := by
  39  unfold yieldGapCost; rw [div_self h]; exact Jcost_unit0
  40
  41theorem yieldGapCost_nonneg (a p : ℝ) (ha : 0 < a) (hp : 0 < p) :
  42    0 ≤ yieldGapCost a p := by
  43  unfold yieldGapCost; exact Jcost_nonneg (div_pos ha hp)
  44
  45/-- Agronomic tipping point: Ya/Yp = 1/φ. -/
  46def agronomicTipPoint : ℝ := phi⁻¹
  47
  48theorem agronomicTipPoint_pos : 0 < agronomicTipPoint :=
  49  inv_pos.mpr phi_pos
  50
  51theorem agronomicTipPoint_lt_one : agronomicTipPoint < 1 :=
  52  inv_lt_one_of_one_lt₀ one_lt_phi
  53
  54structure YieldGapCert where
  55  cost_at_potential : ∀ y : ℝ, y ≠ 0 → yieldGapCost y y = 0
  56  cost_nonneg : ∀ a p : ℝ, 0 < a → 0 < p → 0 ≤ yieldGapCost a p
  57  tip_pos : 0 < agronomicTipPoint
  58  tip_lt_one : agronomicTipPoint < 1
  59
  60noncomputable def cert : YieldGapCert where
  61  cost_at_potential := yieldGapCost_at_potential
  62  cost_nonneg := yieldGapCost_nonneg
  63  tip_pos := agronomicTipPoint_pos
  64  tip_lt_one := agronomicTipPoint_lt_one
  65
  66theorem cert_inhabited : Nonempty YieldGapCert := ⟨cert⟩
  67