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

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

Weak-solution bridges for the RHS weak-flux lane

This file starts the Section 3.2.3 development by exposing the existing RHS Poincare machinery through the same H¹ weak-solution predicate used by the Section 3.3 black boxes. The theorem below controls the gradient field; the full weak-flux estimate still needs the local Neumann-correction and harmonic-flux recurrence from manuscript lines 1720--2224.

theorem HCPolySupport.exists_centeredNeumannCorrector_aHarmonicRemainder_of_h1DirichletRhsWeakSolutionOn {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (g : Vec d → Vec d) (u : H1Function (cubeSet Q)) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hu : IsH1DirichletRhsWeakSolutionOn a (cubeSet Q) u g) (hg : MemVectorL2 (cubeSet Q) g) (hC : H1CoerciveEstimate (cubeSet Q)) : ∃ (ω : MeanZeroNeumannCorrectorData Q a fun (x : Vec d) => g x - cubeAverageVec Q g) (w : AHarmonicFunction a (cubeSet Q)), ∀ x ∈ cubeSet Q, u.grad x = w.toH1.grad x + ω.toH1MeanZero.toH1Function.grad x

Build the centered Neumann corrector and the corresponding harmonic remainder directly from an H¹ RHS weak solution on one cube.

This is the manuscript Step 1 interface for Section 3.2.3, modulo the supplied mean-zero coercive estimate on the half-open cube.

theorem HCPolySupport.exists_centeredNeumannCorrector_aHarmonicRemainder_fluxStepEnergy_of_h1DirichletRhsWeakSolutionOn {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (g : Vec d → Vec d) (u : H1Function (cubeSet Q)) {s lam Lam : ℝ} (hs : 0 < s) (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hu : IsH1DirichletRhsWeakSolutionOn a (cubeSet Q) u g) (hg : MemVectorL2 (cubeSet Q) g) (hC : H1CoerciveEstimate (cubeSet Q)) (N : ℕ) : ∃ (ω : MeanZeroNeumannCorrectorData Q a fun (x : Vec d) => g x - cubeAverageVec Q g) (w : AHarmonicFunction a (cubeSet Q)), (∀ x ∈ cubeSet Q, u.grad x = w.toH1.grad x + ω.toH1MeanZero.toH1Function.grad x) ∧ ∀ (energy : Vec d → ℝ), (∀ x ∈ cubeSet Q, 0 ≤ energy x) → MeasureTheory.IntegrableOn energy (cubeSet Q) MeasureTheory.volume → CubeAverageFluxEnergyControl Q a (fun (x : Vec d) => matVecMul (a x) (w.toH1.grad x)) energy → (Summable fun (n : ℕ) => geometricWeight s 2 n * maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a) → (cubeBesovNegativeVectorPartialSeminormTwo Q s (N + 1) fun (x : Vec d) => matVecMul (a x) (u.grad x)) ^ 2 ≤ (Real.rpow 3 (-2 * s) * descendantsAverage Q 1 fun (R : TriadicCube d) => (cubeBesovNegativeVectorPartialSeminormTwo R s N fun (x : Vec d) => matVecMul (a x) (u.grad x)) ^ 2) + (geometricDiscount s 2)⁻¹ * LambdaSq Q s (MultiscaleExponent.finite 2) a * cubeAverage Q energy

One-cube PDE-facing local recurrence interface for the weak-flux RHS lane.

Starting from an H¹ RHS weak solution, this constructs the centered Neumann corrector and harmonic remainder, and packages the flux local-step estimate for any supplied descendant flux-energy control of that harmonic remainder. This is the Lean counterpart of manuscript Section 3.2.3, Steps 1--3, at the single-cube interface level.

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

PDE-facing wrapper around the q=2 RHS Poincare final theorem.

If u solves -div(a grad u) = div g on Q, then grad u is a potential field whose residual flux a grad u - g is solenoidal. This packages those two facts and applies negativeBesovSeminormTwo_le_sqrt_intrinsicGlobalEnergyForce_of_parent_potential.

This is an infrastructure step for p.weak.flux.RHS.deterministic.theory, not the final weak-flux estimate.

theorem HCPolySupport.negativeBesovSeminormTwo_grad_le_sqrt_of_h1DirichletRhsWeakSolutionOn {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (g : Vec d → Vec d) (u : H1Function (cubeSet Q)) {s lam Lam : ℝ} (hs : 0 < s) (hs_le : s ≤ 1) (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hu : IsH1DirichletRhsWeakSolutionOn a (cubeSet Q) u g) (hg : CubeVectorBesovHRegularity Q s g) : cubeBesovNegativeVectorSeminormTwo Q s u.grad ≤ √(250 * s⁻¹ ^ 2 * (lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ * cubeAverage Q (coefficientEnergyDensity a u.grad) + 15000 * s⁻¹ ^ 4 * (lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ ^ 2 * (↑d * (3 ^ (↑d + s) * √2)) ^ 2 * cubeBesovPositiveVectorSeminormTwo Q s g ^ 2)

PDE-facing RHS Poincare estimate with the manuscript g ∈ H^s regularity package, rather than separate L² and positive-Besov boundedness hypotheses.