`mapDelta_step`

proved

show as: view math explainer →

module: IndisputableMonolith.UnitMapping
domain: UnitMapping
line: 80 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.UnitMapping on GitHub at line 80.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  77  classical
  78  simp [mapDelta, LedgerUnits.toZ_fromZ δ hδ]
  79
  80lemma mapDelta_step (δ : ℤ) (hδ : δ ≠ 0) (f : AffineMapZ) (n : ℤ) :
  81  mapDelta δ hδ f (LedgerUnits.fromZ δ (n+1)) - mapDelta δ hδ f (LedgerUnits.fromZ δ n) = f.slope := by
  82  classical
  83  calc
  84    mapDelta δ hδ f (LedgerUnits.fromZ δ (n+1))
  85      - mapDelta δ hδ f (LedgerUnits.fromZ δ n)
  86        = (f.slope * ((n+1 : ℤ) : ℝ) + f.offset)
  87            - (f.slope * (n : ℝ) + f.offset) := by
  88              simp [mapDelta, LedgerUnits.toZ_fromZ]
  89    _   = f.slope * ((n+1 : ℤ) : ℝ) - f.slope * (n : ℝ) := by
  90              ring
  91    _   = f.slope * ((n : ℝ) + 1) - f.slope * (n : ℝ) := by
  92              simpa [Int.cast_add, Int.cast_one]
  93    _   = f.slope := by
  94              simp [mul_add, sub_eq_add_neg, add_comm, add_left_comm, add_assoc]
  95
  96@[simp] lemma mapDeltaTime_fromZ (δ : ℤ) (hδ : δ ≠ 0)
  97  (U : Constants.RSUnits) (n : ℤ) :
  98  mapDeltaTime δ hδ U (LedgerUnits.fromZ δ n) = U.tau0 * (n : ℝ) := by
  99  classical
 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 : ℤ) :

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.