CLRS-Lean
Chapter 4. Divide-and-Conquer
4.6. Proof of the Master Theorem

Imports

import CLRSLean.Chapter_04.Section_04_5_Master_Theorem

CLRS Section 4.6 - All-input Master-theorem bridge

Section 4.5 proves the exact-power Master-theorem core for values T(b^i). The full CLRS theorem needs a second bridge from exact powers to arbitrary natural input sizes, including floor and ceiling recurrences.

This file proves the reusable transfer layer for that bridge. It first keeps the power-sandwich facts as explicit hypotheses, then gives a reusable way to discharge them from a monotonicity hypothesis plus a one-step scale bound between adjacent powers of the base. It also proves a real-log comparison bridge that connects the discrete scale a^(⌊log_b n⌋) to the textbook scale n^(log_b a) for all a ≥ 1 and b > 1.

namespace CLRSnamespace Chapter04

Monotone and sandwich interfaces

Absolute-value monotonicity for a cost function.

def MonotoneAbs (T : ℕ → ℝ) : Prop :=
  ∀ {m n : ℕ}, m ≤ n → |T m| ≤ |T n|

A monotone natural-valued cost remains monotone after casting to real absolute values.


theorem monotoneAbs_natCast {T : ℕ → ℕ} (hT : Monotone T) :
    MonotoneAbs (fun n => (T n : ℝ)) := by
  intro m n hmn
  rw [abs_of_nonneg (Nat.cast_nonneg _), abs_of_nonneg (Nat.cast_nonneg _)]
  change (T m : ℝ) ≤ (T n : ℝ)
  exact_mod_cast hT hmn

Eventual one-step control for a comparison scale across one multiplication by the Master-theorem base. This is the local regularity assumption that turns the adjacent-power interval b^i ≤ n < b^(i+1) into the global power-sandwich hypotheses below.

def EventuallyPowerStepBound (b : ℕ) (g : ℕ → ℝ) : Prop :=
  ∃ A : ℝ, 0 < A ∧ ∃ n₀ : ℕ, ∀ n, n₀ ≤ n → |g (b * n)| ≤ A * |g n|

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

Discrete case-2 Master scale with a polylog factor. On exact powers this is (i+1)^(k+1) a^i; between exact powers it is the step function determined by Nat.log b n. This is the f(n) = Θ(n^(log_b a)·log^k n) extension of criticalPowerLogScale.

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

The discrete polylog case-2 scale is nonnegative.

theorem criticalPowerLogPolylogScale_nonneg (a b k n : ℕ) :
    0 ≤ criticalPowerLogPolylogScale a b k n := by
  unfold criticalPowerLogPolylogScale criticalPowerScale
  positivity

On an exact power the discrete polylog case-2 scale collapses to (i+1)^(k+1)·a^i.

theorem criticalPowerLogPolylogScale_exactPower (a b k i : ℕ) (hb : 1 < b) :
    criticalPowerLogPolylogScale a b k (b ^ i) =
      ((i : ℝ) + 1) ^ (k + 1) * ((a : ℝ) ^ i) := by
  simp [criticalPowerLogPolylogScale, criticalPowerScale, Nat.log_pow hb]

The discrete polylog case-2 scale is monotone in absolute value.


theorem criticalPowerLogPolylogScale_monotoneAbs
    (a b k : ℕ) (ha : 1 ≤ a) :
    MonotoneAbs (criticalPowerLogPolylogScale a b k) := by
  intro m n hmn
  have ha_nonneg : 0 ≤ (a : ℝ) := by positivity
  have ha_one : 1 ≤ (a : ℝ) := by exact_mod_cast ha
  have hlog : Nat.log b m ≤ Nat.log b n := Nat.log_mono_right hmn
  have hlog_real : (Nat.log b m : ℝ) + 1 ≤ (Nat.log b n : ℝ) + 1 := by
    have hcast : (Nat.log b m : ℝ) ≤ Nat.log b n := by exact_mod_cast hlog
    linarith
  have hpow_factor : ((Nat.log b m : ℝ) + 1) ^ (k + 1) ≤
      ((Nat.log b n : ℝ) + 1) ^ (k + 1) := by
    exact pow_le_pow_left₀ (by positivity : 0 ≤ (Nat.log b m : ℝ) + 1) hlog_real (k + 1)
  have hpow : (a : ℝ) ^ Nat.log b m ≤ (a : ℝ) ^ Nat.log b n :=
    pow_le_pow_right₀ ha_one hlog
  rw [abs_of_nonneg (criticalPowerLogPolylogScale_nonneg a b k m),
    abs_of_nonneg (criticalPowerLogPolylogScale_nonneg a b k n)]
  unfold criticalPowerLogPolylogScale criticalPowerScale
  exact mul_le_mul hpow_factor hpow (pow_nonneg ha_nonneg _) (by positivity)

The discrete polylog case-2 scale has eventual one-step control across one multiplication by b.


theorem criticalPowerLogPolylogScale_powerStepBound
    (a b k : ℕ) (ha : 1 ≤ a) (hb : 1 < b) :
    EventuallyPowerStepBound b (criticalPowerLogPolylogScale a b k) := by
  refine ⟨(2 ^ (k + 1) : ℝ) * (a : ℝ), ?_, 1, ?_⟩
  · have ha_pos : 0 < (a : ℝ) := by exact_mod_cast Nat.lt_of_lt_of_le Nat.zero_lt_one ha
    positivity
  · intro n hn
    have ha_nonneg : 0 ≤ (a : ℝ) := by positivity
    have hn_ne_zero : n ≠ 0 := by omega
    have hlog : Nat.log b (b * n) = Nat.log b n + 1 := by
      rw [Nat.mul_comm]
      exact Nat.log_mul_base hb hn_ne_zero
    have hratio : ((Nat.log b n : ℝ) + 2) ^ (k + 1) ≤
        (2 ^ (k + 1) : ℝ) * ((Nat.log b n : ℝ) + 1) ^ (k + 1) := by
      have hlog_nonneg : 0 ≤ (Nat.log b n : ℝ) := by positivity
      have h2 : (Nat.log b n : ℝ) + 2 ≤ 2 * ((Nat.log b n : ℝ) + 1) := by linarith
      calc
        ((Nat.log b n : ℝ) + 2) ^ (k + 1) ≤ (2 * ((Nat.log b n : ℝ) + 1)) ^ (k + 1) := by
          exact pow_le_pow_left₀ (by positivity) h2 (k + 1)
        _ = (2 ^ (k + 1) : ℝ) * ((Nat.log b n : ℝ) + 1) ^ (k + 1) := by
          rw [mul_pow]
    calc
      |criticalPowerLogPolylogScale a b k (b * n)|
          = ((Nat.log b n : ℝ) + 2) ^ (k + 1) * ((a : ℝ) ^ (Nat.log b n + 1)) := by
            rw [abs_of_nonneg (criticalPowerLogPolylogScale_nonneg a b k (b * n))]
            unfold criticalPowerLogPolylogScale criticalPowerScale
            rw [hlog]
            norm_cast
      _ = (a : ℝ) * (((Nat.log b n : ℝ) + 2) ^ (k + 1) * (a : ℝ) ^ Nat.log b n) := by
        rw [pow_succ]
        ring
      _ ≤ (a : ℝ) *
          ((2 ^ (k + 1) : ℝ) * ((Nat.log b n : ℝ) + 1) ^ (k + 1) * (a : ℝ) ^ Nat.log b n) := by
            exact mul_le_mul_of_nonneg_left
              (mul_le_mul_of_nonneg_right hratio (by positivity : 0 ≤ (a : ℝ) ^ Nat.log b n))
              ha_nonneg
      _ = ((2 ^ (k + 1) : ℝ) * (a : ℝ)) * |criticalPowerLogPolylogScale a b k n| := by
        rw [abs_of_nonneg (criticalPowerLogPolylogScale_nonneg a b k n)]
        simp [criticalPowerLogPolylogScale, criticalPowerScale]
        ring

Discrete case-3 Master scale. On exact powers this is the scale from master_case3_tail_dominated; between exact powers it is again the step function determined by Nat.log b n.

noncomputable def tailDominatedScale (a b : ℕ) (f : ℕ → ℝ) (n : ℕ) : ℝ :=
  (if Nat.log b n = 0 then 1 else normalizedForcing a b f (Nat.log b n - 1)) *
    criticalPowerScale a b n

              theorem criticalPowerScale_exactPower
    (a b i : ℕ) (hb : 1 < b) :
    criticalPowerScale a b (b ^ i) = (a : ℝ) ^ i := by
  simp [criticalPowerScale, Nat.log_pow hb]theorem criticalPowerLogScale_exactPower
    (a b i : ℕ) (hb : 1 < b) :
    criticalPowerLogScale a b (b ^ i) =
      ((i : ℝ) + 1) * ((a : ℝ) ^ i) := by
  simp [criticalPowerLogScale, criticalPowerScale, Nat.log_pow hb]theorem tailDominatedScale_exactPower
    (a b : ℕ) (f : ℕ → ℝ) (i : ℕ) (hb : 1 < b) :
    tailDominatedScale a b f (b ^ i) =
      (if i = 0 then 1 else normalizedForcing a b f (i - 1)) *
        ((a : ℝ) ^ i) := by
  simp [tailDominatedScale, criticalPowerScale, Nat.log_pow hb]theorem criticalPowerLogScale_nonneg (a b n : ℕ) :
    0 ≤ criticalPowerLogScale a b n := by
  unfold criticalPowerLogScale criticalPowerScale
  positivity

theorem criticalPowerScale_monotoneAbs
    (a b : ℕ) (ha : 1 ≤ a) :
    MonotoneAbs (criticalPowerScale a b) := by
  intro m n hmn
  have ha_nonneg : 0 ≤ (a : ℝ) := by positivity
  have ha_one : 1 ≤ (a : ℝ) := by exact_mod_cast ha
  have hlog : Nat.log b m ≤ Nat.log b n :=
    Nat.log_mono_right hmn
  calc
    |criticalPowerScale a b m| = (a : ℝ) ^ Nat.log b m := by
      rw [criticalPowerScale, abs_of_nonneg (pow_nonneg ha_nonneg _)]
    _ ≤ (a : ℝ) ^ Nat.log b n :=
      pow_le_pow_right₀ ha_one hlog
    _ = |criticalPowerScale a b n| := by
      rw [criticalPowerScale, abs_of_nonneg (pow_nonneg ha_nonneg _)]

theorem criticalPowerScale_powerStepBound
    (a b : ℕ) (ha : 1 ≤ a) (hb : 1 < b) :
    EventuallyPowerStepBound b (criticalPowerScale a b) := by
  refine ⟨(a : ℝ), ?_, 1, ?_⟩
  · exact_mod_cast Nat.lt_of_lt_of_le Nat.zero_lt_one ha
  · intro n hn
    have hn_ne_zero : n ≠ 0 := by omega
    have hlog : Nat.log b (b * n) = Nat.log b n + 1 := by
      rw [Nat.mul_comm]
      exact Nat.log_mul_base hb hn_ne_zero
    simp [criticalPowerScale, hlog, abs_of_nonneg (pow_nonneg ha_nonneg _),
      pow_succ, mul_comm]

theorem criticalPowerLogScale_monotoneAbs
    (a b : ℕ) (ha : 1 ≤ a) :
    MonotoneAbs (criticalPowerLogScale a b) := by
  intro m n hmn
  have ha_nonneg : 0 ≤ (a : ℝ) := by positivity
  have ha_one : 1 ≤ (a : ℝ) := by exact_mod_cast ha
  have hlog : Nat.log b m ≤ Nat.log b n :=
    Nat.log_mono_right hmn
  have hlog_real :
      (Nat.log b m : ℝ) + 1 ≤ (Nat.log b n : ℝ) + 1 := by
    have hcast : (Nat.log b m : ℝ) ≤ Nat.log b n := by
      exact_mod_cast hlog
    linarith
  have hpow :
      (a : ℝ) ^ Nat.log b m ≤ (a : ℝ) ^ Nat.log b n :=
    pow_le_pow_right₀ ha_one hlog
  rw [abs_of_nonneg (criticalPowerLogScale_nonneg a b m),
    abs_of_nonneg (criticalPowerLogScale_nonneg a b n)]
  unfold criticalPowerLogScale criticalPowerScale
  exact mul_le_mul hlog_real hpow (pow_nonneg ha_nonneg _)
    (by positivity)

