Coarse-graining support: Support.Book.Ch03.Theorems.EnergyRHS.HarmonicRemainder

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

Energy RHS: Harmonic remainder estimates

theorem HCPolySupport.Book.Ch03.dirichletHarmonicRemainder_sqrt_two_energy_le_of_boundary_pairing_and_flux_bound {d : ℕ} {C Cpair Cflux : ℝ} (hCpair_nonneg : 0 ≤ Cpair) (hCflux_nonneg : 0 ≤ Cflux) (hC_absorb : √2 * Cpair * Cflux ≤ C) {Q : TriadicCube d} {a : CoeffFamily d} {s : ℝ} {g : Vec d → Vec d} (v : DirichletForcedCubeSolution Q a g) (w : AHarmonicFunction (publicCoeffField Q a) (cubeSet Q)) (hs : 0 < s) (hboundary : ForceBesovRegularity Q s (dirichletBoundaryGradientField v)) (hpairing : cubeAverage Q (coefficientEnergyDensity (publicCoeffField Q a) fun (x : Vec d) => w.toH1.grad x) ≤ (Cpair * cubeBesovNegativeVectorSeminormTwo Q s fun (x : Vec d) => matVecMul (publicCoeffField Q a x) (w.toH1.grad x)) * scaleNormalizedPositiveBesovVectorNormTwo Q s (dirichletBoundaryGradientField v)) (hflux : (cubeBesovNegativeVectorSeminormTwo Q s fun (x : Vec d) => matVecMul (publicCoeffField Q a x) (w.toH1.grad x)) ≤ Cflux * s.rpow (-(1 / 2)) * poincareUpperEllipticityFactor Q a s (Ch02.MultiscaleExponent.finite 2) * √(cubeAverage Q (coefficientEnergyDensity (publicCoeffField Q a) fun (x : Vec d) => w.toH1.grad x))) : √(2 * cubeAverage Q (coefficientEnergyDensity (publicCoeffField Q a) fun (x : Vec d) => w.toH1.grad x)) ≤ C * s.rpow (-(1 / 2)) * poincareUpperEllipticityFactor Q a s (Ch02.MultiscaleExponent.finite 2) * scaleNormalizedPositiveBesovVectorNormTwo Q s (dirichletBoundaryGradientField v)

Boundary harmonic-remainder energy from the two quantitative inputs used in the manuscript: the weak-testing/Besov-duality pairing and the homogeneous coarse-grained flux estimate. This deliberately keeps the route through poincareUpperEllipticityFactor and contains no raw Lam absorption.

theorem HCPolySupport.Book.Ch03.dirichletHarmonicRemainder_fluxSeminorm_le_poincareUpperEllipticityFactor {d : ℕ} [NeZero d] {Q : TriadicCube d} {a : CoeffFamily d} {s : ℝ} (w : AHarmonicFunction (publicCoeffField Q a) (cubeSet Q)) (hs : 0 < s) (hs_le : s ≤ 1) : (cubeBesovNegativeVectorSeminormTwo Q s fun (x : Vec d) => matVecMul (publicCoeffField Q a x) (w.toH1.grad x)) ≤ ↑d * √5 * s.rpow (-1 / 2) * poincareUpperEllipticityFactor Q a s (Ch02.MultiscaleExponent.finite 2) * √(cubeAverage Q (coefficientEnergyDensity (publicCoeffField Q a) fun (x : Vec d) => w.toH1.grad x))

Public wrapper for the homogeneous flux half of the notes' Dirichlet harmonic-remainder proof. It applies the deterministic q = 2 coarse Poincare theorem to the public coefficient representative, rewrites Λ_{s,2}^{1/2} into poincareUpperEllipticityFactor, and absorbs the geometric discount into the displayed s^(-1/2) scale loss.

theorem HCPolySupport.Book.Ch03.dirichletHarmonicRemainder_fluxPartialSeminorm_le_poincareUpperEllipticityFactor {d : ℕ} [NeZero d] {Q : TriadicCube d} {a : CoeffFamily d} {s : ℝ} (w : AHarmonicFunction (publicCoeffField Q a) (cubeSet Q)) (N : ℕ) (hs : 0 < s) (hs_le : s ≤ 1) : (cubeBesovNegativeVectorPartialSeminormTwo Q s N fun (x : Vec d) => matVecMul (publicCoeffField Q a x) (w.toH1.grad x)) ≤ ↑d * √5 * s.rpow (-1 / 2) * poincareUpperEllipticityFactor Q a s (Ch02.MultiscaleExponent.finite 2) * √(cubeAverage Q (coefficientEnergyDensity (publicCoeffField Q a) fun (x : Vec d) => w.toH1.grad x))

Finite-depth public wrapper for the homogeneous flux half of the Dirichlet harmonic-remainder proof. This is the partial-norm version consumed by the Besov-duality pairing theorem.

