lemma
proved
mapDeltaAction_fromZ
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.UnitMapping on GitHub at line 109.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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