Coarse-graining support: Support.Book.Ch01.Theorems.NormScaling

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Scaling of normalized averages

These are the Chapter 1 bookkeeping lemmas for dilation. The main use in Chapter 3 is the last theorem: a unit-scale estimate for the pulled-back gradient transfers to the physical cube with the expected r^{-2} factor on the right-hand side.

theorem HCPolySupport.Book.Ch01.volumeAverage_translateSet_comp_subRight {d : ℕ} (z : Vec d) (U : Set (Vec d)) (f : Vec d → ℝ) : (volumeAverage (translateSet z U) fun (x : Vec d) => f (x - z)) = volumeAverage U f

Normalized volume averages are invariant under translation of the domain, with the function pulled back by the inverse translation.

theorem HCPolySupport.Book.Ch01.volumeAverage_translateSet_eq_comp_addRight {d : ℕ} (z : Vec d) (U : Set (Vec d)) (f : Vec d → ℝ) : volumeAverage (translateSet z U) f = volumeAverage U fun (x : Vec d) => f (x + z)

Equivalent forward form of translation invariance for normalized volume averages.

theorem HCPolySupport.Book.Ch01.volumeAverage_sq_translateSet_comp_subRight {d : ℕ} (z : Vec d) (U : Set (Vec d)) (u : Vec d → ℝ) : (volumeAverage (translateSet z U) fun (x : Vec d) => u (x - z) ^ 2) = volumeAverage U fun (x : Vec d) => u x ^ 2

Scalar normalized L² square is invariant under translation of the domain, with the scalar field pulled back.

theorem HCPolySupport.Book.Ch01.volumeAverage_vecNormSq_translateSet_comp_subRight {d : ℕ} (z : Vec d) (U : Set (Vec d)) (G : Vec d → Vec d) : (volumeAverage (translateSet z U) fun (x : Vec d) => vecNormSq (G (x - z))) = volumeAverage U fun (x : Vec d) => vecNormSq (G x)

Vector normalized L² square is invariant under translation of the domain, with the vector field pulled back.

theorem HCPolySupport.Book.Ch01.volume_smul_toReal_of_pos {d : ℕ} {r : ℝ} (hr : 0 < r) (U : Set (Vec d)) : (MeasureTheory.volume (r • U)).toReal = r ^ d * (MeasureTheory.volume U).toReal

Lebesgue volume of a positive dilation, written in toReal form.

theorem HCPolySupport.Book.Ch01.volumeAverage_smul_set_comp_smul_of_pos {d : ℕ} {r : ℝ} (hr : 0 < r) (U : Set (Vec d)) (f : Vec d → ℝ) : volumeAverage (r • U) f = volumeAverage U fun (x : Vec d) => f (r • x)

Normalized volume averages are invariant under positive dilation of the domain, with the function pulled back by the dilation map.

