LocalComposition

formal source

  36  no_external_scale : ∀ (λ : ℝ), λ > 0 →
  37    ∀ n, levels n / levels (n + 1) = levels 0 / levels 1
  38
  39structure LocalComposition (L : ZeroParameterLedger) where
  40  compose : ℕ → ℝ
  41  compose_from_levels : ∀ k, compose k = L.levels k / L.levels (k + 1)
  42  compose_positive : ∀ k, 0 < compose k
  43
  44structure BinaryRecurrence (L : ZeroParameterLedger) where
  45  ratio : ℝ
  46  ratio_pos : 0 < ratio
  47  recurrence : ∀ k, L.levels (k + 2) = ratio * L.levels (k + 1) + (1 - ratio) * L.levels k
  48  actually_binary : ∀ k, L.levels (k + 2) = ratio * L.levels (k + 1) + (1 - ratio) * L.levels k
  49
  50/-! ## Key Theorems -/
  51
  52theorem ratio_only (L : ZeroParameterLedger) :
  53    ∀ m n : ℕ, L.levels m / L.levels n =
  54      (L.levels 0 / L.levels 1) ^ ((m : ℤ) - n) := by
  55  intro m n
  56  induction m with
  57  | zero =>
  58    induction n with
  59    | zero => simp
  60    | succ n ih =>
  61      have h := L.no_external_scale 1 one_pos n
  62      rw [div_eq_div_iff (ne_of_gt (L.all_positive 0)) (ne_of_gt (L.all_positive (n + 1)))]
  63      have := L.no_external_scale 1 one_pos 0
  64      rw [Nat.zero_add] at this
  65      rw [div_eq_div_iff (ne_of_gt (L.all_positive 0)) (ne_of_gt (L.all_positive 1))] at this
  66      nlinarith [L.all_positive 0, L.all_positive 1, L.all_positive n, L.all_positive (n+1)]
  67  | succ m ih =>
  68    have h := L.no_external_scale 1 one_pos m
  69    rw [div_eq_div_iff (ne_of_gt (L.all_positive (m+1))) (ne_of_gt (L.all_positive n))]