theorem criticalPowerLogScale_powerStepBound
    (a b : ℕ) (ha : 1 ≤ a) (hb : 1 < b) :
    EventuallyPowerStepBound b (criticalPowerLogScale a b) := by
  refine ⟨2 * (a : ℝ), ?_, 1, ?_⟩
  · have ha_pos : 0 < (a : ℝ) := by
      exact_mod_cast Nat.lt_of_lt_of_le Nat.zero_lt_one ha
    positivity
  · intro n hn
    have ha_nonneg : 0 ≤ (a : ℝ) := by positivity
    have hn_ne_zero : n ≠ 0 := by omega
    have hlog : Nat.log b (b * n) = Nat.log b n + 1 := by
      rw [Nat.mul_comm]
      exact Nat.log_mul_base hb hn_ne_zero
    have hratio :
        (Nat.log b n : ℝ) + 2 ≤
          2 * ((Nat.log b n : ℝ) + 1) := by
      have hlog_nonneg : 0 ≤ (Nat.log b n : ℝ) := by positivity
      linarith
    calc
      |criticalPowerLogScale a b (b * n)|
          = ((Nat.log b n : ℝ) + 2) *
              ((a : ℝ) * (a : ℝ) ^ Nat.log b n) := by
            rw [abs_of_nonneg (criticalPowerLogScale_nonneg a b (b * n))]
            simp [criticalPowerLogScale, criticalPowerScale, hlog, pow_succ,
              Nat.cast_add]
            ring
      _ = (a : ℝ) *
            (((Nat.log b n : ℝ) + 2) *
              (a : ℝ) ^ Nat.log b n) := by ring
      _ ≤ (a : ℝ) *
            (2 * ((Nat.log b n : ℝ) + 1) *
              (a : ℝ) ^ Nat.log b n) := by
            gcongr
      _ = (2 * (a : ℝ)) * |criticalPowerLogScale a b n| := by
            rw [abs_of_nonneg (criticalPowerLogScale_nonneg a b n)]
            simp [criticalPowerLogScale, criticalPowerScale]
            ring

Polynomial comparison scales

The usual polynomial comparison scale n^p. This is the textbook-facing specialization of the critical Master scale when a = b^p.

noncomputable def polynomialScale (p : ℕ) (n : ℕ) : ℝ :=
  (n : ℝ) ^ p

The polynomial-logarithmic comparison scale (⌊log_b n⌋ + 1)n^p. It is a discrete-log version of the CLRS case-2 scale n^p log n, chosen so that it connects directly to the all-input exact-power bridge.

noncomputable def polynomialLogScale (b p : ℕ) (n : ℕ) : ℝ :=
  ((Nat.log b n : ℝ) + 1) * polynomialScale p n

              

theorem criticalPowerScale_of_base_pow (b p n : ℕ) :
    criticalPowerScale (b ^ p) b n =
      (((b ^ Nat.log b n : ℕ) : ℝ) ^ p) := by
  simp only [criticalPowerScale, Nat.cast_pow]
  rw [← pow_mul, ← pow_mul, Nat.mul_comm]

theorem pow_succ_pow_eq_mul_pow (b i p : ℕ) :
    (b ^ (i + 1)) ^ p = (b ^ p) * (b ^ i) ^ p := by
  rw [show b ^ (i + 1) = b * b ^ i by
    rw [pow_succ, Nat.mul_comm]]
  rw [Nat.mul_pow]private theorem one_le_base_pow_of_one_lt (b p : ℕ) (hb : 1 < b) :
    1 ≤ b ^ p := by
  have hb_pos : 0 < b := Nat.lt_trans Nat.zero_lt_one hb
  exact Nat.succ_le_iff.mpr (pow_pos hb_pos p)

When a = b^p, the discrete critical-power scale is asymptotic to the ordinary polynomial scale n^p. This is the main comparison lemma that turns case-1 all-input Master wrappers into textbook-looking statements whenever log_b a is a natural number.


theorem criticalPowerScale_isBigTheta_polynomialScale
    (b p : ℕ) (hb : 1 < b) :
    Chapter03.isBigTheta (criticalPowerScale (b ^ p) b) (polynomialScale p) := by
  constructor
  · refine (Chapter03.isBigO_iff _ _).mpr ?_
    refine ⟨1, by norm_num, 1, ?_⟩
    intro n hn
    have hn_ne_zero : n ≠ 0 := by omega
    have hlow : b ^ Nat.log b n ≤ n :=
      Nat.pow_log_le_self b hn_ne_zero
    have hpow :
        ((b ^ Nat.log b n : ℕ) : ℝ) ^ p ≤ (n : ℝ) ^ p := by
      exact_mod_cast Nat.pow_le_pow_left hlow p
    calc
      |criticalPowerScale (b ^ p) b n|
          = ((b ^ Nat.log b n : ℕ) : ℝ) ^ p := by
            rw [criticalPowerScale_of_base_pow]
            exact abs_of_nonneg (pow_nonneg (by positivity) p)
      _ ≤ (n : ℝ) ^ p := hpow
      _ = 1 * |polynomialScale p n| := by
            rw [polynomialScale,
              abs_of_nonneg (pow_nonneg (by positivity) p)]
            ring
  · refine (Chapter03.isBigOmega_iff _ _).mpr ?_
    let B : ℝ := ((b ^ p : ℕ) : ℝ)
    have hb_pos : 0 < b := Nat.lt_trans Nat.zero_lt_one hb
    have hB_pos_nat : 0 < b ^ p := pow_pos hb_pos p
    have hB_pos : 0 < B := by
      dsimp [B]
      exact_mod_cast hB_pos_nat
    refine ⟨B⁻¹, inv_pos.mpr hB_pos, 1, ?_⟩
    intro n hn
    have hn_ne_zero : n ≠ 0 := by omega
    let i := Nat.log b n
    have hhigh : n < b ^ (i + 1) := by
      simpa [i] using Nat.lt_pow_succ_log_self hb n
    have hupper_nat : n ^ p ≤ (b ^ p) * (b ^ i) ^ p := by
      calc
        n ^ p ≤ (b ^ (i + 1)) ^ p :=
          Nat.pow_le_pow_left (Nat.le_of_lt hhigh) p
        _ = (b ^ p) * (b ^ i) ^ p :=
          pow_succ_pow_eq_mul_pow b i p
    have hupper_real :
        (n : ℝ) ^ p ≤ B * (((b ^ i : ℕ) : ℝ) ^ p) := by
      dsimp [B]
      exact_mod_cast hupper_nat
    calc
      B⁻¹ * |polynomialScale p n|
          = B⁻¹ * (n : ℝ) ^ p := by
            rw [polynomialScale,
              abs_of_nonneg (pow_nonneg (by positivity) p)]
      _ ≤ B⁻¹ * (B * (((b ^ i : ℕ) : ℝ) ^ p)) := by
            gcongr
      _ = ((b ^ i : ℕ) : ℝ) ^ p := by
            field_simp [ne_of_gt hB_pos]
      _ = |criticalPowerScale (b ^ p) b n| := by
            rw [criticalPowerScale_of_base_pow]
            simp [i, abs_of_nonneg (pow_nonneg (by positivity) p)]

When a = b^p, the discrete case-2 Master scale is asymptotic to (⌊log_b n⌋ + 1)n^p. This keeps the statement discrete while matching the standard n^p log n shape used in CLRS.


theorem criticalPowerLogScale_isBigTheta_polynomialLogScale
    (b p : ℕ) (hb : 1 < b) :
    Chapter03.isBigTheta (criticalPowerLogScale (b ^ p) b)
      (polynomialLogScale b p) := by
  constructor
  · refine (Chapter03.isBigO_iff _ _).mpr ?_
    refine ⟨1, by norm_num, 1, ?_⟩
    intro n hn
    have hn_ne_zero : n ≠ 0 := by omega
    have hlow : b ^ Nat.log b n ≤ n :=
      Nat.pow_log_le_self b hn_ne_zero
    have hpow :
        ((b ^ Nat.log b n : ℕ) : ℝ) ^ p ≤ (n : ℝ) ^ p := by
      exact_mod_cast Nat.pow_le_pow_left hlow p
    have hL_nonneg : 0 ≤ (Nat.log b n : ℝ) + 1 := by positivity
    calc
      |criticalPowerLogScale (b ^ p) b n|
          = ((Nat.log b n : ℝ) + 1) *
              (((b ^ Nat.log b n : ℕ) : ℝ) ^ p) := by
            rw [abs_of_nonneg (criticalPowerLogScale_nonneg (b ^ p) b n)]
            simp [criticalPowerLogScale, criticalPowerScale_of_base_pow]
      _ ≤ ((Nat.log b n : ℝ) + 1) * ((n : ℝ) ^ p) := by
            gcongr
      _ = 1 * |polynomialLogScale b p n| := by
            rw [polynomialLogScale, polynomialScale,
              abs_of_nonneg
                (mul_nonneg hL_nonneg (pow_nonneg (by positivity) p))]
            ring
  · refine (Chapter03.isBigOmega_iff _ _).mpr ?_
    let B : ℝ := ((b ^ p : ℕ) : ℝ)
    have hb_pos : 0 < b := Nat.lt_trans Nat.zero_lt_one hb
    have hB_pos_nat : 0 < b ^ p := pow_pos hb_pos p
    have hB_pos : 0 < B := by
      dsimp [B]
      exact_mod_cast hB_pos_nat
    refine ⟨B⁻¹, inv_pos.mpr hB_pos, 1, ?_⟩
    intro n hn
    have hn_ne_zero : n ≠ 0 := by omega
    let i := Nat.log b n
    have hhigh : n < b ^ (i + 1) := by
      simpa [i] using Nat.lt_pow_succ_log_self hb n
    have hupper_nat : n ^ p ≤ (b ^ p) * (b ^ i) ^ p := by
      calc
        n ^ p ≤ (b ^ (i + 1)) ^ p :=
          Nat.pow_le_pow_left (Nat.le_of_lt hhigh) p
        _ = (b ^ p) * (b ^ i) ^ p :=
          pow_succ_pow_eq_mul_pow b i p
    have hupper_real :
        (n : ℝ) ^ p ≤ B * (((b ^ i : ℕ) : ℝ) ^ p) := by
      dsimp [B]
      exact_mod_cast hupper_nat
    have hL_nonneg : 0 ≤ (Nat.log b n : ℝ) + 1 := by positivity
    calc
      B⁻¹ * |polynomialLogScale b p n|
          = B⁻¹ * (((Nat.log b n : ℝ) + 1) * (n : ℝ) ^ p) := by
            rw [polynomialLogScale, polynomialScale,
              abs_of_nonneg
                (mul_nonneg hL_nonneg (pow_nonneg (by positivity) p))]
      _ ≤ B⁻¹ * (((Nat.log b n : ℝ) + 1) *
            (B * (((b ^ i : ℕ) : ℝ) ^ p))) := by
            gcongr
      _ = ((Nat.log b n : ℝ) + 1) * (((b ^ i : ℕ) : ℝ) ^ p) := by
            field_simp [ne_of_gt hB_pos]
      _ = |criticalPowerLogScale (b ^ p) b n| := by
            rw [abs_of_nonneg (criticalPowerLogScale_nonneg (b ^ p) b n)]
            simp [criticalPowerLogScale, criticalPowerScale_of_base_pow, i]

Real-logarithmic comparison scales

