CLRS-Lean
Chapters 1–35 · CLRS Fourth Edition
Chapter 4. Divide-and-Conquer
4.6. Proof of the Continuous Master Theorem

Imports

import CLRSLean.Chapter_04.Section_04_6_Master_Theorem_All_Input

open Finsetopen scoped BigOperators

4.6. Proof of the Continuous Master Theorem

The continuous master theorem (CLRS §4.6) treats the divide-and-conquer recurrence T(n) = a T(n/b) + f(n) with exact division n/b. Unrolling the recurrence to the bottom of the recursion tree expresses the work as the geometric sum

  T(b^k) = Θ(1) + Σ_{j = 0}^{k - 1} a^j · f(b^(k - j))

whose three textbook cases are governed by the ratio r = a / b^p when the forcing is polynomial f(n) = n^p. This section formalizes the analytic core — the real geometric series — and the three continuous cases, then bridges the continuous scale back to the discrete comparison scales used by the all-input Master-theorem wrappers.

Main results:

Definition geomSum: the real geometric partial sum Σ_{j<k} r^j.
Theorem geomSum_le_of_lt_one: a ratio 0 ≤ r < 1 yields a partial sum bounded independently of the number of terms.
Theorem geomSum_eq_of_one: a ratio r = 1 yields exactly k terms.
Theorem geomSum_bigTheta_of_gt_one: a ratio r > 1 yields a geometric tail Θ(r^k).
Definition continuousWork: the recursion-tree work Σ_{j<k} a^j (b^(k-j))^p with polynomial forcing.
Theorem continuousWork_eq_geomSum: the work equals b^(p·k) · geomSum (a / b^p) k.
Theorems continuous_master_case1, continuous_master_case2, and continuous_master_case3: the three continuous cases.
Theorem continuous_case1_scale_eq_criticalPowerScale: the continuous case-1 scale equals the discrete critical-power scale on exact powers.

Status: proved for the continuous geometric-series core and its bridge to the discrete comparison scales. Floors, ceilings, and the non-polynomial forcing of the full all-input transfer remain in CLRSLean.Chapter_04.Section_04_6_Master_Theorem_All_Input.

Notation conventions used in this section:

a : number of subproblems
b : factor by which the subproblem size shrinks
p : exponent of the polynomial forcing f(n) = n^p
k : continuous level count (so n = b^k)

namespace CLRSnamespace Chapter04

The real geometric series

The real geometric partial sum Σ_{j ∈ range k} r^j.

noncomputable def geomSum (r : ℝ) (k : ℕ) : ℝ :=
  ∑ j ∈ range k, r ^ j

A geometric partial sum with a nonnegative ratio is nonnegative.


theorem geomSum_nonneg {r : ℝ} (hr0 : 0 ≤ r) (k : ℕ) : 0 ≤ geomSum r k := by
  rw [geomSum]
  exact Finset.sum_nonneg (by intro j hj; exact pow_nonneg hr0 j)

Continuous master theorem, case-1 ratio. For a ratio 0 ≤ r < 1 the partial sum is bounded by (1 - r)⁻¹, independently of the number of terms. This is the analytic reason the forcing in the third Master case (whose ratio is smaller than one) contributes only Θ(f(n)) rather than growing with the recursion tree.


theorem geomSum_le_of_lt_one {r : ℝ} (hr0 : 0 ≤ r) (hr1 : r < 1) (k : ℕ) :
    geomSum r k ≤ (1 - r)⁻¹ := by
  have hr_ne : r ≠ 1 := by linarith
  have hpos : 0 < 1 - r := by linarith
  rw [geomSum, geom_sum_eq hr_ne]
  have hrk_nonneg : 0 ≤ r ^ k := pow_nonneg hr0 _
  have hnum : 1 - r ^ k ≤ 1 := by linarith
  have hdiv : (1 - r ^ k) / (1 - r) ≤ 1 / (1 - r) :=
    (div_le_div_iff_of_pos_right hpos).mpr hnum
  have hcast : (r ^ k - 1) / (r - 1) = (1 - r ^ k) / (1 - r) := by
    field_simp [ne_of_gt hpos]
    ring
  rw [hcast]
  rw [inv_eq_one_div]
  exact hdiv

Continuous master theorem, case-2 ratio. For a ratio r = 1 the partial sum has exactly k unit terms, the logarithmic factor in the second Master case.


theorem geomSum_eq_of_one (k : ℕ) : geomSum 1 k = (k : ℝ) := by
  rw [geomSum]
  simp only [one_pow, Finset.sum_const, Finset.card_range, nsmul_eq_mul, mul_one]

