Coarse-graining support: Support.Book.Ch03.ABK26.LocalCoarseGrainingPDE

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

Local coarse-graining PDE bridges

This module transports the source-facing weak equation and finite-p forcing assumption to the internal carriers used by local coarse-graining estimates. The public statements retain CoeffOn; pointwise coefficient representatives are confined to the private bridge to the legacy weak-solution predicate.

theorem HCPolySupport.Book.Ch03.ABK26.IsForcedEquation.restrictToDescendant {d : ℕ} {Q R : TriadicCube d} {n : ℤ} (hn : n ≤ Q.scale) (hR : R ∈ descendantsAtScale Q n) {a : Ch02.CoeffOn (Ch02.cubeDomain Q)} {u : H1Function (openCubeSet Q)} {g : Vec d → Vec d} (h : IsForcedEquation Q a u g) : IsForcedEquation R (a.restrictToSubcube ⋯) (restrictH1ToSubcube u ⋯) g

The source weak equation restricts to every descendant by zero-extending the descendant test function.

theorem HCPolySupport.Book.Ch03.ABK26.MemCubeEuclideanFullWsp.memLpTwoOnDescendant {d : ℕ} {Q R : TriadicCube d} {n : ℤ} {s : ↑FractionalOrder} {p : FiniteLpExponent} {g : Vec d → Vec d} (hn : n ≤ Q.scale) (hR : R ∈ descendantsAtScale Q n) (hp : 2 ≤ p.exponent) (h : MemCubeEuclideanFullWsp Q s p g) : MeasureTheory.MemLp (fun (x : Vec d) => HilbertVec.ofVec (g x)) 2 (normalizedCubeMeasure R)

Finite-p source forcing is L² on every descendant whenever p ≥ 2.

theorem HCPolySupport.Book.Ch03.ABK26.IsForcedEquation.toIsH1DirichletRhsWeakSolutionOnNeg {d : ℕ} {Q : TriadicCube d} {a : Ch02.CoeffOn (Ch02.cubeDomain Q)} {u : H1Function (openCubeSet Q)} {g : Vec d → Vec d} (h : IsForcedEquation Q a u g) : IsH1DirichletRhsWeakSolutionOn a.toCoeffField (openCubeSet Q) u fun (x : Vec d) => -g x

The source negative-sign weak equation is the legacy weak-solution carrier with datum -g.

theorem HCPolySupport.Book.Ch03.ABK26.localSymmetricEnergyENorm_eq_coefficientEnergyDensity {d : ℕ} (R : TriadicCube d) (a : Ch02.CoeffOn (Ch02.cubeDomain R)) (u : H1Function (openCubeSet R)) : localSymmetricEnergyENorm R a u = (∫⁻ (x : Vec d), ENNReal.ofReal (coefficientEnergyDensity a.toCoeffField u.grad x) ∂normalizedCubeMeasure R) ^ (1 / 2)

The local symmetric energy is exactly the old coefficient-energy density integrated against the normalized cube measure.

theorem HCPolySupport.Book.Ch03.ABK26.localSymmetricEnergyENorm_eq_ofReal_cubeAverage_coefficientEnergyDensity {d : ℕ} (R : TriadicCube d) (a : Ch02.CoeffOn (Ch02.cubeDomain R)) (u : H1Function (openCubeSet R)) : localSymmetricEnergyENorm R a u = ENNReal.ofReal (cubeAverage R (coefficientEnergyDensity a.toCoeffField u.grad)) ^ (1 / 2)

The local symmetric energy is the square-root energy associated with the legacy normalized cube average.

theorem HCPolySupport.Book.Ch03.ABK26.localSymmetricEnergyENorm_nonneg {d : ℕ} (R : TriadicCube d) (a : Ch02.CoeffOn (Ch02.cubeDomain R)) (u : H1Function (openCubeSet R)) : 0 ≤ localSymmetricEnergyENorm R a u

The normalized local symmetric energy is nonnegative.

theorem HCPolySupport.Book.Ch03.ABK26.localSymmetricEnergyENorm_ne_top {d : ℕ} (R : TriadicCube d) (a : Ch02.CoeffOn (Ch02.cubeDomain R)) (u : H1Function (openCubeSet R)) : localSymmetricEnergyENorm R a u ≠ ⊤

The local symmetric energy is finite.