Coarse-graining support:

Support.Deterministic.HomogenizationBlackBoxes.DualityPositiveBridge.Contracts

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

Positive-test bridge contracts

The restored proof of the deterministic flux-defect duality lemma tests each component of the solution-comparison field against a scalar unit full-dual positive Besov test. To feed that test into the discrete compatibility Dirichlet theorem, we insert the scalar test into one vector coordinate and need the resulting vector field to be admissible for the overlapping positive norm used by the discrete compatibility statement DiscreteConstantCoefficientDirichletBesovFunctionSpacesUniform (not the source theorem pending the continuum K/H^s gate).

This file records that bridge with the true target norm. The MemLp part is formal and proved here; the remaining analytic comparison is the finite-overlap positive-localization estimate.

def HCPolySupport.coordinateVectorField {d : ℕ} (i : Fin d) (g : Vec d → ℝ) : Vec d → Vec d

Insert a scalar field into one vector coordinate.

Equations

• HCPolySupport.coordinateVectorField i g x j = if j = i then g x else 0

@[simp]

theorem HCPolySupport.coordinateVectorField_same {d : ℕ} (i : Fin d) (g : Vec d → ℝ) (x : Vec d) : coordinateVectorField i g x i = g x

@[simp]

theorem HCPolySupport.coordinateVectorField_of_ne {d : ℕ} {i j : Fin d} (hji : j ≠ i) (g : Vec d → ℝ) (x : Vec d) : coordinateVectorField i g x j = 0

@[simp]

theorem HCPolySupport.vecDot_coordinateVectorField {d : ℕ} (U : Vec d → Vec d) (i : Fin d) (g : Vec d → ℝ) (x : Vec d) : vecDot (U x) (coordinateVectorField i g x) = U x i * g x

@[simp]

theorem HCPolySupport.vecDot_coordinateVectorField_left {d : ℕ} (U : Vec d → Vec d) (i : Fin d) (g : Vec d → ℝ) (x : Vec d) : vecDot (coordinateVectorField i g x) (U x) = g x * U x i

theorem HCPolySupport.cubeBesovPairing_component_eq_cubeAverage_vecDot_coordinateVectorField {d : ℕ} (Q : TriadicCube d) (U : Vec d → Vec d) (i : Fin d) (g : Vec d → ℝ) : cubeBesovPairing Q (fun (x : Vec d) => U x i) g = cubeAverage Q fun (x : Vec d) => vecDot (U x) (coordinateVectorField i g x)

A scalar component pairing is the vector pairing against the corresponding coordinate-inserted vector field.

theorem HCPolySupport.coordinateVectorField_memLp_of_cubeBesovDualFullTest_two_two {d : ℕ} {Q : TriadicCube d} {s : ℝ} {i : Fin d} {g : Vec d → ℝ} (hg : CubeBesovDualFullTest Q s 2 2 g) : MeasureTheory.MemLp (coordinateVectorField i g) 2 (normalizedCubeMeasure Q)

Unit full-dual tests at p=q=2 are L²; inserting such a test into one coordinate gives an L² vector field on the parent cube.

def HCPolySupport.LocalizedFluxDefectPositivePairingEstimate (d : ℕ) (C : ℝ) : Prop

The remaining local analytic estimate in budget form.

It pairs a flux-defect field F against any vector test field whose corrected overlapping positive Besov norm is bounded by a caller-supplied budget B. The explicit regularity hypothesis is part of the honest sSup interface: without bounded positive partial sums, the full norm cannot be used to recover finite-level test bounds. The right side is the localized negative Besov flux-defect average times that positive test budget, with the explicit s⁻¹ loss from the LaTeX proof.

Equations

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

theorem HCPolySupport.LocalizedFluxDefectPositivePairingEstimate.nonneg {d : ℕ} {C : ℝ} (hpair : LocalizedFluxDefectPositivePairingEstimate d C) : 0 ≤ C

theorem HCPolySupport.LocalizedFluxDefectPositivePairingEstimate.bound {d : ℕ} {C : ℝ} (hpair : LocalizedFluxDefectPositivePairingEstimate d C) (Q : TriadicCube d) {s : ℝ} (j : ℕ) (F H : Vec d → Vec d) (B : ℝ) (hs : 0 < s) (hs_lt_one : s < 1) (hF : MemVectorL2 (cubeSet Q) F) (hHreg : CubeVectorOverlappingBesovHRegularity Q s H) (hB : 0 ≤ B) (hH : cubeBesovOverlappingPositiveVectorNormTwo Q s H ≤ B) : |cubeAverage Q fun (x : Vec d) => vecDot (F x) (H x)| ≤ C * s⁻¹ * localizedFluxDefectNegativeBesovAverageTwo Q s F j * B