1. CLRS-Lean
  2. CLRS Fourth Edition
  3. Chapter 17. Augmenting Data Structures
Imports
import CLRSLean.Chapter_14 import CLRSLean.FourthEdition.Chapter_17.Section_17_1_Dynamic_Order_Statistics import CLRSLean.FourthEdition.Chapter_17.Section_17_2_Augmenting_Data_Structures import CLRSLean.FourthEdition.Chapter_17.Section_17_3_Interval_Trees

Chapter 17 — Augmenting Data Structures

This is the canonical CLRS fourth-edition chapter guide during the migration period.

Current source

During the compatibility period this guide imports CLRSLean.Chapter_14. Existing declarations retain their current namespaces until the chapter-by-chapter source migration.

Coverage boundary

The third-edition Chapter 14 developments supply substantial relocated proof content, and three fourth-edition section layers close the §17.1–§17.3 boundaries:

  • §17.1 (Section_17_1_Dynamic_Order_Statistics): OS-RANK osRank/rankOf, their agreement on well-sized trees, and the O(log n) query bound osRankCost_log_bound.

  • §17.2 (Section_17_2_Augmenting_Data_Structures): the constant-time combine premise and the asymptotic augmentation update bound augmentation_update_bound.

  • §17.3 (Section_17_3_Interval_Trees): the dynamic/static interval-tree bridge toIntervalTree/wellAugmented_toIntervalTree, search-after-update intervalSearch_after_update, and the Interval-keyed O(log n) search bound intervalSearchCost_log_bound.

See docs/clrs-fourth-edition-map.csv for the section-level mapping and docs/migrations/clrs4.md for compatibility and deprecation policy.