The real-valued exponent log_b a = log a / log b. This is the exponent that appears in the standard CLRS Master-theorem statement as n^(log_b a).

When a = b^p for natural p, this reduces to (p : ℝ), and the criticalPowerScale_isBigTheta_polynomialScale comparison above is a special case of the general comparison proved here.

noncomputable def realLogExponent (a b : ℕ) : ℝ :=
  Real.log (a : ℝ) / Real.log (b : ℝ)

The real-log comparison scale n^(log_b a). This is the textbook scale used in the standard CLRS statement of the Master theorem: the homogeneous-solution growth rate without floors and ceilings.

For integer exponents it coincides with the ordinary polynomial scale polynomialScale.

noncomputable def realLogScale (a b : ℕ) (n : ℕ) : ℝ :=
  (n : ℝ) ^ (realLogExponent a b)

The textbook case-2 Master scale n^(log_b a) log n.

noncomputable def realLogLogScale (a b : ℕ) (n : ℕ) : ℝ :=
  realLogScale a b n * Real.log (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]

When 1 ≤ a and 1 < b, the discrete case-2 scale (⌊log_b n⌋+1)a^(⌊log_b n⌋) is asymptotically equivalent to the textbook scale n^(log_b a) log n.


theorem criticalPowerLogScale_isBigTheta_realLogLogScale
    (a b : ℕ) (ha : 1 ≤ a) (hb : 1 < b) :
    Chapter03.isBigTheta (criticalPowerLogScale a b) (realLogLogScale a b) := by
  have hb1 : 1 < (b : ℝ) := by exact_mod_cast hb
  have hb_pos_nat : 0 < b := Nat.lt_trans Nat.zero_lt_one hb
  have hb_log_pos : 0 < Real.log (b : ℝ) := Real.log_pos hb1
  have hb_log_nonneg : 0 ≤ Real.log (b : ℝ) := hb_log_pos.le
  have hscale := criticalPowerScale_isBigTheta_realLogScale a b ha hb
  constructor
  · rcases (Chapter03.isBigO_iff _ _).mp hscale.1 with
      ⟨Cscale, hCscale_pos, nScale, hScale⟩
    let Clog : ℝ := 2 / Real.log (b : ℝ)
    have hClog_pos : 0 < Clog := by
      dsimp [Clog]
      exact div_pos (by norm_num) hb_log_pos
    refine (Chapter03.isBigO_iff _ _).mpr ?_
    refine ⟨Cscale * Clog, mul_pos hCscale_pos hClog_pos, max nScale b, ?_⟩
    intro n hn
    have hnScale : nScale ≤ n := le_trans (Nat.le_max_left nScale b) hn
    have hnb : b ≤ n := le_trans (Nat.le_max_right nScale b) hn
    have hn_pos_nat : 0 < n := lt_of_lt_of_le hb_pos_nat hnb
    have hn_pos : 0 < (n : ℝ) := by exact_mod_cast hn_pos_nat
    have hbn_real : (b : ℝ) ≤ (n : ℝ) := by exact_mod_cast hnb
    have hlogb_le_logn : Real.log (b : ℝ) ≤ Real.log (n : ℝ) :=
      Real.log_le_log (by exact_mod_cast hb_pos_nat) hbn_real
    have hlogn_nonneg : 0 ≤ Real.log (n : ℝ) :=
      le_trans hb_log_nonneg hlogb_le_logn
    let k := Nat.log b n
    have hk_def : k = Nat.log b n := rfl
    have hpow_le : b ^ k ≤ n := by
      rw [hk_def]
      exact Nat.pow_log_le_self b (ne_of_gt hn_pos_nat)
    have hpow_le_real : ((b : ℕ) ^ k : ℝ) ≤ (n : ℝ) := by
      exact_mod_cast hpow_le
    have hpow_pos : 0 < ((b : ℕ) ^ k : ℝ) := by
      exact_mod_cast pow_pos hb_pos_nat k
    have hlog_lower := Real.log_le_log hpow_pos hpow_le_real
    have hklog_le : (k : ℝ) * Real.log (b : ℝ) ≤ Real.log (n : ℝ) := by
      simpa [Real.log_pow] using hlog_lower
    have hsum :
        ((k : ℝ) + 1) * Real.log (b : ℝ) ≤ 2 * Real.log (n : ℝ) := by
      calc
        ((k : ℝ) + 1) * Real.log (b : ℝ)
            = (k : ℝ) * Real.log (b : ℝ) + Real.log (b : ℝ) := by ring
        _ ≤ Real.log (n : ℝ) + Real.log (n : ℝ) := by gcongr
        _ = 2 * Real.log (n : ℝ) := by ring
    have hdiv := (div_le_div_iff_of_pos_right hb_log_pos).mpr hsum
    have hlog_upper :
        ((k : ℝ) + 1) ≤ Clog * Real.log (n : ℝ) := by
      calc
        (k : ℝ) + 1 =
            (((k : ℝ) + 1) * Real.log (b : ℝ)) / Real.log (b : ℝ) := by
              field_simp [ne_of_gt hb_log_pos]
        _ ≤ (2 * Real.log (n : ℝ)) / Real.log (b : ℝ) := hdiv
        _ = Clog * Real.log (n : ℝ) := by
              dsimp [Clog]
              ring
    have hL_nonneg : 0 ≤ (k : ℝ) + 1 := by positivity
    have hcrit_nonneg : 0 ≤ criticalPowerScale a b n := by
      unfold criticalPowerScale
      positivity
    have hreal_nonneg : 0 ≤ realLogScale a b n := by
      unfold realLogScale
      exact Real.rpow_nonneg (by exact_mod_cast Nat.zero_le n) _
    have hscale_bound :
        criticalPowerScale a b n ≤ Cscale * realLogScale a b n := by
      have h := hScale n hnScale
      simpa [abs_of_nonneg hcrit_nonneg, abs_of_nonneg hreal_nonneg] using h
    have hright_nonneg :
        0 ≤ realLogScale a b n * Real.log (n : ℝ) :=
      mul_nonneg hreal_nonneg hlogn_nonneg
    calc
      |criticalPowerLogScale a b n|
          = ((k : ℝ) + 1) * criticalPowerScale a b n := by
            rw [abs_of_nonneg (criticalPowerLogScale_nonneg a b n)]
            simp [criticalPowerLogScale, k, criticalPowerScale]
      _ ≤ ((k : ℝ) + 1) * (Cscale * realLogScale a b n) := by
            gcongr
      _ ≤ (Clog * Real.log (n : ℝ)) * (Cscale * realLogScale a b n) := by
            gcongr
      _ = (Cscale * Clog) * (realLogScale a b n * Real.log (n : ℝ)) := by
            ring
      _ = (Cscale * Clog) * |realLogLogScale a b n| := by
            rw [realLogLogScale, abs_of_nonneg hright_nonneg]
  · rcases (Chapter03.isBigOmega_iff _ _).mp hscale.2 with
      ⟨Cscale, hCscale_pos, nScale, hScale⟩
    let Clog : ℝ := (Real.log (b : ℝ))⁻¹
    have hClog_pos : 0 < Clog := by
      dsimp [Clog]
      exact inv_pos.mpr hb_log_pos
    refine (Chapter03.isBigOmega_iff _ _).mpr ?_
    refine ⟨Cscale * Clog, mul_pos hCscale_pos hClog_pos, max nScale b, ?_⟩
    intro n hn
    have hnScale : nScale ≤ n := le_trans (Nat.le_max_left nScale b) hn
    have hnb : b ≤ n := le_trans (Nat.le_max_right nScale b) hn
    have hn_pos_nat : 0 < n := lt_of_lt_of_le hb_pos_nat hnb
    have hn_pos : 0 < (n : ℝ) := by exact_mod_cast hn_pos_nat
    have hbn_real : (b : ℝ) ≤ (n : ℝ) := by exact_mod_cast hnb
    have hlogb_le_logn : Real.log (b : ℝ) ≤ Real.log (n : ℝ) :=
      Real.log_le_log (by exact_mod_cast hb_pos_nat) hbn_real
    have hlogn_nonneg : 0 ≤ Real.log (n : ℝ) :=
      le_trans hb_log_nonneg hlogb_le_logn
    let k := Nat.log b n
    have hk_def : k = Nat.log b n := rfl
    have hpow_lt : n < b ^ (k + 1) := by
      rw [hk_def]
      exact Nat.lt_pow_succ_log_self hb n
    have hpow_le_real : (n : ℝ) ≤ ((b : ℕ) ^ (k + 1) : ℝ) := by
      exact_mod_cast Nat.le_of_lt hpow_lt
    have hlog_le := Real.log_le_log hn_pos hpow_le_real
    have hlog_upper_by_L :
        Real.log (n : ℝ) ≤ Real.log (b : ℝ) * ((k : ℝ) + 1) := by
      calc
        Real.log (n : ℝ) ≤ ((k : ℝ) + 1) * Real.log (b : ℝ) := by
          simpa [Real.log_pow, Nat.cast_add, add_mul] using hlog_le
        _ = Real.log (b : ℝ) * ((k : ℝ) + 1) := by ring
    have hlog_lower :
        Clog * Real.log (n : ℝ) ≤ (k : ℝ) + 1 := by
      calc
        Clog * Real.log (n : ℝ)
            ≤ Clog * (Real.log (b : ℝ) * ((k : ℝ) + 1)) := by
              gcongr
        _ = (k : ℝ) + 1 := by
              dsimp [Clog]
              field_simp [ne_of_gt hb_log_pos]
    have hL_nonneg : 0 ≤ (k : ℝ) + 1 := by positivity
    have hcrit_nonneg : 0 ≤ criticalPowerScale a b n := by
      unfold criticalPowerScale
      positivity
    have hreal_nonneg : 0 ≤ realLogScale a b n := by
      unfold realLogScale
      exact Real.rpow_nonneg (by exact_mod_cast Nat.zero_le n) _
    have hscale_bound :
        Cscale * realLogScale a b n ≤ criticalPowerScale a b n := by
      have h := hScale n hnScale
      simpa [abs_of_nonneg hcrit_nonneg, abs_of_nonneg hreal_nonneg] using h
    have hright_nonneg :
        0 ≤ realLogScale a b n * Real.log (n : ℝ) :=
      mul_nonneg hreal_nonneg hlogn_nonneg
    calc
      (Cscale * Clog) * |realLogLogScale a b n|
          = (Clog * Real.log (n : ℝ)) *
              (Cscale * realLogScale a b n) := by
            rw [realLogLogScale, abs_of_nonneg hright_nonneg]
            ring
      _ ≤ ((k : ℝ) + 1) * criticalPowerScale a b n := by
            gcongr
      _ = |criticalPowerLogScale a b n| := by
            rw [abs_of_nonneg (criticalPowerLogScale_nonneg a b n)]
            simp [criticalPowerLogScale, k, criticalPowerScale]

Floor/ceiling recurrence interfaces

All-input floor-division form of the Master-theorem recurrence: T(n) = a T(⌊n / b⌋) + f(n).

structure FloorDivideRecurrence (a b : ℕ) (f T : ℕ → ℝ) : Prop where
  step : ∀ n : ℕ, T n = (a : ℝ) * T (n / b) + f n

All-input ceiling-division form of the Master-theorem recurrence: T(n) = a T(⌈n / b⌉) + f(n), represented over natural numbers as (n + b - 1) / b.

structure CeilDivideRecurrence (a b : ℕ) (f T : ℕ → ℝ) : Prop where
  step : ∀ n : ℕ, T n = (a : ℝ) * T ((n + (b - 1)) / b) + f n

              

theorem pow_succ_div_base {b i : ℕ} (hb : 0 < b) :
    b ^ (i + 1) / b = b ^ i := by
  rw [show b ^ (i + 1) = b * b ^ i by
    rw [pow_succ, Nat.mul_comm]]
  exact Nat.mul_div_right (b ^ i) hb

