DeltaSub

formal source

   8namespace LedgerUnits
   9
  10/-- Subgroup generated by δ (abstract placeholder using integers for mapping only). -/
  11def DeltaSub (δ : ℤ) := ℤ
  12
  13@[simp] def fromZ (δ : ℤ) (n : ℤ) : DeltaSub δ := n
  14@[simp] def toZ   (δ : ℤ) (p : DeltaSub δ) : ℤ := p
  15
  16@[simp] lemma toZ_fromZ (δ : ℤ) (hδ : δ ≠ 0) (n : ℤ) :
  17  toZ δ (fromZ δ n) = n := rfl
  18
  19end LedgerUnits
  20
  21open LedgerUnits
  22
  23/-- Affine map from ℤ to ℝ: n ↦ slope·n + offset. -/
  24structure AffineMapZ where
  25  slope : ℝ
  26  offset : ℝ
  27
  28@[simp] def apply (f : AffineMapZ) (n : ℤ) : ℝ := f.slope * (n : ℝ) + f.offset
  29
  30/-- Map δ-subgroup to ℝ by composing the (stubbed) projection `toZ` with an affine map. -/
  31noncomputable def mapDelta (δ : ℤ) (hδ : δ ≠ 0) (f : AffineMapZ) : DeltaSub δ → ℝ :=
  32  fun p => f.slope * ((LedgerUnits.toZ δ p) : ℝ) + f.offset
  33
  34lemma mapDelta_diff (δ : ℤ) (hδ : δ ≠ 0) (f : AffineMapZ)
  35  (p q : DeltaSub δ) :
  36  mapDelta δ hδ f p - mapDelta δ hδ f q
  37    = f.slope * ((LedgerUnits.toZ δ p - LedgerUnits.toZ δ q : ℤ) : ℝ) := by
  38  classical
  39  calc
  40    mapDelta δ hδ f p - mapDelta δ hδ f q
  41        = (f.slope * (LedgerUnits.toZ δ p : ℝ) + f.offset)