Coarse-graining support: Support.Deterministic.CoarsePoincareRHS.FinalTheorems.ZeroDirichletEnergy

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

Zero-Dirichlet RHS energy bridge

This leaf packages the note-facing bridge between the zero-trace energy identity and the expanded coarse-Poincare-with-RHS estimate. The final Young absorption is intentionally left as a separate algebraic step.

noncomputable def HCPolySupport.zeroTraceDirichletEnergyEnvelope {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (g : Vec d → Vec d) : ℝ

The note-facing forcing-square envelope for the coefficient energy of a zero-trace RHS corrector.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.ZeroTraceDirichletCorrectorData.coefficientEnergy_average_le_centered_force_mul_sqrt_intrinsicGlobalEnergyForce {d : ℕ} [NeZero d] {Q : TriadicCube d} {a : CoeffField d} {g : Vec d → Vec d} (ρ : ZeroTraceDirichletCorrectorData Q a 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)) (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) => ρ.toH10.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) => ρ.toH10.grad x) + 15000 * s⁻¹ ^ 4 * (lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ ^ 2 * (↑d * (3 ^ (↑d + s) * √2)) ^ 2 * cubeBesovPositiveVectorSeminormTwo Q s g ^ 2) * cubeBesovPositiveVectorSeminormTwo Q s fun (x : Vec d) => g x - cubeAverageVec Q g)

Pre-Young zero-Dirichlet energy estimate.

The coefficient energy of the zero-trace corrector is bounded by the centered positive-Besov forcing seminorm times the square-root coarse-Poincare RHS bound for the same corrector gradient. This is the faithful formal socket immediately before the manuscript's Young absorption step.

theorem HCPolySupport.ZeroTraceDirichletCorrectorData.coefficientEnergy_average_le_forcing_square_envelope_noteConstants_expanded {d : ℕ} [NeZero d] {Q : TriadicCube d} {a : CoeffField d} {g : Vec d → Vec d} (ρ : ZeroTraceDirichletCorrectorData Q a 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) => ρ.toH10.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)

Zero-Dirichlet energy estimate after the sharp Young absorption.

This turns the pre-Young energy/Poincare bridge into the note-facing sharp envelope. The source term remains as 2 B sqrt(F) instead of being over-absorbed into the larger B^2 + F envelope.

theorem HCPolySupport.ZeroTraceDirichletCorrectorData.coefficientEnergy_average_le_zeroTraceDirichletEnergyEnvelope_noteConstants_expanded {d : ℕ} [NeZero d] {Q : TriadicCube d} {a : CoeffField d} {g : Vec d → Vec d} (ρ : ZeroTraceDirichletCorrectorData Q a 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) => ρ.toH10.grad x) ≤ zeroTraceDirichletEnergyEnvelope Q a s g

Bundled version of the Young-absorbed zero-Dirichlet energy estimate using the named forcing-square envelope.

theorem HCPolySupport.ZeroTraceDirichletCorrectorData.coefficientEnergy_average_le_zeroTraceDirichletEnergyEnvelope {d : ℕ} [NeZero d] {Q : TriadicCube d} {a : CoeffField d} {g : Vec d → Vec d} (ρ : ZeroTraceDirichletCorrectorData Q a g) {s lam Lam : ℝ} (hs : 0 < s) (hs_le : s ≤ 1) (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hg : CubeVectorBesovHRegularity Q s g) : cubeAverage Q (coefficientEnergyDensity a fun (x : Vec d) => ρ.toH10.grad x) ≤ zeroTraceDirichletEnergyEnvelope Q a s g

Zero-Dirichlet energy estimate with the manuscript g ∈ H^s regularity package, rather than separate L² and positive-Besov boundedness hypotheses.

theorem HCPolySupport.coefficientEnergy_average_le_of_isZeroTraceDirichletRhsWeakSolution {d : ℕ} [NeZero d] {Q : TriadicCube d} {a : CoeffField d} {g : Vec d → Vec d} (v : H10Function (cubeSet Q)) {s lam Lam : ℝ} (hs : 0 < s) (hs_le : s ≤ 1) (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hweak : IsZeroTraceDirichletRhsWeakSolution a (cubeSet Q) v g) (hg : CubeVectorBesovHRegularity Q s g) : cubeAverage Q (coefficientEnergyDensity a fun (x : Vec d) => v.grad x) ≤ zeroTraceDirichletEnergyEnvelope Q a s g

PDE-facing zero-Dirichlet energy estimate for an explicit zero-trace weak solution, with RHS regularity supplied by the single manuscript H^s package.