theorem pow_succ_add_pred_div_base {b i : ℕ} (hb : 0 < b) :
    (b ^ (i + 1) + (b - 1)) / b = b ^ i := by
  apply Nat.div_eq_of_lt_le
  · rw [show b ^ i * b = b ^ (i + 1) by rw [pow_succ]]
    exact Nat.le_add_right _ _
  · rw [Nat.add_mul, one_mul]
    rw [show b ^ i * b = b ^ (i + 1) by rw [pow_succ]]
    omega

theorem exactPowerRecurrence_of_floorDivideRecurrence
    (a b : ℕ) (f T : ℕ → ℝ)
    (h_rec : FloorDivideRecurrence a b f T) (hb : 0 < b) :
    ExactPowerRecurrence a b f T := by
  refine ⟨?_⟩
  intro i
  rw [h_rec.step (b ^ (i + 1))]
  rw [pow_succ_div_base (b := b) (i := i) hb]

theorem exactPowerRecurrence_of_ceilDivideRecurrence
    (a b : ℕ) (f T : ℕ → ℝ)
    (h_rec : CeilDivideRecurrence a b f T) (hb : 0 < b) :
    ExactPowerRecurrence a b f T := by
  refine ⟨?_⟩
  intro i
  rw [h_rec.step (b ^ (i + 1))]
  rw [pow_succ_add_pred_div_base (b := b) (i := i) hb]

Eventually every large input can be bounded above by a large enough exact power, with the comparison scale at that power controlled by the scale at the original input.

def EventuallyPowerUpperSandwich (b : ℕ) (g : ℕ → ℝ) : Prop :=
  ∃ A : ℝ, 0 < A ∧
    ∀ i₀ : ℕ, ∃ n₀ : ℕ, ∀ n, n ≥ n₀ →
      ∃ i : ℕ, i ≥ i₀ ∧ n ≤ b ^ i ∧ |g (b ^ i)| ≤ A * |g n|

Eventually every large input has a large enough exact power below it, with the comparison scale at the original input controlled by the scale at that power.

def EventuallyPowerLowerSandwich (b : ℕ) (g : ℕ → ℝ) : Prop :=
  ∃ A : ℝ, 0 < A ∧
    ∀ i₀ : ℕ, ∃ n₀ : ℕ, ∀ n, n ≥ n₀ →
      ∃ i : ℕ, i ≥ i₀ ∧ b ^ i ≤ n ∧ |g n| ≤ A * |g (b ^ i)|

Adjacent powers generate sandwich witnesses

Every positive natural input lies between adjacent powers of a base b > 1. This is the arithmetic step that CLRS uses implicitly when it extends exact-power recurrence bounds to all input sizes.

theorem powerInterval_of_pos (b n : ℕ) (hb : 1 < b) (hn : n ≠ 0) :
    b ^ Nat.log b n ≤ n ∧ n < b ^ (Nat.log b n + 1) :=
  ⟨Nat.pow_log_le_self b hn, by
    simpa [Nat.succ_eq_add_one] using Nat.lt_pow_succ_log_self hb n⟩

Mapping the adjacent-power interval through a monotone natural-valued cost gives the corresponding cost sandwich.

theorem monotone_power_sandwich {T : ℕ → ℕ} (hT : Monotone T)
    (b n : ℕ) (hb : 1 < b) (hn : n ≠ 0) :
    T (b ^ Nat.log b n) ≤ T n ∧
      T n ≤ T (b ^ (Nat.log b n + 1)) := by
  rcases powerInterval_of_pos b n hb hn with ⟨hlo, hhi⟩
  exact ⟨hT hlo, hT (Nat.le_of_lt hhi)⟩

private theorem power_log_ge_step_threshold
    {b step n j₀ : ℕ} (hb : 1 < b)
    (hj₀_step : Nat.log b step + 1 ≤ j₀)
    (hj₀_log : j₀ ≤ Nat.log b n) :
    step ≤ b ^ Nat.log b n := by
  have hb_pos : 0 < b := Nat.lt_trans Nat.zero_lt_one hb
  have hstep_lt : step < b ^ (Nat.log b step + 1) :=
    Nat.lt_pow_succ_log_self hb step
  have hpow_le :
      b ^ (Nat.log b step + 1) ≤ b ^ Nat.log b n :=
    Nat.pow_le_pow_right hb_pos (Nat.le_trans hj₀_step hj₀_log)
  exact Nat.le_trans (Nat.le_of_lt hstep_lt) hpow_le

Monotone scales with eventual one-step control automatically satisfy the upper power-sandwich hypothesis: for every large n, choose the next exact power above it.


theorem eventuallyPowerUpperSandwich_of_powerStep
    (b : ℕ) (g : ℕ → ℝ) (hb : 1 < b)
    (hg_mono : MonotoneAbs g)
    (hg_step : EventuallyPowerStepBound b g) :
    EventuallyPowerUpperSandwich b g := by
  rcases hg_step with ⟨A, hA_pos, step₀, hstep⟩
  refine ⟨A, hA_pos, ?_⟩
  intro i₀
  let j₀ := max i₀ (Nat.log b step₀ + 1)
  refine ⟨b ^ j₀, ?_⟩
  intro n hn
  have hb_pos : 0 < b := Nat.lt_trans Nat.zero_lt_one hb
  have hn_ne_zero : n ≠ 0 := by
    have hpow_pos : 0 < b ^ j₀ := pow_pos hb_pos j₀
    exact Nat.ne_of_gt (Nat.lt_of_lt_of_le hpow_pos hn)
  have hj₀_log : j₀ ≤ Nat.log b n :=
    Nat.le_log_of_pow_le hb hn
  let i := Nat.log b n + 1
  refine ⟨i, ?_, ?_, ?_⟩
  · exact Nat.le_trans (Nat.le_max_left i₀ (Nat.log b step₀ + 1))
      (Nat.le_trans hj₀_log (Nat.le_succ _))
  · exact Nat.le_of_lt (powerInterval_of_pos b n hb hn_ne_zero).2
  · have hstep_arg : step₀ ≤ b ^ Nat.log b n :=
      power_log_ge_step_threshold (b := b) (step := step₀) (n := n)
        (j₀ := j₀) hb (Nat.le_max_right _ _) hj₀_log
    have hlocal := hstep (b ^ Nat.log b n) hstep_arg
    have hmono_to_n : |g (b ^ Nat.log b n)| ≤ |g n| :=
      hg_mono (Nat.pow_log_le_self b hn_ne_zero)
    calc
      |g (b ^ i)| = |g (b * b ^ Nat.log b n)| := by
        simp [i, pow_succ, Nat.mul_comm]
      _ ≤ A * |g (b ^ Nat.log b n)| := hlocal
      _ ≤ A * |g n| := by
        gcongr

Monotone scales with eventual one-step control automatically satisfy the lower power-sandwich hypothesis: for every large n, choose the previous exact power below it.


theorem eventuallyPowerLowerSandwich_of_powerStep
    (b : ℕ) (g : ℕ → ℝ) (hb : 1 < b)
    (hg_mono : MonotoneAbs g)
    (hg_step : EventuallyPowerStepBound b g) :
    EventuallyPowerLowerSandwich b g := by
  rcases hg_step with ⟨A, hA_pos, step₀, hstep⟩
  refine ⟨A, hA_pos, ?_⟩
  intro i₀
  let j₀ := max i₀ (Nat.log b step₀ + 1)
  refine ⟨b ^ j₀, ?_⟩
  intro n hn
  have hb_pos : 0 < b := Nat.lt_trans Nat.zero_lt_one hb
  have hn_ne_zero : n ≠ 0 := by
    have hpow_pos : 0 < b ^ j₀ := pow_pos hb_pos j₀
    exact Nat.ne_of_gt (Nat.lt_of_lt_of_le hpow_pos hn)
  have hj₀_log : j₀ ≤ Nat.log b n :=
    Nat.le_log_of_pow_le hb hn
  let i := Nat.log b n
  refine ⟨i, ?_, ?_, ?_⟩
  · exact Nat.le_trans (Nat.le_max_left i₀ (Nat.log b step₀ + 1)) hj₀_log
  · exact (powerInterval_of_pos b n hb hn_ne_zero).1
  · have hstep_arg : step₀ ≤ b ^ Nat.log b n :=
      power_log_ge_step_threshold (b := b) (step := step₀) (n := n)
        (j₀ := j₀) hb (Nat.le_max_right _ _) hj₀_log
    have hlocal := hstep (b ^ Nat.log b n) hstep_arg
    have hn_le_next :
        n ≤ b ^ (Nat.log b n + 1) :=
      Nat.le_of_lt (powerInterval_of_pos b n hb hn_ne_zero).2
    calc
      |g n| ≤ |g (b ^ (Nat.log b n + 1))| := hg_mono hn_le_next
      _ = |g (b * b ^ Nat.log b n)| := by
        simp [pow_succ, Nat.mul_comm]
      _ ≤ A * |g (b ^ Nat.log b n)| := hlocal
      _ = A * |g (b ^ i)| := by simp [i]

Exact powers to all inputs

Transfer an exact-power big-O bound to all natural inputs, provided the cost is monotone in absolute value and the comparison function admits an eventual upper power sandwich.

theorem allInput_bigO_of_power_upper_sandwich
    (b : ℕ) (T g : ℕ → ℝ)
    (hT_mono : MonotoneAbs T)
    (hg_sandwich : EventuallyPowerUpperSandwich b g)
    (h_power :
      Chapter03.isBigO
        (fun i : ℕ => T (b ^ i))
        (fun i : ℕ => g (b ^ i))) :
    Chapter03.isBigO T g := by
  rcases (Chapter03.isBigO_iff
      (fun i : ℕ => T (b ^ i))
      (fun i : ℕ => g (b ^ i))).mp h_power with
    ⟨C, hC_pos, i₀, hC⟩
  rcases hg_sandwich with ⟨A, hA_pos, hA⟩
  rcases hA i₀ with ⟨n₀, hn₀⟩
  refine (Chapter03.isBigO_iff T g).mpr ?_
  refine ⟨C * A, mul_pos hC_pos hA_pos, n₀, ?_⟩
  intro n hn
  rcases hn₀ n hn with ⟨i, hi_ge, hn_le_pow, hg⟩
  calc
    |T n| ≤ |T (b ^ i)| := hT_mono hn_le_pow
    _ ≤ C * |g (b ^ i)| := hC i hi_ge
    _ ≤ C * (A * |g n|) := by
      gcongr
    _ = (C * A) * |g n| := by ring

Transfer an exact-power big-Omega bound to all natural inputs, provided the cost is monotone in absolute value and the comparison function admits an eventual lower power sandwich.

theorem allInput_bigOmega_of_power_lower_sandwich
    (b : ℕ) (T g : ℕ → ℝ)
    (hT_mono : MonotoneAbs T)
    (hg_sandwich : EventuallyPowerLowerSandwich b g)
    (h_power :
      Chapter03.isBigOmega
        (fun i : ℕ => T (b ^ i))
        (fun i : ℕ => g (b ^ i))) :
    Chapter03.isBigOmega T g := by
  rcases (Chapter03.isBigOmega_iff
      (fun i : ℕ => T (b ^ i))
      (fun i : ℕ => g (b ^ i))).mp h_power with
    ⟨c, hc_pos, i₀, hc⟩
  rcases hg_sandwich with ⟨A, hA_pos, hA⟩
  rcases hA i₀ with ⟨n₀, hn₀⟩
  refine (Chapter03.isBigOmega_iff T g).mpr ?_
  refine ⟨c / A, div_pos hc_pos hA_pos, n₀, ?_⟩
  intro n hn
  rcases hn₀ n hn with ⟨i, hi_ge, hpow_le_n, hg⟩
  have hA_ne_zero : A ≠ 0 := ne_of_gt hA_pos
  have hdiv_nonneg : 0 ≤ c / A := (div_pos hc_pos hA_pos).le
  calc
    (c / A) * |g n| ≤ (c / A) * (A * |g (b ^ i)|) := by
      gcongr
    _ = c * |g (b ^ i)| := by
      field_simp [hA_ne_zero]
    _ ≤ |T (b ^ i)| := hc i hi_ge
    _ ≤ |T n| := hT_mono hpow_le_n