theorem HCPolySupport.Book.Ch03.dirichletHarmonicRemainder_energy_le_abs_boundary_pairing_of_zeroTrace {d : ℕ} [NeZero d] {Q : TriadicCube d} {a : CoeffFamily d} {g : Vec d → Vec d} (v : DirichletForcedCubeSolution Q a g) (w : AHarmonicFunction (publicCoeffField Q a) (cubeSet Q)) (hzero : IsPotentialZeroTraceOn (cubeSet Q) fun (x : Vec d) => w.toH1.grad x - dirichletBoundaryGradientField v x) : cubeAverage Q (coefficientEnergyDensity (publicCoeffField Q a) fun (x : Vec d) => w.toH1.grad x) ≤ |cubeAverage Q fun (x : Vec d) => vecDot (matVecMul (publicCoeffField Q a x) (w.toH1.grad x)) (dirichletBoundaryGradientField v x)|

Weak testing for the homogeneous Dirichlet remainder. If the difference between the homogeneous solution gradient and the prescribed boundary-extension gradient is a zero-trace potential, then testing the homogeneous equation by that difference identifies the energy with the boundary pairing.

theorem HCPolySupport.Book.Ch03.abs_cubeAverage_vecDot_le_public_negative_positive_besov_duality_of_partial_flux_bound {d : ℕ} {Q : TriadicCube d} {s Bflux : ℝ} {F H : Vec d → Vec d} (hs : 0 < s) (hs_le : s ≤ 1) (hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure Q)) (hH : ForceBesovRegularity Q s H) (hBflux : 0 ≤ Bflux) (hneg : ∀ (N : ℕ), cubeBesovNegativeVectorPartialSeminormTwo Q s N F ≤ Bflux) : |cubeAverage Q fun (x : Vec d) => vecDot (F x) (H x)| ≤ (1 + ↑d * Real.rpow 3 (↑d + 1)) * Bflux * scaleNormalizedPositiveBesovVectorNormTwo Q s H

Public q = 2 Besov-duality wrapper for the boundary pairing. It combines the depth-zero average term with the deterministic fluctuation duality estimate, and absorbs the scale weights and s ≤ 1 into the dimension-only constant 1 + d * 3^(d+1).

theorem HCPolySupport.Book.Ch03.dirichletHarmonicRemainder_boundary_pairing_le_of_zeroTrace_and_partial_flux_bound {d : ℕ} [NeZero d] {Q : TriadicCube d} {a : CoeffFamily d} {s Bflux : ℝ} {g : Vec d → Vec d} (v : DirichletForcedCubeSolution Q a g) (w : AHarmonicFunction (publicCoeffField Q a) (cubeSet Q)) (hs : 0 < s) (hs_le : s ≤ 1) (hboundary : ForceBesovRegularity Q s (dirichletBoundaryGradientField v)) (hzero : IsPotentialZeroTraceOn (cubeSet Q) fun (x : Vec d) => w.toH1.grad x - dirichletBoundaryGradientField v x) (hBflux : 0 ≤ Bflux) (hpartial : ∀ (N : ℕ), (cubeBesovNegativeVectorPartialSeminormTwo Q s N fun (x : Vec d) => matVecMul (publicCoeffField Q a x) (w.toH1.grad x)) ≤ Bflux) : cubeAverage Q (coefficientEnergyDensity (publicCoeffField Q a) fun (x : Vec d) => w.toH1.grad x) ≤ (1 + ↑d * Real.rpow 3 (↑d + 1)) * Bflux * scaleNormalizedPositiveBesovVectorNormTwo Q s (dirichletBoundaryGradientField v)

Weak testing plus the public q = 2 Besov-duality wrapper for the Dirichlet harmonic remainder, with the flux side supplied as a uniform finite-depth negative-Besov bound.

theorem HCPolySupport.Book.Ch03.dirichletHarmonicRemainder_sqrt_two_energy_le_of_zeroTrace_and_partial_flux_bound {d : ℕ} [NeZero d] {C Cflux : ℝ} (hCflux_nonneg : 0 ≤ Cflux) (hC_absorb : √2 * (1 + ↑d * Real.rpow 3 (↑d + 1)) * Cflux ≤ C) {Q : TriadicCube d} {a : CoeffFamily d} {s : ℝ} {g : Vec d → Vec d} (v : DirichletForcedCubeSolution Q a g) (w : AHarmonicFunction (publicCoeffField Q a) (cubeSet Q)) (hs : 0 < s) (hs_le : s ≤ 1) (hboundary : ForceBesovRegularity Q s (dirichletBoundaryGradientField v)) (hzero : IsPotentialZeroTraceOn (cubeSet Q) fun (x : Vec d) => w.toH1.grad x - dirichletBoundaryGradientField v x) (hpartial : ∀ (N : ℕ), (cubeBesovNegativeVectorPartialSeminormTwo Q s N fun (x : Vec d) => matVecMul (publicCoeffField Q a x) (w.toH1.grad x)) ≤ Cflux * s.rpow (-(1 / 2)) * poincareUpperEllipticityFactor Q a s (Ch02.MultiscaleExponent.finite 2) * √(cubeAverage Q (coefficientEnergyDensity (publicCoeffField Q a) fun (x : Vec d) => w.toH1.grad x))) : √(2 * cubeAverage Q (coefficientEnergyDensity (publicCoeffField Q a) fun (x : Vec d) => w.toH1.grad x)) ≤ C * s.rpow (-(1 / 2)) * poincareUpperEllipticityFactor Q a s (Ch02.MultiscaleExponent.finite 2) * scaleNormalizedPositiveBesovVectorNormTwo Q s (dirichletBoundaryGradientField v)