For a ratio r > 1 the partial sum is at most a constant times its last term r^k.


theorem geomSum_le_geometric_of_gt_one {r : ℝ} (hr1 : 1 < r) (k : ℕ) :
    geomSum r k ≤ (r - 1)⁻¹ * r ^ k := by
  have hr_ne : r ≠ 1 := by linarith
  rw [geomSum, geom_sum_eq hr_ne]
  calc
    (r ^ k - 1) / (r - 1) ≤ r ^ k / (r - 1) :=
      (div_le_div_iff_of_pos_right (sub_pos.mpr hr1)).mpr (by linarith)
    _ = (r - 1)⁻¹ * r ^ k := by
      rw [div_eq_mul_inv]
      ring

For a ratio r > 1 and a nonempty partial sum, the sum is at least a constant times its last term r^k.


theorem geometric_le_geomSum_of_gt_one {r : ℝ} (hr1 : 1 < r) {k : ℕ} (hk : 1 ≤ k) :
    (r : ℝ)⁻¹ * r ^ k ≤ geomSum r k := by
  have hr_pos : 0 < r := lt_trans zero_lt_one hr1
  have hlast : r ^ (k - 1) ≤ geomSum r k := by
    rw [geomSum]
    exact Finset.single_le_sum (by intro j hj; exact pow_nonneg hr_pos.le j)
      (by rw [mem_range]; omega)
  have hfac : (r : ℝ)⁻¹ * r ^ k = r ^ (k - 1) := by
    field_simp [ne_of_gt hr_pos]
    rw [mul_comm, ← pow_succ]
    rw [show (k - 1) + 1 = k by omega]
  rw [hfac]
  exact hlast

Continuous master theorem, case-3 ratio. For a ratio r > 1 the partial sum is Θ(r^k), dominated by its largest (last) term. This is the analytic reason the forcing in the first Master case (whose ratio exceeds one) grows to Θ(n^(log_b a)).


theorem geomSum_bigTheta_of_gt_one {r : ℝ} (hr1 : 1 < r) :
    Chapter03.isBigTheta (geomSum r) (fun k => r ^ k) := by
  have hr_pos : 0 < r := lt_trans zero_lt_one hr1
  constructor
  · rw [Chapter03.isBigO_iff]
    refine ⟨(r - 1)⁻¹, inv_pos.mpr (sub_pos.mpr hr1), 0, ?_⟩
    intro k hk
    rw [abs_of_nonneg (geomSum_nonneg hr_pos.le k)]
    rw [abs_of_nonneg (pow_nonneg hr_pos.le k)]
    exact geomSum_le_geometric_of_gt_one hr1 k
  · rw [Chapter03.isBigOmega_iff]
    refine ⟨(r : ℝ)⁻¹, inv_pos.mpr hr_pos, 1, ?_⟩
    intro k hk
    rw [abs_of_nonneg (geomSum_nonneg hr_pos.le k)]
    rw [abs_of_nonneg (pow_nonneg hr_pos.le k)]
    exact geometric_le_geomSum_of_gt_one hr1 hk

The continuous recursion-tree work

The recursion-tree work of a divide-and-conquer recurrence with polynomial forcing f(n) = n^p: level j has a^j subproblems, each of size b^(k-j) and cost (b^(k-j))^p (here n = b^k is an exact power, so division n/b is exact).

noncomputable def continuousWork (a b p k : ℕ) : ℝ :=
  ∑ j ∈ range k, (a : ℝ) ^ j * ((b : ℝ) ^ (k - j)) ^ p

The continuous ratio a / b^p that governs the geometric series.

noncomputable def continuousRatio (a b p : ℕ) : ℝ :=
  (a : ℝ) / (b : ℝ) ^ p

The recursion-tree work is nonnegative.


theorem continuousWork_nonneg (a b p k : ℕ) : 0 ≤ continuousWork a b p k := by
  rw [continuousWork]
  exact Finset.sum_nonneg (by
    intro j hj
    exact mul_nonneg (pow_nonneg (Nat.cast_nonneg a) j)
      (pow_nonneg (pow_nonneg (Nat.cast_nonneg b) (k - j)) p))

The recursion-tree work factors as b^(p·k) times the geometric series with ratio a / b^p: each level's work a^j (b^(k-j))^p equals b^(p·k) (a / b^p)^j.


