Documentation

HighDimProb.Concentration.LayerCake

Layer-cake and exponential-tail calculus helpers #

This module is the public import boundary for reusable layer-cake and tail-integral infrastructure.

For Stage C1 the existing declarations are re-exported from HighDimProb.Concentration.TailToOrlicz to keep names stable and avoid a risky physical move of proof-heavy analytic lemmas. Future cleanup can move the declaration bodies here without changing public theorem names.

Verified Wikipedia reference:

Formula reference: the re-exported lemmas formalize the layer-cake identity that rewrites nonnegative functions and integrals through super-level-set tails, as summarized at https://en.wikipedia.org/wiki/Layer_cake_representation