Coarse-graining support: Support.Book.Ch03.Theorems.CoarseCaccioppoliDilationTransport

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

Dilation transport proof for coarse Caccioppoli

The scale-zero coarse Caccioppoli theorem and public arbitrary-scale target are imported from CoarseCaccioppoli.Interface. This file proves the concrete normalization witnesses and closes the public arbitrary-scale theorem directly, without exporting an intermediate bridge package.

The intended source of the witnesses below is the public Chapter 2 dilation package, together with the Chapter 1 norm-scaling lemmas. The interface fixes the normalized cube to Ch02.dilateCube (-Q.scale) Q, so downstream code cannot drift to a different normalization convention.

theorem HCPolySupport.Book.Ch03.cubeCenter_dilateCube {d : ℕ} (k : ℤ) (Q : TriadicCube d) : cubeCenter (Ch02.dilateCube k Q) = Ch02.dilateVec k (cubeCenter Q)

The center of a dilated triadic cube is the dilation of its center.

theorem HCPolySupport.Book.Ch03.openCubeAtScale_dilateVec {d : ℕ} (k m : ℤ) (x : Vec d) : openCubeAtScale (Ch02.dilateVec k x) (m + k) = Ch02.triadicDilationFactor k • openCubeAtScale x m

A triadic open window dilates with its center and scale.

theorem HCPolySupport.Book.Ch03.caccioppoliCoreSet_dilateCube {d : ℕ} (k : ℤ) (Q : TriadicCube d) (x : Vec d) : caccioppoliCoreSet (Ch02.dilateCube k Q) (Ch02.dilateVec k x) = Ch02.triadicDilationFactor k • caccioppoliCoreSet Q x

Dilation commutes with the Caccioppoli core set.

theorem HCPolySupport.Book.Ch03.boundaryPatchWindow_dilateCube {d : ℕ} (k : ℤ) (Q : TriadicCube d) (x : Vec d) : openCubeAtScale (Ch02.dilateVec k x) ((Ch02.dilateCube k Q).scale - 1) = Ch02.triadicDilationFactor k • openCubeAtScale x (Q.scale - 1)

Dilation commutes with the boundary Caccioppoli localization window.

theorem HCPolySupport.Book.Ch03.localizedZeroTraceFunctionOn_dilate {d : ℕ} {Ω V Ω' V' : Set (Vec d)} {u v : Vec d → ℝ} {r : ℝ} (hr : 0 < r) (hΩ' : Ω' = r • Ω) (hV' : V' = r • V) (hv : ∀ (y : Vec d), v y = r * u (r⁻¹ • y)) (hu : LocalizedZeroTraceFunctionOn Ω V u) : LocalizedZeroTraceFunctionOn Ω' V' v

Localized zero trace is transported by positive dilations, with the solution normalization v(y) = r u(r^{-1} y).

theorem HCPolySupport.Book.Ch03.localizedCoeffEnergyValue_dilate_eq {d : ℕ} {k : ℤ} {Q : TriadicCube d} {a : Ch02.CoeffOn (Ch02.cubeDomain Q)} {b : Ch02.CoeffOn (Ch02.cubeDomain (Ch02.dilateCube k Q))} (hCoeff : Ch02.CoeffOn.IsCubeDilation k a b) {u : Ch02.Solution (Ch02.cubeDomain Q) a} {v : Ch02.Solution (Ch02.cubeDomain (Ch02.dilateCube k Q)) b} (hDilation : Ch02.Solution.IsCubeDilation hCoeff u v) {V : Set (Vec d)} (hVsub : V ⊆ openCubeSet Q) : localizedCoeffEnergyValue (Ch02.triadicDilationFactor k • V) b v.toH1 = localizedCoeffEnergyValue V a u.toH1

The localized coefficient energy is invariant under the public solution dilation normalization v(x) = r u(r^{-1}x).