theorem continuousWork_eq_geomSum (a b p : ℕ) (hb : (b : ℝ) ≠ 0) (k : ℕ) :
    continuousWork a b p k =
      (b : ℝ) ^ (p * k) * geomSum (continuousRatio a b p) k := by
  unfold continuousWork geomSum continuousRatio
  rw [Finset.mul_sum]
  apply Finset.sum_congr rfl
  intro j hj
  have hjlt : j < k := by simpa [mem_range] using hj
  calc
    (a : ℝ) ^ j * ((b : ℝ) ^ (k - j)) ^ p
        = (a : ℝ) ^ j * (b : ℝ) ^ ((k - j) * p) := by rw [← pow_mul]
    _ = (a : ℝ) ^ j * (b : ℝ) ^ (p * (k - j)) := by rw [Nat.mul_comm (k - j) p]
    _ = (a : ℝ) ^ j * (b : ℝ) ^ (p * k - p * j) := by
        rw [show p * (k - j) = p * k - p * j by exact Nat.mul_sub_left_distrib p k j]
    _ = (a : ℝ) ^ j * ((b : ℝ) ^ (p * k) / (b : ℝ) ^ (p * j)) := by
        rw [pow_sub₀ (b : ℝ) hb (Nat.mul_le_mul_left p (le_of_lt hjlt))]
        rw [div_eq_mul_inv]
    _ = (b : ℝ) ^ (p * k) * ((a : ℝ) ^ j / (b : ℝ) ^ (p * j)) := by ring
    _ = (b : ℝ) ^ (p * k) * ((a : ℝ) / (b : ℝ) ^ p) ^ j := by
        rw [div_pow, ← pow_mul]

The three continuous cases

Continuous master theorem, case 1. When the ratio a / b^p > 1 (so p < log_b a, i.e. the forcing n^p is polynomially smaller than the critical n^(log_b a)), the recursion-tree work is Θ(a^k), matching Θ(n^(log_b a)) on the exact power n = b^k.


theorem continuous_master_case1 (a b p : ℕ) (hb : (b : ℝ) ≠ 0)
    (hr : 1 < continuousRatio a b p) :
    Chapter03.isBigTheta (continuousWork a b p) (fun k => (a : ℝ) ^ k) := by
  have hratio : 1 < (a : ℝ) / (b : ℝ) ^ p := by simpa [continuousRatio] using hr
  have hpow_identity : ∀ k, (b : ℝ) ^ (p * k) * ((a : ℝ) / (b : ℝ) ^ p) ^ k = (a : ℝ) ^ k := by
    intro k
    calc
      (b : ℝ) ^ (p * k) * ((a : ℝ) / (b : ℝ) ^ p) ^ k
          = (b : ℝ) ^ (p * k) * ((a : ℝ) ^ k / (b : ℝ) ^ (p * k)) := by
            rw [div_pow, ← pow_mul]
      _ = (a : ℝ) ^ k := by
            field_simp [pow_ne_zero (p * k) hb]
  constructor
  · rw [Chapter03.isBigO_iff]
    refine ⟨((a : ℝ) / (b : ℝ) ^ p - 1)⁻¹, inv_pos.mpr (sub_pos.mpr hratio), 0, ?_⟩
    intro k hk
    rw [abs_of_nonneg (continuousWork_nonneg a b p k)]
    rw [abs_of_nonneg (pow_nonneg (Nat.cast_nonneg a) k)]
    rw [continuousWork_eq_geomSum a b p hb k]
    have hgeom : geomSum ((a : ℝ) / (b : ℝ) ^ p) k
        ≤ ((a : ℝ) / (b : ℝ) ^ p - 1)⁻¹ * ((a : ℝ) / (b : ℝ) ^ p) ^ k :=
      geomSum_le_geometric_of_gt_one hratio k
    have hterm : (b : ℝ) ^ (p * k) * geomSum ((a : ℝ) / (b : ℝ) ^ p) k
        ≤ ((a : ℝ) / (b : ℝ) ^ p - 1)⁻¹ * (a : ℝ) ^ k := by
      calc
        (b : ℝ) ^ (p * k) * geomSum ((a : ℝ) / (b : ℝ) ^ p) k
            ≤ (b : ℝ) ^ (p * k) *
                (((a : ℝ) / (b : ℝ) ^ p - 1)⁻¹ * ((a : ℝ) / (b : ℝ) ^ p) ^ k) :=
              mul_le_mul_of_nonneg_left hgeom (pow_nonneg (Nat.cast_nonneg b) (p * k))
        _ = ((a : ℝ) / (b : ℝ) ^ p - 1)⁻¹ *
                ((b : ℝ) ^ (p * k) * ((a : ℝ) / (b : ℝ) ^ p) ^ k) := by ring
        _ = ((a : ℝ) / (b : ℝ) ^ p - 1)⁻¹ * (a : ℝ) ^ k := by rw [hpow_identity k]
    exact hterm
  · rw [Chapter03.isBigOmega_iff]
    refine ⟨((a : ℝ) / (b : ℝ) ^ p)⁻¹, inv_pos.mpr (lt_trans zero_lt_one hratio), 1, ?_⟩
    intro k hk
    rw [abs_of_nonneg (continuousWork_nonneg a b p k)]
    rw [abs_of_nonneg (pow_nonneg (Nat.cast_nonneg a) k)]
    rw [continuousWork_eq_geomSum a b p hb k]
    have hgeom : ((a : ℝ) / (b : ℝ) ^ p)⁻¹ * ((a : ℝ) / (b : ℝ) ^ p) ^ k
        ≤ geomSum ((a : ℝ) / (b : ℝ) ^ p) k :=
      geometric_le_geomSum_of_gt_one hratio hk
    have hterm : ((a : ℝ) / (b : ℝ) ^ p)⁻¹ * (a : ℝ) ^ k
        ≤ (b : ℝ) ^ (p * k) * geomSum ((a : ℝ) / (b : ℝ) ^ p) k := by
      calc
        ((a : ℝ) / (b : ℝ) ^ p)⁻¹ * (a : ℝ) ^ k
            = ((a : ℝ) / (b : ℝ) ^ p)⁻¹ *
                ((b : ℝ) ^ (p * k) * ((a : ℝ) / (b : ℝ) ^ p) ^ k) := by rw [hpow_identity k]
        _ = (b : ℝ) ^ (p * k) *
                (((a : ℝ) / (b : ℝ) ^ p)⁻¹ * ((a : ℝ) / (b : ℝ) ^ p) ^ k) := by ring
        _ ≤ (b : ℝ) ^ (p * k) * geomSum ((a : ℝ) / (b : ℝ) ^ p) k :=
              mul_le_mul_of_nonneg_left hgeom (pow_nonneg (Nat.cast_nonneg b) (p * k))
    exact hterm

