toRat_add

formal source

  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]
  99  linarith [h_sum]
 100
 101/-- Reciprocal symmetry of `J` at the index level: `J(1/q) = J(q)`. -/
 102theorem costAt_neg_eq (v : MultIndex) : costAt (-v) = costAt v := by
 103  unfold costAt
 104  rw [toRat_neg]
 105  exact (Jcost_symm (toRat_pos v)).symm
 106
 107/-! ## The state space: free ℝ-module on `MultIndex` -/
 108
 109/-- The pre-Hilbert space: free `ℝ`-module on `MultIndex`. -/
 110abbrev StateSpace : Type := MultIndex →₀ ℝ
 111