SharpMeanLayerProperties

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Elementary properties of the sharp mean-layer envelope

This file proves the sign and measurability facts needed to turn the sharp mean-layer domination into Orlicz lanes.

theorem Algsuperdiff.Section3.Provider.Multiscale.probeSharpLayerMassEnvelope_nonneg (d n : ℕ) : 0 ≤ probeSharpLayerMassEnvelope d n