Coarse-graining support: Support.Deterministic.HomogenizationBlackBoxes.DualityPositiveBridge

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

Positive-test bridge helper lemmas

This file contains the shared PDE identity and full-dual bookkeeping lemmas used by the sharp-boundary scalar duality assembly. The old all-exponent coordinate bridge route has been removed from the active code path.

theorem HCPolySupport.cubeScaleNormalizedDualNegativeBesovVectorNormTwo_le_of_forall_component_fullTest_pairing_le {d : ℕ} (Q : TriadicCube d) (t : ℝ) (F : Vec d → Vec d) {B : Fin d → ℝ} (hB : ∀ (i : Fin d) (g : Vec d → ℝ), CubeBesovDualFullTest Q t 2 2 g → |cubeBesovPairing Q (fun (x : Vec d) => F x i) g| ≤ B i) : cubeScaleNormalizedDualNegativeBesovVectorNormTwo Q t F ≤ cubeBesovScaleWeight t Q * ∑ i : Fin d, B i

Componentwise scalar full-dual pairing bounds control the note-normalized vector genuine-dual negative Besov norm.

This is the bookkeeping supremum step used by the restored deterministic duality proof: after the PDE identity bounds each scalar component against every unit full-dual test, the vector norm is obtained by summing over coordinates and multiplying by the parent scale weight.

theorem HCPolySupport.cubeScaleNormalizedDualNegativeBesovVectorNormTwo_le_card_mul {d : ℕ} (Q : TriadicCube d) (t : ℝ) (F : Vec d → Vec d) {B : ℝ} (hB : ∀ (i : Fin d) (g : Vec d → ℝ), CubeBesovDualFullTest Q t 2 2 g → |cubeBesovPairing Q (fun (x : Vec d) => F x i) g| ≤ B) : cubeScaleNormalizedDualNegativeBesovVectorNormTwo Q t F ≤ cubeBesovScaleWeight t Q * (↑(Fintype.card (Fin d)) * B)

Uniform scalar full-dual pairing bounds control the note-normalized vector genuine-dual negative Besov norm with the expected coordinate-cardinality factor.

theorem HCPolySupport.exists_cubeDirichletDivergenceProblem_of_memLp_normalizedCubeMeasure {d : ℕ} [NeZero d] {Q : TriadicCube d} {h : Vec d → Vec d} (hh : MeasureTheory.MemLp h 2 (normalizedCubeMeasure Q)) : ∃ (w : H10Function (openCubeSet Q)), CubeDirichletDivergenceProblem Q w h

Any normalized-cube L² vector datum has a zero-trace weak solution to the Dirichlet divergence problem on the corresponding open cube.

theorem HCPolySupport.dirichletDivergence_solutionComparison_integral_identity {d : ℕ} [NeZero d] {Q : TriadicCube d} {sigma0 : ℝ} {w F h : Vec d → Vec d} {v : H10Function (openCubeSet Q)} (hF : MemVectorL2 (cubeSet Q) F) (hdiv : CubeDirichletDivergenceProblem Q v h) (hw : IsPotentialZeroTraceOn (cubeSet Q) w) (hsol : IsSolenoidalOn (cubeSet Q) fun (x : Vec d) => matVecMul (scalarMatrix sigma0) (w x) + F x) : ∫ (x : Vec d) in openCubeSet Q, vecDot (matVecMul (scalarMatrix sigma0) (w x)) (h x) = ∫ (x : Vec d) in openCubeSet Q, vecDot (F x) (v.grad x)

Weak-form identity behind the scalar-background solution-comparison duality argument.

If v solves the Dirichlet divergence problem with datum h, w is a zero-trace potential field, and sigma0 w + F is solenoidal, then the pairing of the scalar-background comparison field sigma0 w against h is equal to the pairing of the flux defect F against the dual solution gradient.

theorem HCPolySupport.dirichletDivergence_fluxComparison_integral_identity {d : ℕ} [NeZero d] {Q : TriadicCube d} {sigma0 : ℝ} {w F h : Vec d → Vec d} {v : H10Function (openCubeSet Q)} (hF : MemVectorL2 (cubeSet Q) F) (hh : MemVectorL2 (openCubeSet Q) h) (hdiv : CubeDirichletDivergenceProblem Q v h) (hw : IsPotentialZeroTraceOn (cubeSet Q) w) (hsol : IsSolenoidalOn (cubeSet Q) fun (x : Vec d) => matVecMul (scalarMatrix sigma0) (w x) + F x) : ∫ (x : Vec d) in openCubeSet Q, vecDot (matVecMul (scalarMatrix sigma0) (w x) + F x) (h x) = ∫ (x : Vec d) in openCubeSet Q, vecDot (F x) (v.grad x + h x)

