MultIndex

formal source

  57
  58/-- Index for the multiplicative group `ℚ_{>0}^×`: a finitely-supported
  59    function from primes to integers. -/
  60abbrev MultIndex : Type := Nat.Primes →₀ ℤ
  61
  62/-- The positive rational corresponding to a multiplicative index,
  63    interpreted as a real number: `toRat v = ∏ p^(v p)`. -/
  64def toRat (v : MultIndex) : ℝ :=
  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)]