Transfer an exact-power big-Theta bound to all natural inputs using both power sandwich directions.

theorem allInput_bigTheta_of_power_sandwich
    (b : ℕ) (T g : ℕ → ℝ)
    (hT_mono : MonotoneAbs T)
    (hg_upper : EventuallyPowerUpperSandwich b g)
    (hg_lower : EventuallyPowerLowerSandwich b g)
    (h_power :
      Chapter03.isBigTheta
        (fun i : ℕ => T (b ^ i))
        (fun i : ℕ => g (b ^ i))) :
    Chapter03.isBigTheta T g := by
  exact
    ⟨allInput_bigO_of_power_upper_sandwich b T g hT_mono hg_upper h_power.1,
      allInput_bigOmega_of_power_lower_sandwich b T g hT_mono hg_lower h_power.2⟩

Direct all-input transfer theorem from exact powers using adjacent-power regularity of the comparison scale. This packages the CLRS proof step: choose the exact power immediately below or above an arbitrary input n, use monotonicity for T, and use one-step regularity for g.

theorem allInput_bigTheta_of_powerStep
    (b : ℕ) (T g : ℕ → ℝ) (hb : 1 < b)
    (hT_mono : MonotoneAbs T)
    (hg_mono : MonotoneAbs g)
    (hg_step : EventuallyPowerStepBound b g)
    (h_power :
      Chapter03.isBigTheta
        (fun i : ℕ => T (b ^ i))
        (fun i : ℕ => g (b ^ i))) :
    Chapter03.isBigTheta T g :=
  allInput_bigTheta_of_power_sandwich b T g hT_mono
    (eventuallyPowerUpperSandwich_of_powerStep b g hb hg_mono hg_step)
    (eventuallyPowerLowerSandwich_of_powerStep b g hb hg_mono hg_step)
    h_power

Concrete all-input bridge for the first exact-power Master scale. If the exact-power sequence T(b^i) is Θ(a^i) and the cost is monotone in absolute value, then the all-input cost is Θ(a^(⌊log_b n⌋)), represented by criticalPowerScale.

This theorem is intentionally discrete: a later analytic comparison can relate criticalPowerScale to n^(log_b a) when that real-valued scale is needed.


theorem allInput_bigTheta_of_criticalPowerScale
    (a b : ℕ) (T : ℕ → ℝ) (ha : 1 ≤ a) (hb : 1 < b)
    (hT_mono : MonotoneAbs T)
    (h_power :
      Chapter03.isBigTheta
        (fun i : ℕ => T (b ^ i))
        (fun i : ℕ => (a : ℝ) ^ i)) :
    Chapter03.isBigTheta T (criticalPowerScale a b) := by
  have h_power_scale :
      Chapter03.isBigTheta
        (fun i : ℕ => T (b ^ i))
        (fun i : ℕ => criticalPowerScale a b (b ^ i)) := by
    have hscale :
        (fun i : ℕ => criticalPowerScale a b (b ^ i)) =
          (fun i : ℕ => (a : ℝ) ^ i) := by
      funext i
      exact criticalPowerScale_exactPower a b i hb
    rw [hscale]
    exact h_power
  exact allInput_bigTheta_of_powerStep b T (criticalPowerScale a b) hb
    hT_mono
    (criticalPowerScale_monotoneAbs a b ha)
    (criticalPowerScale_powerStepBound a b ha hb)
    h_power_scale



theorem allInput_bigTheta_of_criticalPowerLogScale
    (a b : ℕ) (T : ℕ → ℝ) (ha : 1 ≤ a) (hb : 1 < b)
    (hT_mono : MonotoneAbs T)
    (h_power :
      Chapter03.isBigTheta
        (fun i : ℕ => T (b ^ i))
        (fun i : ℕ => ((i : ℝ) + 1) * ((a : ℝ) ^ i))) :
    Chapter03.isBigTheta T (criticalPowerLogScale a b) := by
  have h_power_scale :
      Chapter03.isBigTheta
        (fun i : ℕ => T (b ^ i))
        (fun i : ℕ => criticalPowerLogScale a b (b ^ i)) := by
    have hscale :
        (fun i : ℕ => criticalPowerLogScale a b (b ^ i)) =
          (fun i : ℕ => ((i : ℝ) + 1) * ((a : ℝ) ^ i)) := by
      funext i
      exact criticalPowerLogScale_exactPower a b i hb
    rw [hscale]
    exact h_power
  exact allInput_bigTheta_of_powerStep b T (criticalPowerLogScale a b) hb
    hT_mono
    (criticalPowerLogScale_monotoneAbs a b ha)
    (criticalPowerLogScale_powerStepBound a b ha hb)
    h_power_scale



theorem allInput_bigTheta_of_tailDominatedScale
    (a b : ℕ) (f T : ℕ → ℝ) (hb : 1 < b)
    (hT_mono : MonotoneAbs T)
    (hscale_mono : MonotoneAbs (tailDominatedScale a b f))
    (hscale_step : EventuallyPowerStepBound b (tailDominatedScale a b f))
    (h_power :
      Chapter03.isBigTheta
        (fun i : ℕ => T (b ^ i))
        (fun i : ℕ =>
          (if i = 0 then 1 else normalizedForcing a b f (i - 1)) *
            ((a : ℝ) ^ i))) :
    Chapter03.isBigTheta T (tailDominatedScale a b f) := by
  have h_power_scale :
      Chapter03.isBigTheta
        (fun i : ℕ => T (b ^ i))
        (fun i : ℕ => tailDominatedScale a b f (b ^ i)) := by
    have hscale :
        (fun i : ℕ => tailDominatedScale a b f (b ^ i)) =
          (fun i : ℕ =>
            (if i = 0 then 1 else normalizedForcing a b f (i - 1)) *
              ((a : ℝ) ^ i)) := by
      funext i
      exact tailDominatedScale_exactPower a b f i hb
    rw [hscale]
    exact h_power
  exact allInput_bigTheta_of_powerStep b T (tailDominatedScale a b f) hb
    hT_mono hscale_mono hscale_step h_power_scale

Packaged all-input Master case 1 wrappers

All-input wrapper for exact-power Master case 1, using the discrete critical scale. This packages three already-proved layers:

exact-power Master case 1;
adjacent-power all-input transfer;
the concrete scale criticalPowerScale.


theorem exactPower_allInput_masterCase1_criticalPowerScale
    (a b : ℕ) (f T : ℕ → ℝ)
    (h_rec : ExactPowerRecurrence a b f T)
    (ha : 1 ≤ a) (hb : 1 < b)
    (hT_mono : MonotoneAbs T)
    (h_base_pos : 0 < normalizedValue a b T 0)
    (h_term_nonneg : ∀ k, 0 ≤ normalizedForcing a b f k)
    {r C : ℝ} (hr_nonneg : 0 ≤ r) (hr_lt_one : r < 1) (hC_pos : 0 < C)
    (h_term_upper : ∀ k, normalizedForcing a b f k ≤ C * r ^ k) :
    Chapter03.isBigTheta T (criticalPowerScale a b) := by
  have ha_pos : 0 < (a : ℝ) := by
    exact_mod_cast Nat.lt_of_lt_of_le Nat.zero_lt_one ha
  exact allInput_bigTheta_of_criticalPowerScale a b T ha hb hT_mono
    (master_case1_geometric a b f T h_rec ha_pos h_base_pos h_term_nonneg
      hr_nonneg hr_lt_one hC_pos h_term_upper)

Floor-division all-input Master case 1 wrapper. The theorem starts from the all-input recurrence T(n) = a T(⌊n/b⌋) + f(n), extracts the exact-power recurrence, applies exact-power case 1, and transfers the result back to every natural input.

theorem floorDivide_allInput_masterCase1_criticalPowerScale
    (a b : ℕ) (f T : ℕ → ℝ)
    (h_rec : FloorDivideRecurrence a b f T)
    (ha : 1 ≤ a) (hb : 1 < b)
    (hT_mono : MonotoneAbs T)
    (h_base_pos : 0 < normalizedValue a b T 0)
    (h_term_nonneg : ∀ k, 0 ≤ normalizedForcing a b f k)
    {r C : ℝ} (hr_nonneg : 0 ≤ r) (hr_lt_one : r < 1) (hC_pos : 0 < C)
    (h_term_upper : ∀ k, normalizedForcing a b f k ≤ C * r ^ k) :
    Chapter03.isBigTheta T (criticalPowerScale a b) := by
  have hb_pos : 0 < b := Nat.lt_trans Nat.zero_lt_one hb
  exact exactPower_allInput_masterCase1_criticalPowerScale a b f T
    (exactPowerRecurrence_of_floorDivideRecurrence a b f T h_rec hb_pos)
    ha hb hT_mono h_base_pos h_term_nonneg hr_nonneg hr_lt_one hC_pos
    h_term_upper

Ceiling-division all-input Master case 1 wrapper. This is the ceiling analogue of floorDivide_allInput_masterCase1_criticalPowerScale, using the natural-number encoding ⌈n/b⌉ = (n + b - 1) / b.

theorem ceilDivide_allInput_masterCase1_criticalPowerScale
    (a b : ℕ) (f T : ℕ → ℝ)
    (h_rec : CeilDivideRecurrence a b f T)
    (ha : 1 ≤ a) (hb : 1 < b)
    (hT_mono : MonotoneAbs T)
    (h_base_pos : 0 < normalizedValue a b T 0)
    (h_term_nonneg : ∀ k, 0 ≤ normalizedForcing a b f k)
    {r C : ℝ} (hr_nonneg : 0 ≤ r) (hr_lt_one : r < 1) (hC_pos : 0 < C)
    (h_term_upper : ∀ k, normalizedForcing a b f k ≤ C * r ^ k) :
    Chapter03.isBigTheta T (criticalPowerScale a b) := by
  have hb_pos : 0 < b := Nat.lt_trans Nat.zero_lt_one hb
  exact exactPower_allInput_masterCase1_criticalPowerScale a b f T
    (exactPowerRecurrence_of_ceilDivideRecurrence a b f T h_rec hb_pos)
    ha hb hT_mono h_base_pos h_term_nonneg hr_nonneg hr_lt_one hC_pos
    h_term_upper

Exact-power all-input Master case 1 stated in the textbook real-log scale n^(log_b a).

theorem exactPower_allInput_masterCase1_realLogScale
    (a b : ℕ) (f T : ℕ → ℝ)
    (h_rec : ExactPowerRecurrence a b f T)
    (ha : 1 ≤ a) (hb : 1 < b)
    (hT_mono : MonotoneAbs T)
    (h_base_pos : 0 < normalizedValue a b T 0)
    (h_term_nonneg : ∀ k, 0 ≤ normalizedForcing a b f k)
    {r C : ℝ} (hr_nonneg : 0 ≤ r) (hr_lt_one : r < 1) (hC_pos : 0 < C)
    (h_term_upper : ∀ k, normalizedForcing a b f k ≤ C * r ^ k) :
    Chapter03.isBigTheta T (realLogScale a b) := by
  exact Chapter03.isBigTheta_trans
    (exactPower_allInput_masterCase1_criticalPowerScale a b f T h_rec
      ha hb hT_mono h_base_pos h_term_nonneg hr_nonneg hr_lt_one hC_pos
      h_term_upper)
    (criticalPowerScale_isBigTheta_realLogScale a b ha hb)

Floor-division all-input Master case 1 stated in the textbook real-log scale n^(log_b a).