Continuous master theorem, case 2. When the ratio a / b^p = 1 (so a = b^p, i.e. the forcing n^p matches the critical n^(log_b a)), the recursion-tree work is Θ(k · a^k), the logarithmic case.


theorem continuous_master_case2 (a b p : ℕ) (hb : (b : ℝ) ≠ 0)
    (hr : continuousRatio a b p = 1) :
    Chapter03.isBigTheta (continuousWork a b p) (fun k => (k : ℝ) * (a : ℝ) ^ k) := by
  have hratio : (a : ℝ) / (b : ℝ) ^ p = 1 := by simpa [continuousRatio] using hr
  have hbp : (b : ℝ) ^ p ≠ 0 := pow_ne_zero p hb
  have hbase : (b : ℝ) ^ p = (a : ℝ) := by
    field_simp [hbp] at hratio
    exact hratio.symm
  have hpow_identity : ∀ k, (b : ℝ) ^ (p * k) = (a : ℝ) ^ k := by
    intro k
    rw [← hbase]
    rw [← pow_mul]
  constructor
  · rw [Chapter03.isBigO_iff]
    refine ⟨1, by norm_num, 0, ?_⟩
    intro k hk
    rw [abs_of_nonneg (continuousWork_nonneg a b p k)]
    rw [abs_of_nonneg (mul_nonneg (Nat.cast_nonneg k) (pow_nonneg (Nat.cast_nonneg a) k))]
    rw [continuousWork_eq_geomSum a b p hb k]
    rw [continuousRatio, hratio, geomSum_eq_of_one k]
    rw [hpow_identity k]
    nlinarith
  · rw [Chapter03.isBigOmega_iff]
    refine ⟨1, by norm_num, 0, ?_⟩
    intro k hk
    rw [abs_of_nonneg (continuousWork_nonneg a b p k)]
    rw [abs_of_nonneg (mul_nonneg (Nat.cast_nonneg k) (pow_nonneg (Nat.cast_nonneg a) k))]
    rw [continuousWork_eq_geomSum a b p hb k]
    rw [continuousRatio, hratio, geomSum_eq_of_one k]
    rw [hpow_identity k]
    nlinarith

