SharpFramedMeanLayerProperties

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

Sign and measurability of the framed sharp layer envelope

These elementary properties support later Orlicz aggregation.

theorem Algsuperdiff.Section3.Provider.Multiscale.measurable_probeSharpLayerFrame {d : ℕ} (M : ABKModel d) (m : ℤ) (E b : ℝ) (k₀ n : ℕ) (i : ℤ) : Measurable (probeSharpLayerFrame M m E b k₀ n i)