lambdaA_ne_zero

formal source

  97lemma kappaA_pos : 0 < kappaA := by
  98  unfold kappaA; simpa using Constants.phi_pos
  99
 100lemma lambdaA_ne_zero : lambdaA ≠ 0 := by
 101  have hpos : 0 < Constants.phi := Constants.phi_pos
 102  have hne1 : Constants.phi ≠ 1 := Constants.phi_ne_one
 103  simpa [lambdaA] using Real.log_ne_zero_of_pos_of_ne_one hpos hne1
 104
 105lemma kappaA_ne_zero : kappaA ≠ 0 := by
 106  simpa [kappaA] using Constants.phi_ne_zero
 107
 108/-! Ledger units (δ subgroup) -/
 109namespace LedgerUnits
 110
 111/-- The subgroup of ℤ generated by δ. We specialize to δ = 1 for a clean order isomorphism. -/
 112def DeltaSub (δ : ℤ) := {x : ℤ // ∃ n : ℤ, x = n * δ}
 113
 114/-- Embed ℤ into the δ=1 subgroup. -/
 115def fromZ_one (n : ℤ) : DeltaSub 1 := ⟨n, by exact ⟨n, by simpa using (Int.mul_one n)⟩⟩
 116
 117/-- Project from the δ=1 subgroup back to ℤ by taking its value. -/
 118def toZ_one (p : DeltaSub 1) : ℤ := p.val
 119
 120@[simp] lemma toZ_fromZ_one (n : ℤ) : toZ_one (fromZ_one n) = n := rfl
 121
 122@[simp] lemma fromZ_toZ_one (p : DeltaSub 1) : fromZ_one (toZ_one p) = p := by
 123  cases p with
 124  | mk x hx =>
 125    apply Subtype.ext
 126    rfl
 127
 128/-- Explicit equivalence between the δ=1 subgroup and ℤ (mapping n·1 ↦ n). -/
 129def equiv_delta_one : DeltaSub 1 ≃ ℤ :=
 130{ toFun := toZ_one