Continuous master theorem, case 3. When the ratio a / b^p < 1 (so p > log_b a, i.e. the forcing n^p dominates the critical n^(log_b a)), the recursion-tree work is Θ(b^(p·k)), matching Θ(f(n)) = Θ(n^p) on the exact power n = b^k.


theorem continuous_master_case3 (a b p : ℕ) (hb : (b : ℝ) ≠ 0)
    (hr0 : 0 ≤ continuousRatio a b p) (hr1 : continuousRatio a b p < 1) :
    Chapter03.isBigTheta (continuousWork a b p) (fun k => (b : ℝ) ^ (p * k)) := by
  have hratio0 : 0 ≤ (a : ℝ) / (b : ℝ) ^ p := by simpa [continuousRatio] using hr0
  have hratio1 : (a : ℝ) / (b : ℝ) ^ p < 1 := by simpa [continuousRatio] using hr1
  constructor
  · rw [Chapter03.isBigO_iff]
    refine ⟨(1 - (a : ℝ) / (b : ℝ) ^ p)⁻¹, inv_pos.mpr (sub_pos.mpr hratio1), 0, ?_⟩
    intro k hk
    rw [abs_of_nonneg (continuousWork_nonneg a b p k)]
    rw [abs_of_nonneg (pow_nonneg (Nat.cast_nonneg b) (p * k))]
    rw [continuousWork_eq_geomSum a b p hb k]
    rw [continuousRatio]
    have hgeom : geomSum ((a : ℝ) / (b : ℝ) ^ p) k ≤ (1 - (a : ℝ) / (b : ℝ) ^ p)⁻¹ :=
      geomSum_le_of_lt_one hratio0 hratio1 k
    have hle := mul_le_mul_of_nonneg_left hgeom (pow_nonneg (Nat.cast_nonneg b) (p * k))
    simpa [mul_comm, mul_left_comm, mul_assoc] using hle
  · rw [Chapter03.isBigOmega_iff]
    refine ⟨1, by norm_num, 1, ?_⟩
    intro k hk
    have hk1 : 1 ≤ k := hk
    rw [abs_of_nonneg (continuousWork_nonneg a b p k)]
    rw [abs_of_nonneg (pow_nonneg (Nat.cast_nonneg b) (p * k))]
    rw [continuousWork_eq_geomSum a b p hb k]
    rw [continuousRatio]
    have hgeom : 1 ≤ geomSum ((a : ℝ) / (b : ℝ) ^ p) k := by
      rw [geomSum]
      rw [show (1 : ℝ) = ((a : ℝ) / (b : ℝ) ^ p) ^ 0 by simp]
      exact Finset.single_le_sum (f := fun j => ((a : ℝ) / (b : ℝ) ^ p) ^ j)
        (by intro j hj; exact pow_nonneg hratio0 j) (a := 0)
        (by rw [mem_range]; exact lt_of_lt_of_le zero_lt_one hk1)
    simpa [mul_comm, mul_left_comm, mul_assoc] using
      (mul_le_mul_of_nonneg_left hgeom (pow_nonneg (Nat.cast_nonneg b) (p * k)))

Bridge to the discrete comparison scales

The continuous case-1 scale a^k at the exact power n = b^k is exactly the discrete critical-power scale CLRS.Chapter04.criticalPowerScale, so the continuous master theorem's Θ(a^k) conclusion is the Θ(n^(log_b a)) scale of the all-input wrappers (through CLRS.Chapter04.criticalPowerScale_isBigTheta_realLogScale).


theorem continuous_case1_scale_eq_criticalPowerScale (a b : ℕ) (hb : 1 < b) (k : ℕ) :
    (a : ℝ) ^ k = criticalPowerScale a b (b ^ k) := by
  unfold criticalPowerScale
  rw [Nat.log_pow hb]

The discrete case-2 scale CLRS.Chapter04.criticalPowerLogScale on the exact power n = b^k is exactly (k + 1) · a^k, matching the continuous case-2 scale k · a^k up to the leading + 1.


theorem continuous_case2_criticalPowerLogScale_eq (a b : ℕ) (hb : 1 < b) (k : ℕ) :
    criticalPowerLogScale a b (b ^ k) = ((k : ℝ) + 1) * (a : ℝ) ^ k := by
  unfold criticalPowerLogScale
  rw [continuous_case1_scale_eq_criticalPowerScale a b hb k]
  rw [Nat.log_pow hb]

end Chapter04end CLRS

Definitions and proofs

