Centering preserves the homogeneous dual seminorm. Finite sums are repaired using the mean of the actual total, rather than individual product means.

noncomputable def AVenhance.Infra.Ergodic.centerCell {d : ℕ} (h : Homogenization.Vec d → ℝ) : Homogenization.Vec d → ℝ

Remove the actual cell mean.

Equations

• AVenhance.Infra.Ergodic.centerCell h x = h x - AVenhance.Infra.Ergodic.cellAverage h

theorem AVenhance.Infra.Ergodic.cellAverage_centerCell {d : ℕ} {h : Homogenization.Vec d → ℝ} (hh : MeasureTheory.LocallyIntegrable h MeasureTheory.volume) : cellAverage (centerCell h) = 0

theorem AVenhance.Infra.Ergodic.homogeneousHMinusOneNorm_centerCell_eq {d : ℕ} {h : Homogenization.Vec d → ℝ} (hh : MeasureTheory.LocallyIntegrable h MeasureTheory.volume) : homogeneousHMinusOneNorm (centerCell h) = homogeneousHMinusOneNorm h

theorem AVenhance.Infra.Ergodic.homogeneousHMinusOneNorm_finset_sum_le {d : ℕ} {ι : Type u_1} (s : Finset ι) (h : ι → Homogenization.Vec d → ℝ) (hh : ∀ i ∈ s, MeasureTheory.LocallyIntegrable (h i) MeasureTheory.volume) : (homogeneousHMinusOneNorm fun (x : Homogenization.Vec d) => ∑ i ∈ s, h i x) ≤ ∑ i ∈ s, homogeneousHMinusOneNorm (h i)

Triangle inequality for an actual finite collection of locally integrable data.