Translation covariance of the exponentially weighted corrector memory.

theorem AVenhance.Infra.Section3.TimeMemorySymmetry.volume_restrict_Iic_add_map (t T : ℝ) : MeasureTheory.Measure.map (⇑(MeasurableEquiv.addRight T)) (MeasureTheory.volume.restrict (Set.Iic t)) = MeasureTheory.volume.restrict (Set.Iic (t + T))

theorem AVenhance.Infra.Section3.TimeMemorySymmetry.integral_Iic_add_right (t T : ℝ) (f : ℝ → ℝ) : ∫ (s : ℝ) in Set.Iic (t + T), f s = ∫ (s : ℝ) in Set.Iic t, f (s + T)

A set integral over a translated left half-line is transported by the translation equivalence.

theorem AVenhance.Infra.Section3.corrTime_add_twoCellCount {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ : ℝ) (k : ℤ) (t : ℝ) : I.corrTime κ m (k + 2 * ↑(Ingredients.tauCellCount β I.Λ m)) (t + 2 * tauPP β I.Λ m) = I.corrTime κ m k t

The corrector memory is invariant under translating time by two large cells and the small index by twice the number of small cells per large cell.