CLRSLean.Chapter_04.Section_04_6_Master_Theorem_All_Input

Discrete critical-power scale for the exact-power Master theorem case 1. On exact powers it satisfies criticalPowerScale a b (b^i) = a^i; between exact powers it is the step function determined by Nat.log b n.

This, criticalPowerLogScale, and tailDominatedScale are deliberately weaker and cleaner than the analytic scales n^(log_b a), but it is enough to make the exact-power-to-all-input bridge concrete for the three Master cases.

def criticalPowerScale (a b : ℕ) (n : ℕ) : ℝ :=
  (a : ℝ) ^ Nat.log b n

Discrete case-2 Master scale. On exact powers this is (i+1) a^i; between exact powers it is the step function determined by Nat.log b n.

def criticalPowerLogScale (a b : ℕ) (n : ℕ) : ℝ :=
  ((Nat.log b n : ℝ) + 1) * criticalPowerScale a b n

When 1 ≤ a and 1 < b, the discrete critical-power scale a^(⌊log_b n⌋) is asymptotically equivalent to the real-log scale n^(log_b a).

This is the main bridge between the discrete all-input Master-theorem proof and the standard CLRS statement in terms of n^(log_b a). The constant factor is at most a in the Ω direction and 1 in the O direction, so the asymptotic class is exact.

Try this:
  [apply] ring_nf
  
  The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
    
  Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.Try this:
  [apply] ring_nf
  
  The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
    
  Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.Try this:
  [apply] ring_nf
  
  The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
    
  Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.Try this:
  [apply] ring_nf
  
  The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
    
  Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.Try this:
  [apply] ring_nf
  
  The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
    
  Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.Try this:
  [apply] ring_nf
  
  The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
    
  Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.Try this:
  [apply] ring_nf
  
  The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
    
  Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.Try this:
  [apply] ring_nf
  
  The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
    
  Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
