Coarse-graining support: Support.Sobolev.CubeEmbedding.FoldNorm

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

Norm transport under the even fold

The coordinatewise even fold Fold lo hi : Vec d → Vec d maps the tripled open box Box3 lo hi onto the box Box lo hi in a 3-to-1, piecewise-affine, measure-preserving way. The load-bearing consequence is the lintegral transport identity

∫⁻ x in Box3, g (Fold lo hi x) = 3 ^ d * ∫⁻ x in Box, g x

for measurable g, and its L² corollary

eLpNorm (v ∘ Fold) 2 (vol Box3) = (3 ^ d) ^ (1/2) * eLpNorm v 2 (vol Box).

The proof factors through the product structure: each coordinate fold pushes the restricted Lebesgue measure on the tripled interval forward to 3 copies of the restricted Lebesgue measure on the base interval, and Measure.pi_map_pi assembles the coordinatewise pushforwards.

def HCPolySupport.Box {d : ℕ} (lo hi : Vec d) : Set (Vec d)

The open axis box ∏ᵢ (loᵢ, hiᵢ).

Equations

• HCPolySupport.Box lo hi = Set.univ.pi fun (k : Fin d) => Set.Ioo (lo k) (hi k)

def HCPolySupport.Box3 {d : ℕ} (lo hi : Vec d) : Set (Vec d)

The tripled open axis box ∏ᵢ (2loᵢ − hiᵢ, 2hiᵢ − loᵢ), i.e. the base box enlarged by its own side length on each face.

Equations

• HCPolySupport.Box3 lo hi = Set.univ.pi fun (k : Fin d) => Set.Ioo (2 * lo k - hi k) (2 * hi k - lo k)

theorem HCPolySupport.measurableSet_Box {d : ℕ} (lo hi : Vec d) : MeasurableSet (Box lo hi)

theorem HCPolySupport.measurableSet_Box3 {d : ℕ} (lo hi : Vec d) : MeasurableSet (Box3 lo hi)

One-dimensional pushforward

theorem HCPolySupport.map_foldR_restrict (lo hi : ℝ) (h : lo < hi) : MeasureTheory.Measure.map (foldR lo hi) (MeasureTheory.volume.restrict (Set.Ioo (2 * lo - hi) (2 * hi - lo))) = 3 • MeasureTheory.volume.restrict (Set.Ioo lo hi)

1-D fold pushforward. The scalar fold pushes the restricted Lebesgue measure on the tripled interval forward to 3 copies of the restricted Lebesgue measure on the base interval.

Product assembly

theorem HCPolySupport.pi_smul_const {ι : Type u_1} [Fintype ι] {α : ι → Type u_2} [(i : ι) → MeasurableSpace (α i)] (ρ : (i : ι) → MeasureTheory.Measure (α i)) [∀ (i : ι), MeasureTheory.SigmaFinite (ρ i)] {c : ENNReal} [∀ (i : ι), MeasureTheory.SigmaFinite (c • ρ i)] : (MeasureTheory.Measure.pi fun (i : ι) => c • ρ i) = c ^ Fintype.card ι • MeasureTheory.Measure.pi ρ

Scaling each factor of a finite product measure by c scales the product by c ^ card.

theorem HCPolySupport.map_Fold_restrict {d : ℕ} (lo hi : Vec d) (hlt : ∀ (k : Fin d), lo k < hi k) : MeasureTheory.Measure.map (Fold lo hi) (MeasureTheory.volume.restrict (Box3 lo hi)) = 3 ^ d • MeasureTheory.volume.restrict (Box lo hi)

d-dimensional fold pushforward. The coordinatewise fold pushes the restricted Lebesgue measure on the tripled box forward to 3 ^ d copies of the restricted Lebesgue measure on the base box.

lintegral and eLpNorm transport

theorem HCPolySupport.lintegral_foldComp {d : ℕ} {g : Vec d → ENNReal} (hg : Measurable g) (lo hi : Vec d) (hlt : ∀ (k : Fin d), lo k < hi k) : ∫⁻ (x : Vec d) in Box3 lo hi, g (Fold lo hi x) = 3 ^ d * ∫⁻ (x : Vec d) in Box lo hi, g x

lintegral fold transport.

theorem HCPolySupport.eLpNorm_foldComp {d : ℕ} {v : Vec d → ℝ} (hv : Measurable v) (lo hi : Vec d) (hlt : ∀ (k : Fin d), lo k < hi k) : MeasureTheory.eLpNorm (fun (x : Vec d) => v (Fold lo hi x)) 2 (MeasureTheory.volume.restrict (Box3 lo hi)) = (3 ^ d) ^ (1 / 2) * MeasureTheory.eLpNorm v 2 (MeasureTheory.volume.restrict (Box lo hi))

L² fold transport. The L²(Box3) norm of v ∘ Fold equals (3 ^ d) ^ (1/2) times the L²(Box) norm of v.