`toRat`

definition

show as: view math explainer →

module: IndisputableMonolith.NumberTheory.HilbertPolyaCandidate
domain: NumberTheory
line: 64 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.NumberTheory.HilbertPolyaCandidate on GitHub at line 64.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  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)]
  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.