theorem criticalPowerScale_isBigTheta_realLogScale
    (a b : ℕ) (ha : 1 ≤ a) (hb : 1 < b) :
    Chapter03.isBigTheta (criticalPowerScale a b) (realLogScale a b) := by
  have ha1 : 1 ≤ (a : ℝ) := by exact_mod_cast ha
  have ha_pos : 0 < (a : ℝ) := by
    exact lt_of_lt_of_le (by norm_num : (0 : ℝ) < 1) ha1
  have ha_nonneg : 0 ≤ (a : ℝ) := ha_pos.le
  have hb1 : 1 < (b : ℝ) := by exact_mod_cast hb
  have hb_pos : 0 < (b : ℝ) := by exact_mod_cast Nat.lt_trans Nat.zero_lt_one hb
  have hb_nonneg : 0 ≤ (b : ℝ) := hb_pos.le
  have hb_log_pos : 0 < Real.log (b : ℝ) := Real.log_pos hb1
  have hb_log_ne_zero : Real.log (b : ℝ) ≠ 0 := ne_of_gt hb_log_pos
  have ha_log_nonneg : 0 ≤ Real.log (a : ℝ) := Real.log_nonneg ha1
  -- The exponent α = log_b a
  have hα_nonneg : 0 ≤ realLogExponent a b := by
    dsimp [realLogExponent]
    exact div_nonneg ha_log_nonneg hb_log_pos.le
  -- Key identity: b^α = a
  have h_base_identity : (b : ℝ) ^ (realLogExponent a b) = (a : ℝ) := by
    dsimp [realLogExponent]
    calc
      (b : ℝ) ^ (Real.log (a : ℝ) / Real.log (b : ℝ))
          = Real.exp (Real.log (b : ℝ) * (Real.log (a : ℝ) / Real.log (b : ℝ))) := by
        rw [Real.rpow_def_of_pos hb_pos]
      _ = Real.exp (Real.log (a : ℝ)) := by
        field_simp [hb_log_ne_zero]
      _ = (a : ℝ) := Real.exp_log ha_pos
  -- formula for criticalPowerScale as a real power
  have hcrit_formula (n : ℕ) : (criticalPowerScale a b n : ℝ) =
      (a : ℝ) ^ (Nat.log b n : ℝ) := by
    dsimp [criticalPowerScale]
    simp [Real.rpow_natCast]
  constructor
  · -- O direction: criticalPowerScale a b = O(realLogScale a b)
    refine (Chapter03.isBigO_iff _ _).mpr ?_
    refine ⟨1, by norm_num, 1, ?_⟩
    intro n hn
    have hn_ne_zero : n ≠ 0 := by omega
    set k := Nat.log b n with hk_def
    have hpow_le : (b : ℕ) ^ k ≤ n := Nat.pow_log_le_self b hn_ne_zero
    have hpow_le_real : ((b : ℕ) ^ k : ℝ) ≤ (n : ℝ) := by exact_mod_cast hpow_le
    have hn_nonneg : 0 ≤ (n : ℝ) := by exact_mod_cast Nat.zero_le n
    have hcrit_nonneg : 0 ≤ criticalPowerScale a b n := by
      rw [hcrit_formula n]
      exact Real.rpow_nonneg (by exact_mod_cast Nat.zero_le a) _
    have hreal_nonneg : 0 ≤ realLogScale a b n := by
      dsimp [realLogScale]
      apply Real.rpow_nonneg hn_nonneg
    set α := realLogExponent a b with hα_def
    -- Core identity: a^k = (b^k)^α
    have hlog_mul : Real.log (b : ℝ) * α = Real.log (a : ℝ) := by
      dsimp [α, realLogExponent]
      field_simp [hb_log_ne_zero]
    have h_key : (a : ℝ) ^ (k : ℝ) = ((b : ℝ) ^ (k : ℝ)) ^ α := by
      calc
        (a : ℝ) ^ (k : ℝ) = Real.exp (Real.log (a : ℝ) * (k : ℝ)) := by
          rw [Real.rpow_def_of_pos ha_pos]
        _ = Real.exp ((k : ℝ) * Real.log (a : ℝ)) := by Try this:
  [apply] ring_nf
  
  The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
    
  Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.ring
        _ = Real.exp ((k : ℝ) * (Real.log (b : ℝ) * α)) := by rw [hlog_mul]
        _ = Real.exp ((Real.log (b : ℝ) * α) * (k : ℝ)) := by Try this:
  [apply] ring_nf
  
  The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
    
  Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.ring
        _ = Real.exp (Real.log (b : ℝ) * (α * (k : ℝ))) := by Try this:
  [apply] ring_nf
  
  The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
    
  Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.ring
        _ = Real.exp (Real.log (b : ℝ) * ((k : ℝ) * α)) := by Try this:
  [apply] ring_nf
  
  The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
    
  Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.ring
        _ = (b : ℝ) ^ ((k : ℝ) * α) := by rw [Real.rpow_def_of_pos hb_pos]
        _ = ((b : ℝ) ^ (k : ℝ)) ^ α := by rw [Real.rpow_mul hb_nonneg (k : ℝ) α]
    have hbpow_nonneg : 0 ≤ (b : ℝ) ^ (k : ℝ) :=
      Real.rpow_nonneg hb_nonneg _
    have hbpow_le_n : (b : ℝ) ^ (k : ℝ) ≤ (n : ℝ) := by
      rw [Real.rpow_natCast]
      simpa [Nat.cast_pow] using hpow_le_real
    calc
      |criticalPowerScale a b n| = criticalPowerScale a b n :=
        abs_of_nonneg hcrit_nonneg
      _ = (a : ℝ) ^ (k : ℝ) := by
        rw [hcrit_formula n, hk_def]
      _ = ((b : ℝ) ^ (k : ℝ)) ^ α := by rw [h_key]
      _ ≤ (n : ℝ) ^ α :=
        Real.rpow_le_rpow hbpow_nonneg hbpow_le_n hα_nonneg
      _ = realLogScale a b n := rfl
      _ = |realLogScale a b n| := by rw [abs_of_nonneg hreal_nonneg]
      _ = 1 * |realLogScale a b n| := by ring
  · -- Ω direction: realLogScale a b = O(criticalPowerScale a b)
    have ha_inv_pos : 0 < (a : ℝ)⁻¹ := inv_pos.mpr ha_pos
    refine (Chapter03.isBigOmega_iff _ _).mpr ?_
    refine ⟨(a : ℝ)⁻¹, ha_inv_pos, 1, ?_⟩
    intro n hn
    have hn_ne_zero : n ≠ 0 := by omega
    set k := Nat.log b n with hk_def
    have hpow_lt : n < b ^ (k + 1) := Nat.lt_pow_succ_log_self hb n
    have hcrit_nonneg : 0 ≤ criticalPowerScale a b n := by
      rw [hcrit_formula n]
      exact Real.rpow_nonneg (by exact_mod_cast Nat.zero_le a) _
    have hn_nonneg : 0 ≤ (n : ℝ) := by exact_mod_cast Nat.zero_le n
    have hreal_nonneg : 0 ≤ realLogScale a b n := by
      dsimp [realLogScale]
      apply Real.rpow_nonneg hn_nonneg
    set α := realLogExponent a b with hα_def
    have hlog_mul : Real.log (b : ℝ) * α = Real.log (a : ℝ) := by
      dsimp [α, realLogExponent]
      field_simp [hb_log_ne_zero]
    have h_key : (a : ℝ) ^ (k : ℝ) = ((b : ℝ) ^ (k : ℝ)) ^ α := by
      calc
        (a : ℝ) ^ (k : ℝ) = Real.exp (Real.log (a : ℝ) * (k : ℝ)) := by
          rw [Real.rpow_def_of_pos ha_pos]
        _ = Real.exp ((k : ℝ) * Real.log (a : ℝ)) := by Try this:
  [apply] ring_nf
  
  The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
    
  Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.ring
        _ = Real.exp ((k : ℝ) * (Real.log (b : ℝ) * α)) := by rw [hlog_mul]
        _ = Real.exp ((Real.log (b : ℝ) * α) * (k : ℝ)) := by Try this:
  [apply] ring_nf
  
  The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
    
  Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.ring
        _ = Real.exp (Real.log (b : ℝ) * (α * (k : ℝ))) := by Try this:
  [apply] ring_nf
  
  The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
    
  Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.ring
        _ = Real.exp (Real.log (b : ℝ) * ((k : ℝ) * α)) := by Try this:
  [apply] ring_nf
  
  The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
    
  Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.ring
        _ = (b : ℝ) ^ ((k : ℝ) * α) := by rw [Real.rpow_def_of_pos hb_pos]
        _ = ((b : ℝ) ^ (k : ℝ)) ^ α := by rw [Real.rpow_mul hb_nonneg (k : ℝ) α]
    have hbpow_nonneg : 0 ≤ (b : ℝ) ^ (k : ℝ) :=
      Real.rpow_nonneg hb_nonneg _
    -- n < b^(k+1) in ℕ → (n:ℝ) ≤ (b:ℝ) * (b:ℝ)^(k:ℝ) in ℝ
    have h_n_le_b_mul_bpow : (n : ℝ) ≤ (b : ℝ) * (b : ℝ) ^ (k : ℝ) := by
      have h_n_lt_bpow_succ_nat : n < b ^ (k + 1) := hpow_lt
      have h_n_lt_bpow_succ_real : (n : ℝ) < ((b : ℕ) ^ (k + 1) : ℝ) := by
        exact_mod_cast h_n_lt_bpow_succ_nat
      have h_bpow_succ_eq : ((b : ℕ) ^ (k + 1) : ℝ) = (b : ℝ) * (b : ℝ) ^ (k : ℝ) := by
        simp [pow_succ, Real.rpow_natCast, mul_comm]
      linarith
    -- n^α ≤ (b * b^k)^α = b^α * (b^k)^α = a * a^k = a * criticalPowerScale
    have h_bound : realLogScale a b n ≤ (a : ℝ) * (criticalPowerScale a b n : ℝ) := by
      calc
        realLogScale a b n = (n : ℝ) ^ α := rfl
        _ ≤ ((b : ℝ) * (b : ℝ) ^ (k : ℝ)) ^ α :=
          Real.rpow_le_rpow hn_nonneg h_n_le_b_mul_bpow hα_nonneg
        _ = ((b : ℝ) ^ α) * (((b : ℝ) ^ (k : ℝ)) ^ α) := by
          rw [Real.mul_rpow (z := α) hb_nonneg hbpow_nonneg]
        _ = (a : ℝ) * (((b : ℝ) ^ (k : ℝ)) ^ α) := by rw [h_base_identity]
        _ = (a : ℝ) * ((a : ℝ) ^ (k : ℝ)) := by rw [h_key]
        _ = (a : ℝ) * (criticalPowerScale a b n : ℝ) := by
          rw [hcrit_formula n, hk_def]
    calc
      (a : ℝ)⁻¹ * |realLogScale a b n|
          = (a : ℝ)⁻¹ * realLogScale a b n := by
            rw [abs_of_nonneg hreal_nonneg]
      _ ≤ (a : ℝ)⁻¹ * ((a : ℝ) * (criticalPowerScale a b n : ℝ)) := by
        gcongr
      _ = criticalPowerScale a b n := by
        field_simp [ne_of_gt ha_pos]
      _ = |criticalPowerScale a b n| := by
        rw [abs_of_nonneg hcrit_nonneg]