theorem HCPolySupport.Book.Ch01.setIntegral_comp_smul_of_pos {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {r : ℝ} (hr : 0 < r) (U : Set (Vec d)) (f : Vec d → E) : ∫ (x : Vec d) in U, f (r • x) = (r ^ d)⁻¹ • ∫ (y : Vec d) in r • U, f y

Raw set-integral form of positive dilation change of variables.

theorem HCPolySupport.Book.Ch01.setIntegral_smul_set_eq_comp_smul_of_pos {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {r : ℝ} (hr : 0 < r) (U : Set (Vec d)) (f : Vec d → E) : ∫ (y : Vec d) in r • U, f y = r ^ d • ∫ (x : Vec d) in U, f (r • x)

Forward raw set-integral form of positive dilation change of variables.

theorem HCPolySupport.Book.Ch01.setIntegral_translateSet_smul_set_eq_comp_affine_of_pos {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {r : ℝ} (hr : 0 < r) (z : Vec d) (U : Set (Vec d)) (f : Vec d → E) : ∫ (y : Vec d) in translateSet z (r • U), f y = r ^ d • ∫ (x : Vec d) in U, f (r • x + z)

Raw set-integral form of a positive dilation followed by translation.

theorem HCPolySupport.Book.Ch01.setIntegral_euclideanBall_eq_unit_affine_of_pos {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {r : ℝ} (hr : 0 < r) (z : Vec d) (f : Vec d → E) : ∫ (y : Vec d) in euclideanBall z r, f y = r ^ d • ∫ (x : Vec d) in euclideanBall 0 1, f (r • x + z)

Raw set integrals over explicit Euclidean balls reduce to unit-ball integrals by affine pullback.

theorem HCPolySupport.Book.Ch01.volumeAverage_sq_comp_smul_of_pos {d : ℕ} {r : ℝ} (hr : 0 < r) (U : Set (Vec d)) (u : Vec d → ℝ) : (volumeAverage (r • U) fun (y : Vec d) => u y ^ 2) = volumeAverage U fun (x : Vec d) => u (r • x) ^ 2

Scalar normalized L² square is invariant under positive dilation of the domain, with the scalar field pulled back.

theorem HCPolySupport.Book.Ch01.volumeAverage_vecNormSq_comp_smul_of_pos {d : ℕ} {r : ℝ} (hr : 0 < r) (U : Set (Vec d)) (G : Vec d → Vec d) : (volumeAverage (r • U) fun (y : Vec d) => vecNormSq (G y)) = volumeAverage U fun (x : Vec d) => vecNormSq (G (r • x))

Vector normalized L² square is invariant under positive dilation of the domain, with the vector field pulled back.

theorem HCPolySupport.Book.Ch01.volumeAverage_translateSet_smul_set_comp_affine_of_pos {d : ℕ} {r : ℝ} (hr : 0 < r) (z : Vec d) (U : Set (Vec d)) (f : Vec d → ℝ) : volumeAverage (translateSet z (r • U)) f = volumeAverage U fun (x : Vec d) => f (r • x + z)

Normalized volume averages are invariant under a positive dilation followed by a translation.

theorem HCPolySupport.Book.Ch01.volumeAverage_euclideanBall_eq_unit_affine_of_pos {d : ℕ} {r : ℝ} (hr : 0 < r) (z : Vec d) (f : Vec d → ℝ) : volumeAverage (euclideanBall z r) f = volumeAverage (euclideanBall 0 1) fun (x : Vec d) => f (r • x + z)

Normalized averages over explicit Euclidean balls reduce to unit-ball averages by affine pullback.

theorem HCPolySupport.Book.Ch01.volumeAverage_euclideanClosedBall_eq_unit_affine_of_pos {d : ℕ} {r : ℝ} (hr : 0 < r) (z : Vec d) (f : Vec d → ℝ) : volumeAverage (euclideanClosedBall z r) f = volumeAverage (euclideanClosedBall 0 1) fun (x : Vec d) => f (r • x + z)

Normalized averages over explicit closed Euclidean balls reduce to unit-ball averages by affine pullback.

theorem HCPolySupport.Book.Ch01.volumeAverage_translateSet_smul_set_comp_inv_affine_of_pos {d : ℕ} {r : ℝ} (hr : 0 < r) (z : Vec d) (U : Set (Vec d)) (f : Vec d → ℝ) : (volumeAverage (translateSet z (r • U)) fun (y : Vec d) => f (r⁻¹ • (y - z))) = volumeAverage U f

Inverse-pullback form of affine invariance for normalized averages.

theorem HCPolySupport.Book.Ch01.volumeAverage_sq_translateSet_smul_set_comp_inv_affine_of_pos {d : ℕ} {r : ℝ} (hr : 0 < r) (z : Vec d) (U : Set (Vec d)) (u : Vec d → ℝ) : (volumeAverage (translateSet z (r • U)) fun (y : Vec d) => u (r⁻¹ • (y - z)) ^ 2) = volumeAverage U fun (x : Vec d) => u x ^ 2

Scalar normalized L² square is invariant under a positive dilation followed by a translation, with the scalar field pulled back.

theorem HCPolySupport.Book.Ch01.volumeAverage_vecNormSq_translateSet_smul_set_comp_inv_affine_of_pos {d : ℕ} {r : ℝ} (hr : 0 < r) (z : Vec d) (U : Set (Vec d)) (G : Vec d → Vec d) : (volumeAverage (translateSet z (r • U)) fun (y : Vec d) => vecNormSq (G (r⁻¹ • (y - z)))) = volumeAverage U fun (x : Vec d) => vecNormSq (G x)

Vector normalized L² square is invariant under a positive dilation followed by a translation, with the vector field pulled back.

theorem HCPolySupport.Book.Ch01.volumeAverage_sq_scaled_comp_smul_of_pos {d : ℕ} {r : ℝ} (hr : 0 < r) (U : Set (Vec d)) (u : Vec d → ℝ) : (volumeAverage U fun (x : Vec d) => (r * u (r • x)) ^ 2) = r ^ 2 * volumeAverage (r • U) fun (y : Vec d) => u y ^ 2

Scalar normalized L² square after an additional amplitude scaling.

theorem HCPolySupport.Book.Ch01.volumeAverage_vecNormSq_scaled_comp_smul_of_pos {d : ℕ} {r : ℝ} (hr : 0 < r) (U : Set (Vec d)) (G : Vec d → Vec d) : (volumeAverage U fun (x : Vec d) => vecNormSq (r • G (r • x))) = r ^ 2 * volumeAverage (r • U) fun (y : Vec d) => vecNormSq (G y)

Vector normalized L² square after the gradient-style amplitude scaling: G pulls back as r • G (r • x).

theorem HCPolySupport.Book.Ch01.caccioppoliScale_from_unit_averages {d : ℕ} {r C : ℝ} (hr : 0 < r) (U : Set (Vec d)) (u : Vec d → ℝ) (G : Vec d → Vec d) (hunit : (volumeAverage U fun (x : Vec d) => vecNormSq (r • G (r • x))) ≤ C * volumeAverage U fun (x : Vec d) => u (r • x) ^ 2) : (volumeAverage (r • U) fun (y : Vec d) => vecNormSq (G y)) ≤ r⁻¹ ^ 2 * C * volumeAverage (r • U) fun (y : Vec d) => u y ^ 2

Transfer a unit-scale Caccioppoli-shaped estimate through a positive dilation. The gradient pullback contributes exactly the physical r^{-2} factor on the right-hand side.