toRat_neg

formal source

  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
 112/-! ## The three operators
 113
 114We use `Finsupp.lsum` and similar mathlib constructions to define
 115linear endomorphisms of `StateSpace`.  The "basis vector" `e_v` is
 116`Finsupp.single v 1`. -/
 117
 118/-- The diagonal cost operator `D`: maps `e_v` to `J(toRat v) · e_v`.
 119
 120    Defined as the linear map sending each basis element `e_v` to
 121    `costAt v • e_v`. -/
 122def diagOp : StateSpace →ₗ[ℝ] StateSpace :=