theorem floorDivide_allInput_masterCase1_realLogScale
    (a b : ℕ) (f T : ℕ → ℝ)
    (h_rec : FloorDivideRecurrence a b f T)
    (ha : 1 ≤ a) (hb : 1 < b)
    (hT_mono : MonotoneAbs T)
    (h_base_pos : 0 < normalizedValue a b T 0)
    (h_term_nonneg : ∀ k, 0 ≤ normalizedForcing a b f k)
    {r C : ℝ} (hr_nonneg : 0 ≤ r) (hr_lt_one : r < 1) (hC_pos : 0 < C)
    (h_term_upper : ∀ k, normalizedForcing a b f k ≤ C * r ^ k) :
    Chapter03.isBigTheta T (realLogScale a b) := by
  exact Chapter03.isBigTheta_trans
    (floorDivide_allInput_masterCase1_criticalPowerScale a b f T h_rec
      ha hb hT_mono h_base_pos h_term_nonneg hr_nonneg hr_lt_one hC_pos
      h_term_upper)
    (criticalPowerScale_isBigTheta_realLogScale a b ha hb)

Ceiling-division all-input Master case 1 stated in the textbook real-log scale n^(log_b a).

theorem ceilDivide_allInput_masterCase1_realLogScale
    (a b : ℕ) (f T : ℕ → ℝ)
    (h_rec : CeilDivideRecurrence a b f T)
    (ha : 1 ≤ a) (hb : 1 < b)
    (hT_mono : MonotoneAbs T)
    (h_base_pos : 0 < normalizedValue a b T 0)
    (h_term_nonneg : ∀ k, 0 ≤ normalizedForcing a b f k)
    {r C : ℝ} (hr_nonneg : 0 ≤ r) (hr_lt_one : r < 1) (hC_pos : 0 < C)
    (h_term_upper : ∀ k, normalizedForcing a b f k ≤ C * r ^ k) :
    Chapter03.isBigTheta T (realLogScale a b) := by
  exact Chapter03.isBigTheta_trans
    (ceilDivide_allInput_masterCase1_criticalPowerScale a b f T h_rec
      ha hb hT_mono h_base_pos h_term_nonneg hr_nonneg hr_lt_one hC_pos
      h_term_upper)
    (criticalPowerScale_isBigTheta_realLogScale a b ha hb)

Exact-power all-input Master case 1 specialized to a = b^p, with the result stated directly as Θ(n^p).

theorem exactPower_allInput_masterCase1_polynomialScale
    (b p : ℕ) (f T : ℕ → ℝ)
    (h_rec : ExactPowerRecurrence (b ^ p) b f T)
    (hb : 1 < b)
    (hT_mono : MonotoneAbs T)
    (h_base_pos : 0 < normalizedValue (b ^ p) b T 0)
    (h_term_nonneg : ∀ k, 0 ≤ normalizedForcing (b ^ p) b f k)
    {r C : ℝ} (hr_nonneg : 0 ≤ r) (hr_lt_one : r < 1) (hC_pos : 0 < C)
    (h_term_upper : ∀ k, normalizedForcing (b ^ p) b f k ≤ C * r ^ k) :
    Chapter03.isBigTheta T (polynomialScale p) := by
  exact Chapter03.isBigTheta_trans
    (exactPower_allInput_masterCase1_criticalPowerScale (b ^ p) b f T h_rec
      (one_le_base_pow_of_one_lt b p hb) hb hT_mono h_base_pos
      h_term_nonneg hr_nonneg hr_lt_one hC_pos h_term_upper)
    (criticalPowerScale_isBigTheta_polynomialScale b p hb)

Floor-division all-input Master case 1 specialized to a = b^p, with the result stated directly as Θ(n^p).

theorem floorDivide_allInput_masterCase1_polynomialScale
    (b p : ℕ) (f T : ℕ → ℝ)
    (h_rec : FloorDivideRecurrence (b ^ p) b f T)
    (hb : 1 < b)
    (hT_mono : MonotoneAbs T)
    (h_base_pos : 0 < normalizedValue (b ^ p) b T 0)
    (h_term_nonneg : ∀ k, 0 ≤ normalizedForcing (b ^ p) b f k)
    {r C : ℝ} (hr_nonneg : 0 ≤ r) (hr_lt_one : r < 1) (hC_pos : 0 < C)
    (h_term_upper : ∀ k, normalizedForcing (b ^ p) b f k ≤ C * r ^ k) :
    Chapter03.isBigTheta T (polynomialScale p) := by
  exact Chapter03.isBigTheta_trans
    (floorDivide_allInput_masterCase1_criticalPowerScale (b ^ p) b f T h_rec
      (one_le_base_pow_of_one_lt b p hb) hb hT_mono h_base_pos
      h_term_nonneg hr_nonneg hr_lt_one hC_pos h_term_upper)
    (criticalPowerScale_isBigTheta_polynomialScale b p hb)

Ceiling-division all-input Master case 1 specialized to a = b^p, with the result stated directly as Θ(n^p).

theorem ceilDivide_allInput_masterCase1_polynomialScale
    (b p : ℕ) (f T : ℕ → ℝ)
    (h_rec : CeilDivideRecurrence (b ^ p) b f T)
    (hb : 1 < b)
    (hT_mono : MonotoneAbs T)
    (h_base_pos : 0 < normalizedValue (b ^ p) b T 0)
    (h_term_nonneg : ∀ k, 0 ≤ normalizedForcing (b ^ p) b f k)
    {r C : ℝ} (hr_nonneg : 0 ≤ r) (hr_lt_one : r < 1) (hC_pos : 0 < C)
    (h_term_upper : ∀ k, normalizedForcing (b ^ p) b f k ≤ C * r ^ k) :
    Chapter03.isBigTheta T (polynomialScale p) := by
  exact Chapter03.isBigTheta_trans
    (ceilDivide_allInput_masterCase1_criticalPowerScale (b ^ p) b f T h_rec
      (one_le_base_pow_of_one_lt b p hb) hb hT_mono h_base_pos
      h_term_nonneg hr_nonneg hr_lt_one hC_pos h_term_upper)
    (criticalPowerScale_isBigTheta_polynomialScale b p hb)

Packaged all-input Master case 2 wrappers

All-input wrapper for exact-power Master case 2, using the discrete criticalPowerLogScale. This is the all-input analogue of the exact power theorem T(b^i) = Θ((i+1)a^i).


theorem exactPower_allInput_masterCase2_criticalPowerLogScale
    (a b : ℕ) (f T : ℕ → ℝ)
    (h_rec : ExactPowerRecurrence a b f T)
    (ha : 1 ≤ a) (hb : 1 < b)
    (hT_mono : MonotoneAbs T)
    (h_base_nonneg : 0 ≤ normalizedValue a b T 0)
    {c C : ℝ} (hc_pos : 0 < c) (hC_pos : 0 < C)
    (h_term_lower : ∀ k, c ≤ normalizedForcing a b f k)
    (h_term_upper : ∀ k, normalizedForcing a b f k ≤ C) :
    Chapter03.isBigTheta T (criticalPowerLogScale a b) := by
  have ha_pos : 0 < (a : ℝ) := by
    exact_mod_cast Nat.lt_of_lt_of_le Nat.zero_lt_one ha
  exact allInput_bigTheta_of_criticalPowerLogScale a b T ha hb hT_mono
    (master_case2_constant_forcing a b f T h_rec ha_pos h_base_nonneg
      hc_pos hC_pos h_term_lower h_term_upper)

All-input wrapper for Master case 2 with a polylog factor: if the normalized forcing grows polynomially, c·j^k ≤ normalizedForcing ≤ C·j^k, then T is Θ of the discrete polylog scale (⌊log_b n⌋+1)^(k+1)·a^(⌊log_b n⌋). For f(n) = Θ(n^(log_b a)·log^k n) this is the standard textbook extension T(n) = Θ(n^(log_b a)·log^(k+1) n); the k = 0 case recovers exactPower_allInput_masterCase2_criticalPowerLogScale.


theorem master_case2_polylog_forcing_all_input (a b k : ℕ) (f T : ℕ → ℝ)
    (h_rec : ExactPowerRecurrence a b f T)
    (ha : 1 ≤ a) (hb : 1 < b)
    (hT_mono : MonotoneAbs T)
    (h_base_nonneg : 0 ≤ normalizedValue a b T 0)
    {c C : ℝ} (hc_pos : 0 < c) (hC_pos : 0 < C)
    (h_term_lower : ∀ j : ℕ, c * (j : ℝ) ^ k ≤ normalizedForcing a b f j)
    (h_term_upper : ∀ j : ℕ, normalizedForcing a b f j ≤ C * (j : ℝ) ^ k) :
    Chapter03.isBigTheta T (criticalPowerLogPolylogScale a b k) := by
  have ha_pos : 0 < (a : ℝ) := by
    exact_mod_cast Nat.lt_of_lt_of_le Nat.zero_lt_one ha
  have h_power : Chapter03.isBigTheta
      (fun i : ℕ => T (b ^ i))
      (fun i : ℕ => criticalPowerLogPolylogScale a b k (b ^ i)) := by
    have h_exact := master_case2_polylog_forcing a b k f T h_rec ha_pos h_base_nonneg
      hc_pos hC_pos h_term_lower h_term_upper
    convert h_exact using 1
    funext i
    exact criticalPowerLogPolylogScale_exactPower a b k i hb
  exact allInput_bigTheta_of_powerStep b T (criticalPowerLogPolylogScale a b k) hb
    hT_mono (criticalPowerLogPolylogScale_monotoneAbs a b k ha)
    (criticalPowerLogPolylogScale_powerStepBound a b k ha hb) h_power

Floor-division all-input Master case 2 wrapper. It extracts the exact-power recurrence from T(n) = a T(⌊n/b⌋) + f(n), applies exact-power case 2, and transfers the result to every natural input through the discrete log scale.

theorem floorDivide_allInput_masterCase2_criticalPowerLogScale
    (a b : ℕ) (f T : ℕ → ℝ)
    (h_rec : FloorDivideRecurrence a b f T)
    (ha : 1 ≤ a) (hb : 1 < b)
    (hT_mono : MonotoneAbs T)
    (h_base_nonneg : 0 ≤ normalizedValue a b T 0)
    {c C : ℝ} (hc_pos : 0 < c) (hC_pos : 0 < C)
    (h_term_lower : ∀ k, c ≤ normalizedForcing a b f k)
    (h_term_upper : ∀ k, normalizedForcing a b f k ≤ C) :
    Chapter03.isBigTheta T (criticalPowerLogScale a b) := by
  have hb_pos : 0 < b := Nat.lt_trans Nat.zero_lt_one hb
  exact exactPower_allInput_masterCase2_criticalPowerLogScale a b f T
    (exactPowerRecurrence_of_floorDivideRecurrence a b f T h_rec hb_pos)
    ha hb hT_mono h_base_nonneg hc_pos hC_pos h_term_lower h_term_upper

Ceiling-division all-input Master case 2 wrapper. This is the ceiling analogue of floorDivide_allInput_masterCase2_criticalPowerLogScale.

theorem ceilDivide_allInput_masterCase2_criticalPowerLogScale
    (a b : ℕ) (f T : ℕ → ℝ)
    (h_rec : CeilDivideRecurrence a b f T)
    (ha : 1 ≤ a) (hb : 1 < b)
    (hT_mono : MonotoneAbs T)
    (h_base_nonneg : 0 ≤ normalizedValue a b T 0)
    {c C : ℝ} (hc_pos : 0 < c) (hC_pos : 0 < C)
    (h_term_lower : ∀ k, c ≤ normalizedForcing a b f k)
    (h_term_upper : ∀ k, normalizedForcing a b f k ≤ C) :
    Chapter03.isBigTheta T (criticalPowerLogScale a b) := by
  have hb_pos : 0 < b := Nat.lt_trans Nat.zero_lt_one hb
  exact exactPower_allInput_masterCase2_criticalPowerLogScale a b f T
    (exactPowerRecurrence_of_ceilDivideRecurrence a b f T h_rec hb_pos)
    ha hb hT_mono h_base_nonneg hc_pos hC_pos h_term_lower h_term_upper

