Documentation

Projects.DigitalRoot.Time

structure DigitalRoot.Time :

hour : Fin 24
minute : Fin 60

Instances For

@[instance_reducible]

instance DigitalRoot.instInhabitedTime :

Equations

DigitalRoot.instInhabitedTime = { default := DigitalRoot.instInhabitedTime.default }

@[instance_reducible]

instance DigitalRoot.instDecidableEqTime :

DecidableEq Time

Equations

DigitalRoot.instDecidableEqTime = DigitalRoot.instDecidableEqTime.decEq

def DigitalRoot.instDecidableEqTime.decEq (x✝ x✝¹ : Time) :

Decidable (x✝ = x✝¹)

Equations

DigitalRoot.instDecidableEqTime.decEq { hour := a, minute := a_1 } { hour := b, minute := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

Instances For

@[instance_reducible]

instance DigitalRoot.instFintypeTime :

Equations

DigitalRoot.instFintypeTime = Fintype.ofEquiv ((_ : Fin 24) × Fin 60) DigitalRoot.Time.proxyTypeEquiv

@[instance_reducible]

instance DigitalRoot.instHashableTime :

Equations

DigitalRoot.instHashableTime = { hash := DigitalRoot.instHashableTime.hash }

def DigitalRoot.instHashableTime.hash :

Time → UInt64

Equations

DigitalRoot.instHashableTime.hash { hour := a, minute := a_1 } = mixHash (mixHash 0 (hash a)) (hash a_1)

Instances For

def DigitalRoot.Time.toList (t : Time) :

Equations

t.toList = [↑t.hour, ↑t.minute]

Instances For

def DigitalRoot.timeSet :

Equations

DigitalRoot.timeSet = Set'.univ

Instances For

def DigitalRoot.digRootTime (b : ℕ) (t : Time) :

Equations

DigitalRoot.digRootTime b t = DigitalRoot.digRootList b t.toList

Instances For

def DigitalRoot.freqTimeCount (b d : ℕ) :

Equations

DigitalRoot.freqTimeCount b d = DigitalRoot.timeSet.count fun (x : DigitalRoot.Time) => decide (DigitalRoot.digRootTime b x = d)

Instances For

noncomputable def DigitalRoot.freqTimeDig (b : ℕ) :

Equations

DigitalRoot.freqTimeDig b = choose? fun (d : ℕ) => d ≤ b ∧ ∀ (d' : ℕ), d' ≠ d → DigitalRoot.freqTimeCount b d' < DigitalRoot.freqTimeCount b d

Instances For

def DigitalRoot.freqTimeDigFn (b : ℕ) (mp : Map ℕ ℕ) (t : Time) :

Equations

DigitalRoot.freqTimeDigFn b mp t = mp.push (DigitalRoot.digRootTime b t)

Instances For

@[simp]

theorem DigitalRoot.Time.toList_mk {hour : Fin 24} {minute : Fin 60} :

{ hour := hour, minute := minute }.toList = [↑hour, ↑minute]

@[simp]

theorem DigitalRoot.digRootTime_mk {b : ℕ} [hb : b.Base] {hour : Fin 24} {minute : Fin 60} :

digRootTime b { hour := hour, minute := minute } = digRoot b (↑hour + ↑minute)

@[simp]

theorem DigitalRoot.digRootTime_lt_base {b : ℕ} [hb : b.Base] {n : Time} :

digRootTime b n < b

@[simp]

theorem DigitalRoot.digRootTime_le_base {b : ℕ} {n : Time} :

digRootTime b n ≤ b

theorem DigitalRoot.freqTimeDigFn_freqTimeDigFn_comm {b : ℕ} {mp : Map ℕ ℕ} {t₁ t₂ : Time} :

freqTimeDigFn b (freqTimeDigFn b mp t₁) t₂ = freqTimeDigFn b (freqTimeDigFn b mp t₂) t₁

def DigitalRoot.freqTimeMp (b : ℕ) :

Equations

DigitalRoot.freqTimeMp b = DigitalRoot.timeSet.fold (DigitalRoot.freqTimeDigFn b) ∅ ⋯

Instances For

def DigitalRoot.freqTimeDig' (b : ℕ) :

Equations

DigitalRoot.freqTimeDig' b = match (DigitalRoot.freqTimeMp b).toList.mergeSort fun (a b : ℕ × ℕ) => decide (b.2 ≤ a.2) with | (d₁, c₁) :: (fst, c₂) :: tail => do guard (c₁ ≠ c₂) pure d₁ | x => none

Instances For

@[simp]

theorem DigitalRoot.exi_digRootTime_eq_iff {n : ℕ} :

(∃ (k : Time), digRootTime 10 k = n) ↔ n < 10

@[simp]

theorem DigitalRoot.mem_freqTimeMp {d : ℕ} :

d ∈ freqTimeMp 10 ↔ d < 10

theorem DigitalRoot.get?_freqTimeMp_eq {d : ℕ} (hd : d < 10) :

Map.get? d (freqTimeMp 10) = some (freqTimeCount 10 d)

theorem DigitalRoot.freqTimeMp_eq :

freqTimeMp 10 = (Set'.ofFinset (Finset.range 10)).toMap fun (d : ℕ) => freqTimeCount 10 d

theorem DigitalRoot.freqTimeCount_eq_zero_of_base_le {b : ℕ} [hb : b.Base] {n : ℕ} (h : b ≤ n) :

freqTimeCount b n = 0

@[simp]

theorem DigitalRoot.freqTimeCount_base_eq_zero {b : ℕ} [hb : b.Base] :

freqTimeCount b b = 0

@[simp]

theorem DigitalRoot.freqTimeCount_base_add_eq_zero {b : ℕ} [hb : b.Base] {n : ℕ} :

freqTimeCount b (b + n) = 0

theorem DigitalRoot.freqTimeDig'_eq_some_of_freqTimeDig_eq_some {d : ℕ} (h : freqTimeDig 10 = some d) :

freqTimeDig' 10 = some d

@[simp]

theorem DigitalRoot.freqTimeCount_eq_zero_iff {n : ℕ} :

freqTimeCount 10 n = 0 ↔ 10 ≤ n

@[simp]

theorem DigitalRoot.freqTimeCount_pos_iff {n : ℕ} :

0 < freqTimeCount 10 n ↔ n < 10

theorem DigitalRoot.freqTimeDig_eq_some_of_freqTimeDig'_eq_some {d : ℕ} (h : freqTimeDig' 10 = some d) :

freqTimeDig 10 = some d

theorem DigitalRoot.freqTimeDig_eq_freqTimeDig' :

freqTimeDig 10 = freqTimeDig' 10

theorem DigitalRoot.freqTimeDig_10_eq_some_5 :

freqTimeDig 10 = some 5

theorem DigitalRoot.toList_freqTimeMp_eq :

(freqTimeMp 10).toList = (List.range 10).zip [1, 159, 159, 160, 161, 162, 161, 160, 159, 158]

theorem DigitalRoot.sum_freqTimeMp_eq_24_mul_60 :

(List.map (fun (x : ℕ × ℕ) => x.2) (freqTimeMp 10).toList).sum = 24 * 60