lemma
proved
mapDeltaAction_step
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.UnitMapping on GitHub at line 116.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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