Exact-power all-input Master case 2 stated in the textbook real-log-log scale n^(log_b a) log n.

theorem exactPower_allInput_masterCase2_realLogLogScale
    (a b : ℕ) (f T : ℕ → ℝ)
    (h_rec : ExactPowerRecurrence a b f T)
    (ha : 1 ≤ a) (hb : 1 < b)
    (hT_mono : MonotoneAbs T)
    (h_base_nonneg : 0 ≤ normalizedValue a b T 0)
    {c C : ℝ} (hc_pos : 0 < c) (hC_pos : 0 < C)
    (h_term_lower : ∀ k, c ≤ normalizedForcing a b f k)
    (h_term_upper : ∀ k, normalizedForcing a b f k ≤ C) :
    Chapter03.isBigTheta T (realLogLogScale a b) := by
  exact Chapter03.isBigTheta_trans
    (exactPower_allInput_masterCase2_criticalPowerLogScale a b f T h_rec
      ha hb hT_mono h_base_nonneg hc_pos hC_pos h_term_lower h_term_upper)
    (criticalPowerLogScale_isBigTheta_realLogLogScale a b ha hb)

Floor-division all-input Master case 2 stated in the textbook real-log-log scale n^(log_b a) log n.

theorem floorDivide_allInput_masterCase2_realLogLogScale
    (a b : ℕ) (f T : ℕ → ℝ)
    (h_rec : FloorDivideRecurrence a b f T)
    (ha : 1 ≤ a) (hb : 1 < b)
    (hT_mono : MonotoneAbs T)
    (h_base_nonneg : 0 ≤ normalizedValue a b T 0)
    {c C : ℝ} (hc_pos : 0 < c) (hC_pos : 0 < C)
    (h_term_lower : ∀ k, c ≤ normalizedForcing a b f k)
    (h_term_upper : ∀ k, normalizedForcing a b f k ≤ C) :
    Chapter03.isBigTheta T (realLogLogScale a b) := by
  exact Chapter03.isBigTheta_trans
    (floorDivide_allInput_masterCase2_criticalPowerLogScale a b f T h_rec
      ha hb hT_mono h_base_nonneg hc_pos hC_pos h_term_lower h_term_upper)
    (criticalPowerLogScale_isBigTheta_realLogLogScale a b ha hb)

Ceiling-division all-input Master case 2 stated in the textbook real-log-log scale n^(log_b a) log n.

theorem ceilDivide_allInput_masterCase2_realLogLogScale
    (a b : ℕ) (f T : ℕ → ℝ)
    (h_rec : CeilDivideRecurrence a b f T)
    (ha : 1 ≤ a) (hb : 1 < b)
    (hT_mono : MonotoneAbs T)
    (h_base_nonneg : 0 ≤ normalizedValue a b T 0)
    {c C : ℝ} (hc_pos : 0 < c) (hC_pos : 0 < C)
    (h_term_lower : ∀ k, c ≤ normalizedForcing a b f k)
    (h_term_upper : ∀ k, normalizedForcing a b f k ≤ C) :
    Chapter03.isBigTheta T (realLogLogScale a b) := by
  exact Chapter03.isBigTheta_trans
    (ceilDivide_allInput_masterCase2_criticalPowerLogScale a b f T h_rec
      ha hb hT_mono h_base_nonneg hc_pos hC_pos h_term_lower h_term_upper)
    (criticalPowerLogScale_isBigTheta_realLogLogScale a b ha hb)

Exact-power all-input Master case 2 specialized to a = b^p, with the result stated directly as Θ((⌊log_b n⌋+1)n^p).

theorem exactPower_allInput_masterCase2_polynomialLogScale
    (b p : ℕ) (f T : ℕ → ℝ)
    (h_rec : ExactPowerRecurrence (b ^ p) b f T)
    (hb : 1 < b)
    (hT_mono : MonotoneAbs T)
    (h_base_nonneg : 0 ≤ normalizedValue (b ^ p) b T 0)
    {c C : ℝ} (hc_pos : 0 < c) (hC_pos : 0 < C)
    (h_term_lower : ∀ k, c ≤ normalizedForcing (b ^ p) b f k)
    (h_term_upper : ∀ k, normalizedForcing (b ^ p) b f k ≤ C) :
    Chapter03.isBigTheta T (polynomialLogScale b p) := by
  exact Chapter03.isBigTheta_trans
    (exactPower_allInput_masterCase2_criticalPowerLogScale (b ^ p) b f T h_rec
      (one_le_base_pow_of_one_lt b p hb) hb hT_mono h_base_nonneg
      hc_pos hC_pos h_term_lower h_term_upper)
    (criticalPowerLogScale_isBigTheta_polynomialLogScale b p hb)

Floor-division all-input Master case 2 specialized to a = b^p, with the result stated directly as Θ((⌊log_b n⌋+1)n^p).

theorem floorDivide_allInput_masterCase2_polynomialLogScale
    (b p : ℕ) (f T : ℕ → ℝ)
    (h_rec : FloorDivideRecurrence (b ^ p) b f T)
    (hb : 1 < b)
    (hT_mono : MonotoneAbs T)
    (h_base_nonneg : 0 ≤ normalizedValue (b ^ p) b T 0)
    {c C : ℝ} (hc_pos : 0 < c) (hC_pos : 0 < C)
    (h_term_lower : ∀ k, c ≤ normalizedForcing (b ^ p) b f k)
    (h_term_upper : ∀ k, normalizedForcing (b ^ p) b f k ≤ C) :
    Chapter03.isBigTheta T (polynomialLogScale b p) := by
  exact Chapter03.isBigTheta_trans
    (floorDivide_allInput_masterCase2_criticalPowerLogScale (b ^ p) b f T h_rec
      (one_le_base_pow_of_one_lt b p hb) hb hT_mono h_base_nonneg
      hc_pos hC_pos h_term_lower h_term_upper)
    (criticalPowerLogScale_isBigTheta_polynomialLogScale b p hb)

Ceiling-division all-input Master case 2 specialized to a = b^p, with the result stated directly as Θ((⌊log_b n⌋+1)n^p).

theorem ceilDivide_allInput_masterCase2_polynomialLogScale
    (b p : ℕ) (f T : ℕ → ℝ)
    (h_rec : CeilDivideRecurrence (b ^ p) b f T)
    (hb : 1 < b)
    (hT_mono : MonotoneAbs T)
    (h_base_nonneg : 0 ≤ normalizedValue (b ^ p) b T 0)
    {c C : ℝ} (hc_pos : 0 < c) (hC_pos : 0 < C)
    (h_term_lower : ∀ k, c ≤ normalizedForcing (b ^ p) b f k)
    (h_term_upper : ∀ k, normalizedForcing (b ^ p) b f k ≤ C) :
    Chapter03.isBigTheta T (polynomialLogScale b p) := by
  exact Chapter03.isBigTheta_trans
    (ceilDivide_allInput_masterCase2_criticalPowerLogScale (b ^ p) b f T h_rec
      (one_le_base_pow_of_one_lt b p hb) hb hT_mono h_base_nonneg
      hc_pos hC_pos h_term_lower h_term_upper)
    (criticalPowerLogScale_isBigTheta_polynomialLogScale b p hb)

Packaged all-input Master case 3 wrappers

All-input wrapper for exact-power Master case 3, using the discrete tailDominatedScale. The last-forcing scale depends on the concrete forcing function, so its monotonicity and adjacent-power regularity are explicit hypotheses rather than built-in facts.


theorem exactPower_allInput_masterCase3_tailDominatedScale
    (a b : ℕ) (f T : ℕ → ℝ)
    (h_rec : ExactPowerRecurrence a b f T)
    (ha : 1 ≤ a) (hb : 1 < b)
    (hT_mono : MonotoneAbs T)
    (hscale_mono : MonotoneAbs (tailDominatedScale a b f))
    (hscale_step : EventuallyPowerStepBound b (tailDominatedScale a b f))
    (h_base_nonneg : 0 ≤ normalizedValue a b T 0)
    (h_term_nonneg : ∀ k, 0 ≤ normalizedForcing a b f k)
    (h_tail_upper :
      ∃ C : ℝ, 0 < C ∧ ∃ n₀ : ℕ, ∀ i, i ≥ n₀ → 1 ≤ i →
        normalizedValue a b T i ≤ C * normalizedForcing a b f (i - 1)) :
    Chapter03.isBigTheta T (tailDominatedScale a b f) := by
  have ha_pos : 0 < (a : ℝ) := by
    exact_mod_cast Nat.lt_of_lt_of_le Nat.zero_lt_one ha
  exact allInput_bigTheta_of_tailDominatedScale a b f T hb hT_mono
    hscale_mono hscale_step
    (master_case3_tail_dominated a b f T h_rec ha_pos h_base_nonneg
      h_term_nonneg h_tail_upper)

Floor-division all-input Master case 3 wrapper. It extracts the exact-power recurrence from the all-input floor recurrence, applies the tail-dominated exact-power theorem, and transfers the result through tailDominatedScale.

theorem floorDivide_allInput_masterCase3_tailDominatedScale
    (a b : ℕ) (f T : ℕ → ℝ)
    (h_rec : FloorDivideRecurrence a b f T)
    (ha : 1 ≤ a) (hb : 1 < b)
    (hT_mono : MonotoneAbs T)
    (hscale_mono : MonotoneAbs (tailDominatedScale a b f))
    (hscale_step : EventuallyPowerStepBound b (tailDominatedScale a b f))
    (h_base_nonneg : 0 ≤ normalizedValue a b T 0)
    (h_term_nonneg : ∀ k, 0 ≤ normalizedForcing a b f k)
    (h_tail_upper :
      ∃ C : ℝ, 0 < C ∧ ∃ n₀ : ℕ, ∀ i, i ≥ n₀ → 1 ≤ i →
        normalizedValue a b T i ≤ C * normalizedForcing a b f (i - 1)) :
    Chapter03.isBigTheta T (tailDominatedScale a b f) := by
  have hb_pos : 0 < b := Nat.lt_trans Nat.zero_lt_one hb
  exact exactPower_allInput_masterCase3_tailDominatedScale a b f T
    (exactPowerRecurrence_of_floorDivideRecurrence a b f T h_rec hb_pos)
    ha hb hT_mono hscale_mono hscale_step h_base_nonneg h_term_nonneg
    h_tail_upper

Ceiling-division all-input Master case 3 wrapper. This is the ceiling analogue of floorDivide_allInput_masterCase3_tailDominatedScale.

theorem ceilDivide_allInput_masterCase3_tailDominatedScale
    (a b : ℕ) (f T : ℕ → ℝ)
    (h_rec : CeilDivideRecurrence a b f T)
    (ha : 1 ≤ a) (hb : 1 < b)
    (hT_mono : MonotoneAbs T)
    (hscale_mono : MonotoneAbs (tailDominatedScale a b f))
    (hscale_step : EventuallyPowerStepBound b (tailDominatedScale a b f))
    (h_base_nonneg : 0 ≤ normalizedValue a b T 0)
    (h_term_nonneg : ∀ k, 0 ≤ normalizedForcing a b f k)
    (h_tail_upper :
      ∃ C : ℝ, 0 < C ∧ ∃ n₀ : ℕ, ∀ i, i ≥ n₀ → 1 ≤ i →
        normalizedValue a b T i ≤ C * normalizedForcing a b f (i - 1)) :
    Chapter03.isBigTheta T (tailDominatedScale a b f) := by
  have hb_pos : 0 < b := Nat.lt_trans Nat.zero_lt_one hb
  exact exactPower_allInput_masterCase3_tailDominatedScale a b f T
    (exactPowerRecurrence_of_ceilDivideRecurrence a b f T h_rec hb_pos)
    ha hb hT_mono hscale_mono hscale_step h_base_nonneg h_term_nonneg
    h_tail_upper