Companion weak-form identity for the flux-comparison field sigma0 w + F. After the previous identity, the extra term is exactly the direct pairing of the flux defect F with the input dual datum h.

theorem HCPolySupport.cubeAverage_eq_inv_cubeVolume_mul_setIntegral_openCubeSet {d : ℕ} (Q : TriadicCube d) (f : Vec d → ℝ) : cubeAverage Q f = (cubeVolume Q)⁻¹ * ∫ (x : Vec d) in openCubeSet Q, f x

theorem HCPolySupport.cubeAverage_vecDot_add_right {d : ℕ} (Q : TriadicCube d) (F H K : Vec d → Vec d) (hF : MemVectorL2 (openCubeSet Q) F) (hH : MemVectorL2 (openCubeSet Q) H) (hK : MemVectorL2 (openCubeSet Q) K) : (cubeAverage Q fun (x : Vec d) => vecDot (F x) (H x + K x)) = (cubeAverage Q fun (x : Vec d) => vecDot (F x) (H x)) + cubeAverage Q fun (x : Vec d) => vecDot (F x) (K x)

Linearity of vector pairings in the test field, written for cube averages over the open-cube representative.

theorem HCPolySupport.abs_cubeAverage_vecDot_add_right_le {d : ℕ} (Q : TriadicCube d) (F H K : Vec d → Vec d) (hF : MemVectorL2 (openCubeSet Q) F) (hH : MemVectorL2 (openCubeSet Q) H) (hK : MemVectorL2 (openCubeSet Q) K) : |cubeAverage Q fun (x : Vec d) => vecDot (F x) (H x + K x)| ≤ |cubeAverage Q fun (x : Vec d) => vecDot (F x) (H x)| + |cubeAverage Q fun (x : Vec d) => vecDot (F x) (K x)|

theorem HCPolySupport.cubeBesovPairing_solutionComparison_component_eq_cubeAverage_fluxDefect_dualGradient {d : ℕ} [NeZero d] {Q : TriadicCube d} {sigma0 : ℝ} {w F : Vec d → Vec d} {v : H10Function (openCubeSet Q)} (i : Fin d) (g : Vec d → ℝ) (hF : MemVectorL2 (cubeSet Q) F) (hdiv : CubeDirichletDivergenceProblem Q v (coordinateVectorField i g)) (hw : IsPotentialZeroTraceOn (cubeSet Q) w) (hsol : IsSolenoidalOn (cubeSet Q) fun (x : Vec d) => matVecMul (scalarMatrix sigma0) (w x) + F x) : cubeBesovPairing Q (fun (x : Vec d) => matVecMul (scalarMatrix sigma0) (w x) i) g = cubeAverage Q fun (x : Vec d) => vecDot (F x) (v.grad x)

Normalized cubeBesovPairing form of dirichletDivergence_solutionComparison_integral_identity.

theorem HCPolySupport.BesovPairing_fluxComparison_component_eq_fluxDefect_dualGradient {d : ℕ} [NeZero d] {Q : TriadicCube d} {sigma0 s : ℝ} {w F : Vec d → Vec d} {v : H10Function (openCubeSet Q)} (i : Fin d) {g : Vec d → ℝ} (hg : CubeBesovDualFullTest Q s 2 2 g) (hF : MemVectorL2 (cubeSet Q) F) (hdiv : CubeDirichletDivergenceProblem Q v (coordinateVectorField i g)) (hw : IsPotentialZeroTraceOn (cubeSet Q) w) (hsol : IsSolenoidalOn (cubeSet Q) fun (x : Vec d) => matVecMul (scalarMatrix sigma0) (w x) + F x) : cubeBesovPairing Q (fun (x : Vec d) => (matVecMul (scalarMatrix sigma0) (w x) + F x) i) g = cubeAverage Q fun (x : Vec d) => vecDot (F x) (v.grad x + coordinateVectorField i g x)

Normalized cubeBesovPairing form of dirichletDivergence_fluxComparison_integral_identity.

theorem HCPolySupport.cubeBesovScaleWeight_mul_neg_self {d : ℕ} (s : ℝ) (Q : TriadicCube d) : cubeBesovScaleWeight s Q * cubeBesovScaleWeight (-s) Q = 1