mapDeltaTime_step

formal source

 100  have h := mapDelta_fromZ (δ:=δ) (hδ:=hδ) (f:=timeMap U) (n:=n)
 101  simpa [mapDeltaTime, timeMap, add_comm] using h
 102
 103lemma mapDeltaTime_step (δ : ℤ) (hδ : δ ≠ 0)
 104  (U : Constants.RSUnits) (n : ℤ) :
 105  mapDeltaTime δ hδ U (LedgerUnits.fromZ δ (n+1)) - mapDeltaTime δ hδ U (LedgerUnits.fromZ δ n) = U.tau0 := by
 106  simpa [mapDeltaTime, timeMap] using
 107    (mapDelta_step (δ:=δ) (hδ:=hδ) (f:=timeMap U) (n:=n))
 108
 109@[simp] lemma mapDeltaAction_fromZ (δ : ℤ) (hδ : δ ≠ 0)
 110  (hbar : ℝ) (n : ℤ) :
 111  mapDeltaAction δ hδ hbar (LedgerUnits.fromZ δ n) = hbar * (n : ℝ) := by
 112  classical
 113  have h := mapDelta_fromZ (δ:=δ) (hδ:=hδ) (f:=actionMap hbar) (n:=n)
 114  simpa [mapDeltaAction, actionMap, add_comm] using h
 115
 116lemma mapDeltaAction_step (δ : ℤ) (hδ : δ ≠ 0)
 117  (hbar : ℝ) (n : ℤ) :
 118  mapDeltaAction δ hδ hbar (LedgerUnits.fromZ δ (n+1)) - mapDeltaAction δ hδ hbar (LedgerUnits.fromZ δ n)
 119    = hbar := by
 120  simpa [mapDeltaAction, actionMap] using
 121    (mapDelta_step (δ:=δ) (hδ:=hδ) (f:=actionMap hbar) (n:=n))
 122
 123lemma mapDelta_diff_toZ (δ : ℤ) (hδ : δ ≠ 0) (f : AffineMapZ)
 124  (p q : DeltaSub δ) :
 125  mapDelta δ hδ f p - mapDelta δ hδ f q
 126    = f.slope * ((LedgerUnits.toZ δ p - LedgerUnits.toZ δ q : ℤ) : ℝ) := by
 127  classical
 128  simpa using (mapDelta_diff (δ:=δ) (hδ:=hδ) (f:=f) (p:=p) (q:=q))
 129
 130end UnitMapping
 131end IndisputableMonolith