Case-3 regularity bridge to the textbook `f(n)` scale

The CLRS regularity condition for Master Theorem case 3 (equation (4.13)): a · f(⌊n / b⌋) ≤ c · f(n) for some constant c < 1 and all sufficiently large n. This ensures that the root cost dominates the recurrence tree.

def Case3Regularity (a b : ℕ) (c : ℝ) (f : ℕ → ℝ) (n₀ : ℕ) : Prop :=
  ∀ n, n₀ ≤ n → (a : ℝ) * f (n / b) ≤ c * f n

On exact powers b^i with i ≥ 1, the tail-dominated scale simplifies to the original forcing function f. This is the key observation that connects the discrete case-3 scale to the textbook scale.


theorem tailDominatedScale_eq_f_on_exact_powers (a b : ℕ) (f : ℕ → ℝ)
    (i : ℕ) (hb : 1 < b) (ha_pos : 0 < (a : ℝ)) :
    tailDominatedScale a b f (b ^ i) =
      (if i = 0 then 1 else f (b ^ i)) := by
  rw [tailDominatedScale_exactPower a b f i hb]
  by_cases hi : i = 0
  · simp [hi]
  · have ha_ne_zero : (a : ℝ) ≠ 0 := by linarith
    have hi_pos : 1 ≤ i := Nat.one_le_of_lt (Nat.pos_of_ne_zero hi)
    dsimp [normalizedForcing]
    have h_exp : (i - 1) + 1 = i := Nat.sub_add_cancel hi_pos
    have h_exp_pow : (a : ℝ) ^ ((i - 1) + 1) = (a : ℝ) ^ i := by rw [h_exp]
    have h_exp_f : f (b ^ ((i - 1) + 1)) = f (b ^ i) := by rw [h_exp]
    simp [hi, h_exp, ha_ne_zero]

try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`

private lemma pow_log_le_n_div_b (b n : ℕ) (hb : 1 < b) :
    n / b ≤ b ^ Nat.log b n := by
  have hb_pos : 0 < b := Nat.lt_trans Nat.zero_lt_one hb
  by_cases hn : n < b
  · have hlog : Nat.log b n = 0 :=
      (Nat.log_eq_zero_iff).mpr (Or.inl hn)
    have hn_div : n / b = 0 := Nat.div_eq_of_lt hn
    try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [hlog, hn_div]
  · have h_pow_succ : n < b ^ Nat.log b n * b := by
      have := Nat.lt_pow_succ_log_self hb n
      -- this gives n < b ^ (log b n).succ = b ^ (log b n) * b
      simpa [pow_succ] using this
    -- n < b^i * b, so n / b < b^i by Nat.div_lt_iff_lt_mul
    have h_div_lt : n / b < b ^ Nat.log b n :=
      (Nat.div_lt_iff_lt_mul hb_pos).mpr h_pow_succ
    exact Nat.le_of_lt h_div_lt

Under the CLRS regularity condition, nonnegativity of f, monotonicity, and a one-step growth bound, the tail-dominated discrete scale is Θ(f(n)).

This is the case-3 analogue of criticalPowerScale_isBigTheta_polynomialScale (case 1) and criticalPowerLogScale_isBigTheta_polynomialLogScale (case 2). Together with the existing all-input case-3 wrappers it yields the textbook conclusion T(n) = Θ(f(n)).


theorem tailDominatedScale_isBigTheta_f_of_regularity
    (a b : ℕ) (f : ℕ → ℝ) (c : ℝ)
    (ha : 1 ≤ a) (hb : 1 < b)
    (hc_pos : 0 < c) (hc_lt_one : c < 1)
    (hf_nonneg : ∀ n, 0 ≤ f n)
    (hf_mono : MonotoneAbs f)
    (hf_step : EventuallyPowerStepBound b f)
    (Variable name `h_reg` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false`h_reg : Case3Regularity a b c f n₀) :
    Chapter03.isBigTheta (tailDominatedScale a b f) f := by
  have ha_pos_nat : 0 < a := Nat.lt_of_lt_of_le Nat.zero_lt_one ha
  have ha_pos : 0 < (a : ℝ) := by exact_mod_cast ha_pos_nat
  have ha_nonneg : 0 ≤ (a : ℝ) := by linarith
  have h_abs_f : ∀ n, |f n| = f n := fun n =>
    abs_of_nonneg (hf_nonneg n)
  have h_abs_tds : ∀ n, |tailDominatedScale a b f n| =
      tailDominatedScale a b f n := by
    intro n
    apply abs_of_nonneg
    unfold tailDominatedScale
    have hcp_nonneg : 0 ≤ criticalPowerScale a b n := by
      unfold criticalPowerScale; apply pow_nonneg ha_nonneg
    by_cases hz : Nat.log b n = 0
    · simp [hz]; positivity
    · have h_nf_nonneg : 0 ≤ normalizedForcing a b f (Nat.log b n - 1) := by
        unfold normalizedForcing
        refine div_nonneg (hf_nonneg _) (pow_nonneg ha_nonneg _)
      simp [hz]
      nlinarith [hcp_nonneg, h_nf_nonneg]
  rcases hf_step with ⟨A, hA_pos, n₁, h_step⟩
  -- threshold: large enough for log_b n ≥ 1 (n ≥ b) and
  -- b^(log_b n) ≥ n₁ (which follows from n ≥ n₁ * b via pow_log_le_n_div_b)
  let n₀' : ℕ := max (max n₀ b) (n₁ * b)
  have hn₀'_ge_n₀ : n₀ ≤ n₀' := by
    unfold n₀'; exact Nat.le_trans (Nat.le_max_left _ _) (Nat.le_max_left _ _)
  have hn₀'_ge_b : b ≤ n₀' := by
    unfold n₀'; exact Nat.le_trans (Nat.le_max_right _ _) (Nat.le_max_left _ _)
  have hn₀'_ge_n₁b : n₁ * b ≤ n₀' := by
    unfold n₀'; exact Nat.le_max_right _ _
  constructor
  · -- O direction: tailDominatedScale a b f = O(f)
    rw [Chapter03.isBigO_iff]
    refine ⟨1, by norm_num, n₀', ?_⟩
    intro n hn
    have hn_pos : n ≠ 0 := by
      have hb_pos : 0 < b := Nat.lt_trans Nat.zero_lt_one hb
      have : 0 < n₀' := Nat.lt_of_lt_of_le hb_pos hn₀'_ge_b
      omega
    rw [h_abs_tds n, h_abs_f n]
    by_cases hi : Nat.log b n = 0
    · -- n < b, but n ≥ n₀' ≥ b, contradiction
      have h_or : n < b ∨ b ≤ 1 := (Nat.log_eq_zero_iff.mp hi)
      rcases h_or with (h_lt_b | hb_le_one)
      · have h_ge_b : b ≤ n := Nat.le_trans hn₀'_ge_b hn
        omega
      · -- b ≤ 1 contradicts hb : 1 < b
        omega
    · -- i ≥ 1, tailDominatedScale n = f(b^i)
      have h_tds : tailDominatedScale a b f n = f (b ^ Nat.log b n) := by
        unfold tailDominatedScale
        simp [hi, criticalPowerScale]
        dsimp [normalizedForcing]
        have hlog_pos : 1 ≤ Nat.log b n := Nat.one_le_of_lt (Nat.pos_of_ne_zero hi)
        have h_exp : (Nat.log b n - 1) + 1 = Nat.log b n :=
          Nat.sub_add_cancel hlog_pos
        simp [h_exp, ha_pos.ne.symm]
      rw [h_tds]
      have hpow_le_n : b ^ Nat.log b n ≤ n :=
        Nat.pow_log_le_self b hn_pos
      have hmono_abs : |f (b ^ Nat.log b n)| ≤ |f n| :=
        hf_mono hpow_le_n
      rw [h_abs_f (b ^ Nat.log b n), h_abs_f n] at hmono_abs
      simpa [mul_comm] using hmono_abs
  · -- Ω direction: f = O(tailDominatedScale a b f)
    rw [Chapter03.isBigOmega_iff]
    refine ⟨A⁻¹, inv_pos.mpr hA_pos, n₀', ?_⟩
    intro n hn
    have hn_pos : n ≠ 0 := by
      have hb_pos : 0 < b := Nat.lt_trans Nat.zero_lt_one hb
      omega
    rw [h_abs_f n, h_abs_tds n]
    have hi : Nat.log b n ≠ 0 := by
      intro hzero
      have h_or : n < b ∨ b ≤ 1 := (Nat.log_eq_zero_iff.mp hzero)
      rcases h_or with (h_lt_b | hb_le_one)
      · have h_ge_b : b ≤ n := Nat.le_trans hn₀'_ge_b hn
        omega
      · omega
    have h_tds : tailDominatedScale a b f n = f (b ^ Nat.log b n) := by
      unfold tailDominatedScale
      simp [hi, criticalPowerScale]
      dsimp [normalizedForcing]
      have hlog_pos : 1 ≤ Nat.log b n := Nat.one_le_of_lt (Nat.pos_of_ne_zero hi)
      have h_exp : (Nat.log b n - 1) + 1 = Nat.log b n :=
        Nat.sub_add_cancel hlog_pos
      simp [h_exp, ha_pos.ne.symm]
    rw [h_tds]
    -- Need: A⁻¹ * f n ≤ f (b ^ Nat.log b n), equivalently f n ≤ A * f(b^i)
    -- Step 1: f(n) ≤ f(b^(i+1)) by monotonicity (n < b^(i+1))
    have h_n_lt_next : n < b ^ (Nat.log b n + 1) :=
      Nat.lt_pow_succ_log_self hb n
    have h_f_n_le_f_next : f n ≤ f (b ^ (Nat.log b n + 1)) := by
      have h_abs : |f n| ≤ |f (b ^ (Nat.log b n + 1))| :=
        hf_mono (Nat.le_of_lt h_n_lt_next)
      rw [h_abs_f n, h_abs_f (b ^ (Nat.log b n + 1))] at h_abs
      exact h_abs
    -- Step 2: f(b^(i+1)) ≤ A * f(b^i) by step bound (since b^i ≥ n₁)
    have h_low_pow_ge_n₁ : n₁ ≤ b ^ Nat.log b n := by
      have hn_ge_n₁b : n₁ * b ≤ n := Nat.le_trans hn₀'_ge_n₁b hn
      have hb_pos : 0 < b := Nat.lt_trans Nat.zero_lt_one hb
      have h_div : n₁ ≤ n / b := by
        by_contra! h
        -- h: n / b < n₁
        have hn_lt : n < n₁ * b := (Nat.div_lt_iff_lt_mul hb_pos).mp h
        omega
      calc
        n₁ ≤ n / b := h_div
        _ ≤ b ^ Nat.log b n := pow_log_le_n_div_b b n hb
    have h_step_bound : f (b ^ (Nat.log b n + 1)) ≤ A * f (b ^ Nat.log b n) := by
      have hstep := h_step (b ^ Nat.log b n) h_low_pow_ge_n₁
      rw [h_abs_f (b * (b ^ Nat.log b n)), h_abs_f (b ^ Nat.log b n)] at hstep
      -- hstep: f(b * b^i) ≤ A * f(b^i), and b * b^i = b^(i+1)
      simpa [pow_succ, mul_comm] using hstep
    calc
      A⁻¹ * f n ≤ A⁻¹ * f (b ^ (Nat.log b n + 1)) := by
        apply mul_le_mul_of_nonneg_left h_f_n_le_f_next
        positivity
      _ ≤ A⁻¹ * (A * f (b ^ Nat.log b n)) := by
        apply mul_le_mul_of_nonneg_left h_step_bound
        positivity
      _ = f (b ^ Nat.log b n) := by
        field_simp [ne_of_gt hA_pos]

end Chapter04end CLRS