Harmonic-remainder energy from weak testing, public Besov duality, and a uniform finite-depth flux bound. This is the direct partial-norm form of the notes' argument and keeps the quantitative coefficient dependence in poincareUpperEllipticityFactor.

theorem HCPolySupport.Book.Ch03.dirichletHarmonicRemainder_boundary_pairing_le_of_weak_testing_and_besov_duality {d : ℕ} {Cpair : ℝ} {Q : TriadicCube d} {a : CoeffFamily d} {s : ℝ} {g : Vec d → Vec d} (v : DirichletForcedCubeSolution Q a g) (w : AHarmonicFunction (publicCoeffField Q a) (cubeSet Q)) (hweak : cubeAverage Q (coefficientEnergyDensity (publicCoeffField Q a) fun (x : Vec d) => w.toH1.grad x) ≤ |cubeAverage Q fun (x : Vec d) => vecDot (matVecMul (publicCoeffField Q a x) (w.toH1.grad x)) (dirichletBoundaryGradientField v x)|) (hduality : |cubeAverage Q fun (x : Vec d) => vecDot (matVecMul (publicCoeffField Q a x) (w.toH1.grad x)) (dirichletBoundaryGradientField v x)| ≤ (Cpair * cubeBesovNegativeVectorSeminormTwo Q s fun (x : Vec d) => matVecMul (publicCoeffField Q a x) (w.toH1.grad x)) * scaleNormalizedPositiveBesovVectorNormTwo Q s (dirichletBoundaryGradientField v)) : cubeAverage Q (coefficientEnergyDensity (publicCoeffField Q a) fun (x : Vec d) => w.toH1.grad x) ≤ (Cpair * cubeBesovNegativeVectorSeminormTwo Q s fun (x : Vec d) => matVecMul (publicCoeffField Q a x) (w.toH1.grad x)) * scaleNormalizedPositiveBesovVectorNormTwo Q s (dirichletBoundaryGradientField v)

Boundary-pairing interface for the harmonic-remainder proof. The mathematical content still sits in the two inputs: weak testing of the homogeneous equation gives the energy-to-pairing inequality, and Besov duality bounds that pairing by the negative flux seminorm times the positive boundary norm.

theorem HCPolySupport.Book.Ch03.dirichletHarmonicRemainder_sqrt_two_energy_le_of_boundary_pairing {d : ℕ} [NeZero d] {C Cpair : ℝ} (hCpair_nonneg : 0 ≤ Cpair) (hC_absorb : √2 * Cpair * (↑d * √5) ≤ C) {Q : TriadicCube d} {a : CoeffFamily d} {s : ℝ} {g : Vec d → Vec d} (v : DirichletForcedCubeSolution Q a g) (w : AHarmonicFunction (publicCoeffField Q a) (cubeSet Q)) (hs : 0 < s) (hs_le : s ≤ 1) (hboundary : ForceBesovRegularity Q s (dirichletBoundaryGradientField v)) (hpairing : cubeAverage Q (coefficientEnergyDensity (publicCoeffField Q a) fun (x : Vec d) => w.toH1.grad x) ≤ (Cpair * cubeBesovNegativeVectorSeminormTwo Q s fun (x : Vec d) => matVecMul (publicCoeffField Q a x) (w.toH1.grad x)) * scaleNormalizedPositiveBesovVectorNormTwo Q s (dirichletBoundaryGradientField v)) : √(2 * cubeAverage Q (coefficientEnergyDensity (publicCoeffField Q a) fun (x : Vec d) => w.toH1.grad x)) ≤ C * s.rpow (-(1 / 2)) * poincareUpperEllipticityFactor Q a s (Ch02.MultiscaleExponent.finite 2) * scaleNormalizedPositiveBesovVectorNormTwo Q s (dirichletBoundaryGradientField v)

Harmonic-remainder energy after the boundary pairing input is known. This closes the homogeneous flux-Poincare half of the notes' proof; the remaining analytic task is precisely to supply the weak-testing/Besov-duality pairing bound.