timeMap

formal source

 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))
 179    - mapDeltaOne LedgerUnits.toZ_one f (LedgerUnits.fromZ_one n) = f.slope := by
 180  simp [mapDeltaOne, add_comm, add_left_comm, add_assoc, sub_eq_add_neg, mul_add]
 181
 182@[simp] lemma mapDeltaTime_fromZ_one
 183  (U : Constants.RSUnits) (n : ℤ) :
 184  mapDeltaOne LedgerUnits.toZ_one (timeMap U) (LedgerUnits.fromZ_one n)
 185    = U.tau0 * (n : ℝ) := by