mapDelta

formal source

 145@[simp] def apply (f : AffineMapZ) (n : ℤ) : ℝ := f.slope * (n : ℝ) + f.offset
 146
 147/-- Map δ-subgroup to ℝ by composing an affine map with a provided projection to ℤ. -/
 148noncomputable def mapDelta (δ : ℤ) (hδ : δ ≠ 0)
 149  (toZ : {x : ℤ // ∃ n : ℤ, x = n * δ} → ℤ) (f : AffineMapZ) :
 150  {x : ℤ // ∃ n : ℤ, x = n * δ} → ℝ :=
 151  fun p => f.slope * ((toZ p) : ℝ) + f.offset
 152
 153/-- Context constructors: charge (quantum `qe`), time (τ0), and action (ħ). -/
 154@[simp] def chargeMap (qe : ℝ) : AffineMapZ := { slope := qe, offset := 0 }
 155@[simp] def timeMap (U : Constants.RSUnits) : AffineMapZ := { slope := U.tau0, offset := 0 }
 156-- actionMap omitted in minimal RSUnits (no `hbar` field)
 157
 158@[simp] lemma apply_chargeMap (qe : ℝ) (n : ℤ) :
 159  apply (chargeMap qe) n = qe * (n : ℝ) := by simp [apply, chargeMap]
 160
 161@[simp] lemma apply_timeMap (U : Constants.RSUnits) (n : ℤ) :
 162  apply (timeMap U) n = U.tau0 * (n : ℝ) := by simp [apply, timeMap]
 163
 164-- (no actionMap in minimal RSUnits)
 165
 166/-- Specialization of `mapDelta` to δ = 1 using the canonical projection. -/
 167noncomputable def mapDeltaOne
 168  (toZ : LedgerUnits.DeltaSub 1 → ℤ) (f : AffineMapZ) : LedgerUnits.DeltaSub 1 → ℝ :=
 169  fun p => f.slope * ((toZ p) : ℝ) + f.offset
 170
 171@[simp] lemma mapDeltaOne_fromZ_one
 172  (f : AffineMapZ) (n : ℤ) :
 173  mapDeltaOne LedgerUnits.toZ_one f (LedgerUnits.fromZ_one n)
 174    = f.slope * (n : ℝ) + f.offset := by
 175  simp [mapDeltaOne, LedgerUnits.toZ_one, LedgerUnits.fromZ_one]
 176
 177lemma mapDeltaOne_step (f : AffineMapZ) (n : ℤ) :
 178  mapDeltaOne LedgerUnits.toZ_one f (LedgerUnits.fromZ_one (n+1))