WaveTermTranslation

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

Measurability of the Step-2 tail leg

The tail leg of e.wave.influence.bound is a random sum: its number of summands is the truncation depth hsep, an observable of the sample built from a lattice of bad sites and a cluster-diameter count. This module proves that the sum is a random variable, the measurability datum every transport of the tail leg consumes.

The truncation depth is NOT a pathwise translation invariant — stationarity equalizes its law, not its values — so nothing here identifies the depths read at two different cubes.

Main results

• Algsuperdiff.Section3.Provider.Multiscale.measurable_waveTailTerm: the tail leg waveTailTerm M m E b lout ell is measurable. The depth hsep is a measurable ℕ-valued observable by measurableSet_lt_hsep, and a Finset.range sum of measurable summands over a measurable depth is measurable because the sample space splits along the countably many values of the depth.

References

• ABK26, e.wave.influence.bound, with the layer decomposition and the tail bookkeeping.

The per-layer wave gauge at an arbitrary cube

The deterministic domination at an arbitrary cube

The per-layer Gamma_2 display at an arbitrary cube

The macroscopic leg at an arbitrary cube

The tail leg at an arbitrary cube

Measurability of the truncated tail sum

theorem Algsuperdiff.Section3.Provider.Multiscale.measurable_waveTailTerm {d : ℕ} (M : ABKModel d) (m : ℤ) (E b : ℝ) (lout ell : ℤ) : Measurable (waveTailTerm M m E b lout ell)

The origin tail leg is a random variable. This is the measurability datum the abstract transport consumes; the truncation depth hsep is a measurable Nat-valued observable by measurableSet_lt_hsep.

The tail leg at an arbitrary cube