lemma
proved
mapDelta_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 75.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
72noncomputable def mapDeltaAction (δ : ℤ) (hδ : δ ≠ 0) (hbar : ℝ) : DeltaSub δ → ℝ :=
73 mapDelta δ hδ (actionMap hbar)
74
75@[simp] lemma mapDelta_fromZ (δ : ℤ) (hδ : δ ≠ 0) (f : AffineMapZ) (n : ℤ) :
76 mapDelta δ hδ f (LedgerUnits.fromZ δ n) = f.slope * (n : ℝ) + f.offset := by
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