Documentation

LeanPool.AnomalousDiffusion.AVenhance.Infra.Section4.Amnr.TemporalPairing

Absolute time-integrated spatial pairings and the actual product measure.

source
theorem AVenhance.Infra.Section4.amnr_time_cell_product_absolutelyContinuous {T : ℝ} (hT : 0 ≤ T) :
((MeasureTheory.volume.restrict (Set.uIoc 0 T)).prod (MeasureTheory.volume.restrict unitCube)).AbsolutelyContinuous (MeasureTheory.volume.restrict (Set.Ioi 0 ×ˢ Set.univ))

The physical finite-time product is absolutely continuous on the full positive-time domain, even when the terminal time is zero.

source
theorem AVenhance.Infra.Section4.amnr_time_cell_product_absolutelyContinuous_closed {T : ℝ} (hT : 0 ≤ T) :
((MeasureTheory.volume.restrict (Set.uIoc 0 T)).prod (MeasureTheory.volume.restrict unitCube)).AbsolutelyContinuous (MeasureTheory.volume.restrict (Set.Ici 0 ×ˢ Set.univ))