Centering on the unit cube

centerCell h = h - ⨍_{(0,1)²} h is the mean-zero part of an L² function on the unit cube. This generic API is used by the grouped mean-zero assembly of BigBoundInputs (the grouped mean-zero decomposition (12)–(18)): three terms (twistie4, twistie5, normie3) need not be individually mean zero, only their sum is; their centered versions are mean zero, are bounded in HDot⁻¹ through the L² estimate, and the centered family has the same pointwise sum as the original one.

• centerCell_meanZero, l2NormSq_centerCell_le: mean zero and L² non-expansiveness;
• sum_centerCell_eq_of_meanZero, centerCell_add_add: centering a family whose sum has mean zero does not change the sum;
• continuousOn_centerCell: centering preserves joint continuity on (0,1) × ℝ².

theorem AVenhance.Infra.Section5.Integration.volume_unitCube : MeasureTheory.volume unitCube = 1

The unit cube has volume one.

instance AVenhance.Infra.Section5.Integration.instIsFiniteMeasureVecOfNatNatRestrictVolumeUnitCube : MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict unitCube)

noncomputable def AVenhance.Infra.Section5.Integration.centerCell (h : Homogenization.Vec 2 → ℝ) (x : Homogenization.Vec 2) : ℝ

h minus its mean over the unit cube.

Equations

• AVenhance.Infra.Section5.Integration.centerCell h x = h x - ∫ (y : Homogenization.Vec 2) in AVenhance.unitCube, h y

theorem AVenhance.Infra.Section5.Integration.integrableOn_unitCube_of_memL2On {h : Homogenization.Vec 2 → ℝ} (hh : Homogenization.MemL2On unitCube h) : MeasureTheory.IntegrableOn h unitCube MeasureTheory.volume

An L² function on the unit cube is integrable there.

theorem AVenhance.Infra.Section5.Integration.integral_centerCell {h : Homogenization.Vec 2 → ℝ} (hh : Homogenization.MemL2On unitCube h) : ∫ (x : Homogenization.Vec 2) in unitCube, centerCell h x = 0

The mean of a function over the unit cube is the integral (volume one).

theorem AVenhance.Infra.Section5.Integration.centerCell_meanZero {h : Homogenization.Vec 2 → ℝ} (hh : Homogenization.MemL2On unitCube h) : Homogenization.MeanZeroOn unitCube (centerCell h)

The centered function has mean zero on the unit cube.

theorem AVenhance.Infra.Section5.Integration.memL2On_centerCell {h : Homogenization.Vec 2 → ℝ} (hh : Homogenization.MemL2On unitCube h) : Homogenization.MemL2On unitCube (centerCell h)

The centered function is L² on the unit cube.

theorem AVenhance.Infra.Section5.Integration.l2NormSq_centerCell_le {h : Homogenization.Vec 2 → ℝ} (hh : Homogenization.MemL2On unitCube h) : l2NormSq (centerCell h) ≤ l2NormSq h

Centering is L²-nonexpansive: ‖h - ⨍ h‖² = ‖h‖² - (⨍ h)² ≤ ‖h‖².

theorem AVenhance.Infra.Section5.Integration.sum_centerCell_eq_of_meanZero {ι : Type u_1} (s : Finset ι) (h : ι → Homogenization.Vec 2 → ℝ) (hint : ∀ i ∈ s, MeasureTheory.IntegrableOn (h i) unitCube MeasureTheory.volume) (hsum : Homogenization.MeanZeroOn unitCube fun (x : Homogenization.Vec 2) => ∑ i ∈ s, h i x) (x : Homogenization.Vec 2) : ∑ i ∈ s, centerCell (h i) x = ∑ i ∈ s, h i x

Centering a finite family whose sum has mean zero does not change the sum.

theorem AVenhance.Infra.Section5.Integration.centerCell_add_add {a b c : Homogenization.Vec 2 → ℝ} (ha : Homogenization.MemL2On unitCube a) (hb : Homogenization.MemL2On unitCube b) (hc : Homogenization.MemL2On unitCube c) (hsum : Homogenization.MeanZeroOn unitCube fun (x : Homogenization.Vec 2) => a x + b x + c x) (x : Homogenization.Vec 2) : centerCell a x + centerCell b x + centerCell c x = a x + b x + c x

Three-term version of sum_centerCell_eq_of_meanZero.

theorem AVenhance.Infra.Section5.Integration.continuousOn_centerCell {F : ℝ → Homogenization.Vec 2 → ℝ} (hF : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => F p.1 p.2) (Set.Ioo 0 1 ×ˢ Set.univ)) : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => centerCell (F p.1) p.2) (Set.Ioo 0 1 ×ˢ Set.univ)

Centering preserves joint continuity on (0,1) × ℝ².