  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)
  42            - (f.slope * (LedgerUnits.toZ δ q : ℝ) + f.offset) := by
  43              simp [mapDelta]
  44    _   = f.slope * (LedgerUnits.toZ δ p : ℝ)
  45            - f.slope * (LedgerUnits.toZ δ q : ℝ) := by
  46              ring
  47    _   = f.slope * ((LedgerUnits.toZ δ p : ℝ)
  48            - (LedgerUnits.toZ δ q : ℝ)) := by
  49              simpa [mul_sub]
  50    _   = f.slope * ((LedgerUnits.toZ δ p - LedgerUnits.toZ δ q : ℤ) : ℝ) := by
  51              have hcast : ((LedgerUnits.toZ δ p - LedgerUnits.toZ δ q : ℤ) : ℝ)
  52                  = (LedgerUnits.toZ δ p : ℝ) - (LedgerUnits.toZ δ q : ℝ) := by
  53                    simpa using (Int.cast_sub (LedgerUnits.toZ δ p) (LedgerUnits.toZ δ q))
  54              simpa [hcast]

papers checked against this theorem

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