def
definition
mapDeltaTime
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.UnitMapping on GitHub at line 68.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
of -
RSUnits -
U -
Constants -
via -
of -
of -
of -
of -
DeltaSub -
U -
DeltaSub -
mapDelta -
timeMap -
RSUnits -
DeltaSub -
mapDelta -
timeMap
used by
formal source
65 mapDelta δ hδ (chargeMap qe)
66
67/-- Existence of affine δ→time mapping via τ0. -/
68noncomputable def mapDeltaTime (δ : ℤ) (hδ : δ ≠ 0) (U : Constants.RSUnits) : DeltaSub δ → ℝ :=
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