def
definition
mapDeltaAction
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.UnitMapping on GitHub at line 72.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
69 mapDelta δ hδ (timeMap U)
70
71/-- Existence of affine δ→action mapping via an explicit ħ parameter. -/
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