def
definition
toZ
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.UnitMapping on GitHub at line 14.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
11def DeltaSub (δ : ℤ) := ℤ
12
13@[simp] def fromZ (δ : ℤ) (n : ℤ) : DeltaSub δ := n
14@[simp] def toZ (δ : ℤ) (p : DeltaSub δ) : ℤ := p
15
16@[simp] lemma toZ_fromZ (δ : ℤ) (hδ : δ ≠ 0) (n : ℤ) :
17 toZ δ (fromZ δ n) = n := rfl
18
19end LedgerUnits
20
21open LedgerUnits
22
23/-- Affine map from ℤ to ℝ: n ↦ slope·n + offset. -/
24structure AffineMapZ where
25 slope : ℝ
26 offset : ℝ
27
28@[simp] def apply (f : AffineMapZ) (n : ℤ) : ℝ := f.slope * (n : ℝ) + f.offset
29
30/-- Map δ-subgroup to ℝ by composing the (stubbed) projection `toZ` with an affine map. -/
31noncomputable def mapDelta (δ : ℤ) (hδ : δ ≠ 0) (f : AffineMapZ) : DeltaSub δ → ℝ :=
32 fun p => f.slope * ((LedgerUnits.toZ δ p) : ℝ) + f.offset
33
34lemma mapDelta_diff (δ : ℤ) (hδ : δ ≠ 0) (f : AffineMapZ)
35 (p q : DeltaSub δ) :
36 mapDelta δ hδ f p - mapDelta δ hδ f q
37 = f.slope * ((LedgerUnits.toZ δ p - LedgerUnits.toZ δ q : ℤ) : ℝ) := by
38 classical
39 calc
40 mapDelta δ hδ f p - mapDelta δ hδ f q
41 = (f.slope * (LedgerUnits.toZ δ p : ℝ) + f.offset)
42 - (f.slope * (LedgerUnits.toZ δ q : ℝ) + f.offset) := by
43 simp [mapDelta]
44 _ = f.slope * (LedgerUnits.toZ δ p : ℝ)