Coarse-graining support: Support.Book.Ch03.Theorems.DualityPositivePairing

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

Localized positive-test pairing

This file isolates the part of the positive-test bridge that is already available from the standard, non-overlapping Ch3 Besov duality theorem.

theorem HCPolySupport.Book.Ch03.abs_cubeAverage_vecDot_le_localized_negative_standard_positive_besov {d : ℕ} {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) (hH : ForceBesovRegularity Q s H) (hB : 0 ≤ B) (hHnorm : scaleNormalizedPositiveBesovVectorNormTwo Q s H ≤ B) : |cubeAverage Q fun (x : Vec d) => vecDot (F x) (H x)| ≤ (1 + ↑d * Real.rpow 3 (↑d + 1)) * s⁻¹ * localizedFluxDefectNegativeBesovAverageTwo Q s F j * B

Standard positive-Besov version of the localized flux-defect pairing.

The remaining bridge work is to compare the corrected overlapping positive norm used by the Dirichlet theorem with this standard positive norm.

theorem HCPolySupport.Book.Ch03.forceBesovRegularity_of_overlappingBesovHRegularity {d : ℕ} {Q : TriadicCube d} {s : ℝ} {H : Vec d → Vec d} (hH : CubeVectorOverlappingBesovHRegularity Q s H) : ForceBesovRegularity Q s H

theorem HCPolySupport.Book.Ch03.scaleNormalizedPositiveBesovVectorNormTwo_le_sqrt_three_pow_mul_overlapping {d : ℕ} (Q : TriadicCube d) (s : ℝ) (H : Vec d → Vec d) (hH : CubeVectorOverlappingBesovHRegularity Q s H) : scaleNormalizedPositiveBesovVectorNormTwo Q s H ≤ √(3 ^ d) * cubeBesovOverlappingPositiveVectorNormTwo Q s H

theorem HCPolySupport.Book.Ch03.abs_cubeAverage_vecDot_le_localized_negative_overlapping_positive_besov {d : ℕ} {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) (hH : CubeVectorOverlappingBesovHRegularity Q s H) (hB : 0 ≤ B) (hHnorm : cubeBesovOverlappingPositiveVectorNormTwo Q s H ≤ B) : |cubeAverage Q fun (x : Vec d) => vecDot (F x) (H x)| ≤ (1 + ↑d * Real.rpow 3 (↑d + 1)) * √(3 ^ d) * s⁻¹ * localizedFluxDefectNegativeBesovAverageTwo Q s F j * B

Overlapping positive-Besov version of the localized flux-defect pairing.

This is the budgeted bridge needed by the restored duality argument. It is obtained from the standard positive-Besov pairing and the finite-overlap comparison between the corrected overlapping positive norm and the standard positive norm.

theorem HCPolySupport.Book.Ch03.localizedFluxDefectPositivePairingEstimate_standardOverlap (d : ℕ) : LocalizedFluxDefectPositivePairingEstimate d ((1 + ↑d * Real.rpow 3 (↑d + 1)) * √(3 ^ d))