Coarse-graining support: Support.Deterministic.WeakFluxRHS.CorrectorEnergyPoincare

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

Corrector energy from the RHS Poincare estimate

This leaf closes the manuscript Step 3.2.3 estimate for the local mean-zero Neumann corrector: the centered energy identity gives E <= C W G, the RHS Poincare estimate bounds W, and a scalar Young absorption returns a forcing-square envelope with the expected lambda_{s/2,2}^{-1} factor.

theorem HCPolySupport.MeanZeroNeumannCorrectorData.coefficientEnergy_average_le_centered_force_mul_sqrt_intrinsicGlobalEnergyForce {d : ℕ} {Q : TriadicCube d} {a : CoeffField d} {g : Vec d → Vec d} [NeZero d] (ω : MeanZeroNeumannCorrectorData Q a fun (x : Vec d) => g x - cubeAverageVec Q g) {s lam Lam : ℝ} (hs : 0 < s) (hs_le : s ≤ 1) (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hg : MeasureTheory.MemLp g 2 (normalizedCubeMeasure Q)) (hCenteredBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q s N fun (x : Vec d) => g x - cubeAverageVec Q g)) : cubeAverage Q (coefficientEnergyDensity a fun (x : Vec d) => ω.toH1MeanZero.toH1Function.grad x) ≤ ↑d * (3 ^ (↑d + s) * √(250 * s⁻¹ ^ 2 * (lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ * cubeAverage Q (coefficientEnergyDensity a fun (x : Vec d) => ω.toH1MeanZero.toH1Function.grad x) + 15000 * s⁻¹ ^ 4 * (lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ ^ 2 * (↑d * (3 ^ (↑d + s) * √2)) ^ 2 * (cubeBesovPositiveVectorSeminormTwo Q s fun (x : Vec d) => g x - cubeAverageVec Q g) ^ 2) * cubeBesovPositiveVectorSeminormTwo Q s fun (x : Vec d) => g x - cubeAverageVec Q g)

Pre-Young Neumann-corrector energy estimate.

The coefficient energy of the centered mean-zero Neumann corrector is bounded by the centered positive-Besov forcing seminorm times the square root of the RHS Poincare radicand for the same corrector gradient.

theorem HCPolySupport.MeanZeroNeumannCorrectorData.coefficientEnergy_average_le_forcing_square_envelope_noteConstants_expanded_centered {d : ℕ} {Q : TriadicCube d} {a : CoeffField d} {g : Vec d → Vec d} [NeZero d] (ω : MeanZeroNeumannCorrectorData Q a fun (x : Vec d) => g x - cubeAverageVec Q g) {s lam Lam : ℝ} (hs : 0 < s) (hs_le : s ≤ 1) (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hg : MeasureTheory.MemLp g 2 (normalizedCubeMeasure Q)) (hCenteredBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q s N fun (x : Vec d) => g x - cubeAverageVec Q g)) : cubeAverage Q (coefficientEnergyDensity a fun (x : Vec d) => ω.toH1MeanZero.toH1Function.grad x) ≤ (↑d * (3 ^ (↑d + s) * cubeBesovPositiveVectorSeminormTwo Q s fun (x : Vec d) => g x - cubeAverageVec Q g)) ^ 2 * (250 * s⁻¹ ^ 2 * (lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a)⁻¹) + 2 * |↑d * (3 ^ (↑d + s) * cubeBesovPositiveVectorSeminormTwo Q s fun (x : Vec d) => g x - cubeAverageVec Q g)| * √(15000 * s⁻¹ ^ 4 * (lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ ^ 2 * (↑d * (3 ^ (↑d + s) * √2)) ^ 2 * (cubeBesovPositiveVectorSeminormTwo Q s fun (x : Vec d) => g x - cubeAverageVec Q g) ^ 2)

Young-absorbed Neumann-corrector energy estimate with the centered forcing seminorm kept explicit.

theorem HCPolySupport.MeanZeroNeumannCorrectorData.coefficientEnergy_average_le_forcing_square_envelope_noteConstants_expanded {d : ℕ} {Q : TriadicCube d} {a : CoeffField d} {g : Vec d → Vec d} [NeZero d] (ω : MeanZeroNeumannCorrectorData Q a fun (x : Vec d) => g x - cubeAverageVec Q g) {s lam Lam : ℝ} (hs : 0 < s) (hs_le : s ≤ 1) (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hg : MeasureTheory.MemLp g 2 (normalizedCubeMeasure Q)) (hGlobalBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q s N g)) : cubeAverage Q (coefficientEnergyDensity a fun (x : Vec d) => ω.toH1MeanZero.toH1Function.grad x) ≤ (↑d * (3 ^ (↑d + s) * cubeBesovPositiveVectorSeminormTwo Q s g)) ^ 2 * (250 * s⁻¹ ^ 2 * (lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a)⁻¹) + 2 * |↑d * (3 ^ (↑d + s) * cubeBesovPositiveVectorSeminormTwo Q s g)| * √(15000 * s⁻¹ ^ 4 * (lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ ^ 2 * (↑d * (3 ^ (↑d + s) * √2)) ^ 2 * cubeBesovPositiveVectorSeminormTwo Q s g ^ 2)

Young-absorbed Neumann-corrector energy estimate with the uncentered forcing seminorm, using the standard invariance of the positive Besov seminorm under subtracting the cube average.

theorem HCPolySupport.MeanZeroNeumannCorrectorData.coefficientEnergy_average_le_force_scale_noteConstants_expanded {d : ℕ} {Q : TriadicCube d} {a : CoeffField d} {g : Vec d → Vec d} [NeZero d] (ω : MeanZeroNeumannCorrectorData Q a fun (x : Vec d) => g x - cubeAverageVec Q g) {s lam Lam : ℝ} (hs : 0 < s) (hs_le : s ≤ 1) (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hg : MeasureTheory.MemLp g 2 (normalizedCubeMeasure Q)) (hGlobalBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q s N g)) : cubeAverage Q (coefficientEnergyDensity a fun (x : Vec d) => ω.toH1MeanZero.toH1Function.grad x) ≤ 500 * s⁻¹ ^ 2 * (lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ * (↑d * (3 ^ (↑d + s) * √2)) ^ 2 * cubeBesovPositiveVectorSeminormTwo Q s g ^ 2

Single-scale force-form consequence of the Young-absorbed Neumann-corrector energy estimate.

This is the local scalar estimate needed before averaging the corrector-energy component over descendants: the two terms in the Young envelope are both absorbed into the same s^{-2} lambda^{-1} N^2 [g]^2 scale.