RandomHsepWaveEnvelope

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

The wave envelope at the random separation scale

measureReal_exists_cubeSupBound_gt_le prices the wave-envelope failure for a deterministic Whitney scale profile. The profile used in Section 3 is instead selected from the same cutoff sample through hsep. This file performs that selection by a finite-cutoff decomposition. No independence or measurability of the random index is used.

A set-valued random-index decomposition

theorem Algsuperdiff.Section3.Provider.Multiscale.measureReal_mem_randomIndex_le {Omega : Type u_1} [MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} [MeasureTheory.IsFiniteMeasure mu] (B : ℕ → Set Omega) (N : Omega → ℕ) (H : ℕ) : mu.real {omega : Omega | omega ∈ B (N omega)} ≤ ∑ h ∈ Finset.range (H + 1), mu.real (B h) + mu.real {omega : Omega | H < N omega}

A finite-cutoff decomposition for a set selected by a random natural index. The pieces with index at most H are bounded separately, while all remaining samples are charged to {omega | H < N omega}. This requires no measurability of N and no independence between N and the family B.

The random-hsep wave event