theorem HCPolySupport.Book.Ch03.normalizedL2SqOnSet_dilate_eq {d : ℕ} {k : ℤ} {Q : TriadicCube d} {a : Ch02.CoeffOn (Ch02.cubeDomain Q)} {b : Ch02.CoeffOn (Ch02.cubeDomain (Ch02.dilateCube k Q))} {hCoeff : Ch02.CoeffOn.IsCubeDilation k a b} {u : Ch02.Solution (Ch02.cubeDomain Q) a} {v : Ch02.Solution (Ch02.cubeDomain (Ch02.dilateCube k Q)) b} (hDilation : Ch02.Solution.IsCubeDilation hCoeff u v) {V : Set (Vec d)} (hVsub : V ⊆ openCubeSet Q) : normalizedL2SqOnSet (Ch02.triadicDilationFactor k • V) v.toH1.toFun = Ch02.triadicDilationFactor k ^ 2 * normalizedL2SqOnSet V u.toH1.toFun

Under solution dilation, normalized scalar L² on a dilated set gains the square of the amplitude factor.

theorem HCPolySupport.Book.Ch03.triadicDilationFactor_neg_scale_sq {d : ℕ} (Q : TriadicCube d) : Ch02.triadicDilationFactor (-Q.scale) ^ 2 = Real.rpow 3 (-2 * ↑Q.scale)

The solution-amplitude square for normalization by -Q.scale is exactly the explicit scale factor in the public Caccioppoli RHS.

theorem HCPolySupport.Book.Ch03.normalizedAverage_dilate_solution_eq {d : ℕ} {k : ℤ} {Q : TriadicCube d} {a : Ch02.CoeffOn (Ch02.cubeDomain Q)} {b : Ch02.CoeffOn (Ch02.cubeDomain (Ch02.dilateCube k Q))} {hCoeff : Ch02.CoeffOn.IsCubeDilation k a b} {u : Ch02.Solution (Ch02.cubeDomain Q) a} {v : Ch02.Solution (Ch02.cubeDomain (Ch02.dilateCube k Q)) b} (hDilation : Ch02.Solution.IsCubeDilation hCoeff u v) : Ch01.Legacy.normalizedAverage (Ch02.dilateCube k Q) v.toH1.toFun = Ch02.triadicDilationFactor k * Ch01.Legacy.normalizedAverage Q u.toH1.toFun

The cube average of a dilated solution scales by the solution-amplitude factor.

theorem HCPolySupport.Book.Ch03.interiorCaccioppoliParentOscillationL2Sq_dilate_eq {d : ℕ} {k : ℤ} {Q : TriadicCube d} {A B : CoeffFamily d} {hCoeff : Ch02.CoeffOn.IsCubeDilation k (A.coeffOn Q) (B.coeffOn (Ch02.dilateCube k Q))} {u : CubeSolution Q A} {v : CubeSolution (Ch02.dilateCube k Q) B} (hDilation : Ch02.Solution.IsCubeDilation hCoeff u v) : interiorCaccioppoliParentOscillationL2Sq (Ch02.dilateCube k Q) B v = Ch02.triadicDilationFactor k ^ 2 * interiorCaccioppoliParentOscillationL2Sq Q A u

The centered parent L² oscillation scales with the same amplitude-square factor as the uncentered parent L² term.

theorem HCPolySupport.Book.Ch03.caccioppoliPrefactor_dilate_neg_scale {d : ℕ} [NeZero d] (hmulti : Ch02.MultiscaleDilationTheory d) {Q : TriadicCube d} {a b : CoeffFamily d} {C s t : ℝ} (hFam : Ch02.TriadicCoeffFamily.IsDilation (-Q.scale) a b) : caccioppoliPrefactor C Q a s t = Real.rpow 3 (-2 * ↑Q.scale) * caccioppoliPrefactor C (Ch02.dilateCube (-Q.scale) Q) b s t

The Caccioppoli scalar prefactor under normalization to scale zero.

The multiscale quantities are invariant under the public Chapter 2 dilation relation, while the explicit 3^{-2m} factor is exactly the scale conversion left in the note-facing statement.

theorem HCPolySupport.Book.Ch03.coarseCaccioppoliTheory (d : ℕ) [NeZero d] : CoarseCaccioppoliTheory d

Fully proved public coarse Caccioppoli theorem package for arbitrary triadic scales. The scale normalization is discharged internally by concrete dilation witnesses, so no transport bridge appears in the public API.