costAt

formal source

  65  v.prod (fun p k => (p.val : ℝ) ^ (k : ℤ))
  66
  67/-- The cost evaluated at the rational represented by `v`. -/
  68def costAt (v : MultIndex) : ℝ := Jcost (toRat v)
  69
  70@[simp] theorem toRat_zero : toRat (0 : MultIndex) = 1 := by
  71  simp [toRat]
  72
  73theorem toRat_pos (v : MultIndex) : 0 < toRat v := by
  74  unfold toRat
  75  rw [Finsupp.prod]
  76  apply Finset.prod_pos
  77  intro p _
  78  apply zpow_pos
  79  exact_mod_cast p.prop.pos
  80
  81theorem toRat_add (v w : MultIndex) :
  82    toRat (v + w) = toRat v * toRat w := by
  83  unfold toRat
  84  rw [Finsupp.prod_add_index]
  85  · intro p _
  86    simp
  87  · intro p _ k₁ k₂
  88    rw [zpow_add₀ (by
  89      have hp : p.val ≠ 0 := Nat.Prime.ne_zero p.prop
  90      exact_mod_cast hp)]
  91
  92theorem toRat_neg (v : MultIndex) : toRat (-v) = (toRat v)⁻¹ := by
  93  have h_sum : toRat ((-v) + v) = toRat (-v) * toRat v := toRat_add (-v) v
  94  have h_zero : ((-v) + v) = (0 : MultIndex) := by simp
  95  rw [h_zero, toRat_zero] at h_sum
  96  have hv_pos : 0 < toRat v := toRat_pos v
  97  have hv_ne : toRat v ≠ 0 := ne_of_gt hv_pos
  98  field_simp [hv_ne]