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

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

Scale-zero Caccioppoli core estimates

This file contains the pointwise coefficient bridge, core-window geometry, and normalized core-energy estimates used by the scale-zero Caccioppoli proof. The theorem assembly remains in CoarseCaccioppoliScaleZero.lean.

Audit tag

Claim: provide the pointwise-coefficient transport and unit-scale core-energy geometry used by the scale-zero Caccioppoli bridge.

Downstream target: CoarseCaccioppoliScaleZeroBridge.lean. This file should remain core estimate infrastructure, not a public theorem-package surface.

@[reducible, inline]

noncomputable abbrev HCPolySupport.Book.Ch03.pointwiseCoeffFor {d : ℕ} (Q : TriadicCube d) (a : CoeffFamily d) : CoeffField d

Pointwise coefficient representative of the coefficient family on the given cube domain.

Equations

• HCPolySupport.Book.Ch03.pointwiseCoeffFor Q a = HCPolySupport.Internal.Ch02.BookCh02.pointwiseCoeffField (HCPolySupport.Book.Ch02.cubeDomain Q) (a.coeffOn Q)

theorem HCPolySupport.Book.Ch03.pointwiseCoeffFor_isEllipticFieldOn_cubeSet {d : ℕ} (Q : TriadicCube d) (a : CoeffFamily d) : IsEllipticFieldOn (a.coeffOn Q).lam (a.coeffOn Q).Lam (cubeSet Q) (pointwiseCoeffFor Q a)

noncomputable def HCPolySupport.Book.Ch03.CubeSolution.toPointwiseAHarmonic {d : ℕ} {Q : TriadicCube d} {a : CoeffFamily d} (u : CubeSolution Q a) : AHarmonicFunction (pointwiseCoeffFor Q a) (openCubeSet Q)

Regard a cube solution as harmonic for the pointwise coefficient representative, retaining its Sobolev data.

Equations

• u.toPointwiseAHarmonic = { toH1 := u.toH1, isHarmonic := ⋯ }

noncomputable def HCPolySupport.Book.Ch03.BoundaryCaccioppoliDatum.toPointwiseAHarmonic {d : ℕ} {Q : TriadicCube d} {a : CoeffFamily d} {x : Vec d} (u : BoundaryCaccioppoliDatum Q a x) : AHarmonicFunction (pointwiseCoeffFor Q a) (openCubeSet Q)

Regard boundary Caccioppoli data as harmonic for the pointwise coefficient representative, retaining its Sobolev data.

Equations

• u.toPointwiseAHarmonic = { toH1 := u.toH1, isHarmonic := ⋯ }

theorem HCPolySupport.Book.Ch03.coarseCaccioppoliLocalOpenCube_one_eq_openCubeAtScale {d : ℕ} (Q : TriadicCube d) (x : Vec d) : coarseCaccioppoliLocalOpenCube Q x 1 = openCubeAtScale x (Q.scale - 1)

theorem HCPolySupport.Book.Ch03.caccioppoliCoreSet_subset_cubeSet {d : ℕ} (Q : TriadicCube d) (x : Vec d) : caccioppoliCoreSet Q x ⊆ cubeSet Q

theorem HCPolySupport.Book.Ch03.coreOpenCubeRadius_eq_scaleFactor_div_eighteen {d : ℕ} (Q : TriadicCube d) : Real.rpow 3 ↑(Q.scale - 2) / 2 = cubeScaleFactor Q / 18

theorem HCPolySupport.Book.Ch03.volume_caccioppoliCoreSet_toReal_ge_scaleFactor_div_eighteen_pow {d : ℕ} (Q : TriadicCube d) {x : Vec d} (hx : x ∈ openCubeSet Q) : (cubeScaleFactor Q / 18) ^ d ≤ (MeasureTheory.volume (caccioppoliCoreSet Q x)).toReal

theorem HCPolySupport.Book.Ch03.caccioppoliCoreSet_volumeRatio_le_eighteen_pow {d : ℕ} (Q : TriadicCube d) {x : Vec d} (hx : x ∈ openCubeSet Q) : (MeasureTheory.volume (caccioppoliCoreSet Q x)).toReal⁻¹ * cubeVolume Q ≤ 18 ^ d

theorem HCPolySupport.Book.Ch03.boundaryCaccioppoliCoreEnergy_le_eighteen_pow_mul_localEnergyRadiusProfile {d : ℕ} [NeZero d] {Q : TriadicCube d} {a : CoeffFamily d} {x : Vec d} (u : BoundaryCaccioppoliDatum Q a x) (hx : x ∈ openCubeSet Q) : boundaryCaccioppoliCoreEnergy u ≤ 18 ^ d * coarseCaccioppoliLocalEnergyRadiusProfile Q x (fun (y : Vec d) => scalarVariationEnergyIntegrand (pointwiseCoeffFor Q a) u.toPointwiseAHarmonic y) 3⁻¹

theorem HCPolySupport.Book.Ch03.interiorCaccioppoliCoreEnergy_le_eighteen_pow_mul_localEnergyRadiusProfile {d : ℕ} [NeZero d] {Q : TriadicCube d} {a : CoeffFamily d} {x : Vec d} (u : CubeSolution Q a) (hx : x ∈ openCubeSet Q) : interiorCaccioppoliCoreEnergy Q a x u ≤ 18 ^ d * coarseCaccioppoliLocalEnergyRadiusProfile Q x (fun (y : Vec d) => scalarVariationEnergyIntegrand (pointwiseCoeffFor Q a) u.toPointwiseAHarmonic y) 3⁻¹