Coarse-graining support:

Support.Deterministic.HomogenizationBlackBoxes.DualityPositiveBridge.SharpLoss

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

Sharp-loss positive-test route

This file keeps the honest low-exponent sharp-boundary loss visible in the scalar duality assembly. The bridge is only used for exponents below 1/2, and the public RHS carries the corresponding factor 1 + sqrt (sharpBoundaryKernelLoss d t).

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

Genuine-dual solution-comparison estimate with the sharp boundary loss shown explicitly.

Equations

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

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

One-parameter concrete/circ scalar duality estimate with the flux defect measured at s / 2 and the sharp-boundary bridge loss displayed.

Equations

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

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

Two-exponent concrete/circ scalar duality estimate with the manuscript loss s^{-1} t^{-2} (1/2 - t)^{-1}.

Equations

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

noncomputable def HCPolySupport.sharpBoundaryKernelNoteConstant (d : ℕ) : ℝ

Dimension-only constant bounding the sharp-boundary loss by the displayed (1/2 - t)^{-1} singularity.

Equations

• HCPolySupport.sharpBoundaryKernelNoteConstant d = 1 + √(8 * 3 ^ d + 100 * HCPolySupport.sharpBoundaryKernelConstant d ^ 2)

theorem HCPolySupport.sharpBoundaryKernelNoteConstant_nonneg (d : ℕ) : 0 ≤ sharpBoundaryKernelNoteConstant d

theorem HCPolySupport.one_add_sqrt_sharpBoundaryKernelLoss_le_noteConstant {d : ℕ} [NeZero d] {t : ℝ} (ht : 0 < t) (ht_lt_half : t < 1 / 2) : 1 + √(sharpBoundaryKernelLoss d t) ≤ sharpBoundaryKernelNoteConstant d * (1 / 2 - t)⁻¹

theorem HCPolySupport.besovExponentLossGap_le_note {s t : ℝ} (hs : 0 < s) (ht : 0 < t) (hts : t < s / 2) (hs_lt_one : s < 1) : besovExponentLossGap s t ≤ 110 * s⁻¹ * t⁻¹

The Ch1 exponent-loss gap has the note-facing two-exponent singularity when the input exponent is below half the output exponent.

theorem HCPolySupport.exists_coordinateDirichletSolution_overlappingPositiveNorm_le_sharpLoss {d : ℕ} [NeZero d] {Cdir Cbridge : ℝ} (hdir : DiscreteConstantCoefficientDirichletBesovFunctionSpacesUniform d Cdir) (hbridge : UnitFullDualCoordinateOverlappingBridgeSharpLoss d Cbridge) (Q : TriadicCube d) {s : ℝ} (i : Fin d) (g : Vec d → ℝ) (hs : 0 < s) (hs_lt_half : s < 1 / 2) (hg : CubeBesovDualFullTest Q s 2 2 g) : ∃ (w : H10Function (openCubeSet Q)), CubeDirichletDivergenceProblem Q w (coordinateVectorField i g) ∧ (CubeVectorOverlappingBesovHRegularity Q s fun (x : Vec d) => w.grad x) ∧ (cubeBesovOverlappingPositiveVectorNormTwo Q s fun (x : Vec d) => w.grad x) ≤ Cdir * (Cbridge * (1 + √(sharpBoundaryKernelLoss d s)) * cubeBesovScaleWeight (-s) Q)

Coordinate-test Dirichlet solution bound using the low-exponent sharp-loss bridge.

theorem HCPolySupport.scalarSolutionComparisonGenuineDualityEstimateSharpLoss_of_component_fullTest_pairing_bounds {d : ℕ} [NeZero d] {Cpair : ℝ} (hCpair : 0 ≤ Cpair) (hSigma : ∀ (Q : TriadicCube d) (sigma0 : ℝ) (w F : Vec d → Vec d) {t : ℝ} (j : ℕ), 0 < sigma0 → 0 < t → t < 1 / 2 → MemVectorL2 (cubeSet Q) F → IsPotentialZeroTraceOn (cubeSet Q) w → (IsSolenoidalOn (cubeSet Q) fun (x : Vec d) => matVecMul (scalarMatrix sigma0) (w x) + F x) → ∀ (i : Fin d) (g : Vec d → ℝ), CubeBesovDualFullTest Q t 2 2 g → |cubeBesovPairing Q (fun (x : Vec d) => matVecMul (scalarMatrix sigma0) (w x) i) g| ≤ Cpair * (1 + √(sharpBoundaryKernelLoss d t)) * t⁻¹ * cubeBesovScaleWeight (-t) Q * localizedFluxDefectNegativeBesovAverageTwo Q t F j) (hFlux : ∀ (Q : TriadicCube d) (sigma0 : ℝ) (w F : Vec d → Vec d) {t : ℝ} (j : ℕ), 0 < sigma0 → 0 < t → t < 1 / 2 → MemVectorL2 (cubeSet Q) F → IsPotentialZeroTraceOn (cubeSet Q) w → (IsSolenoidalOn (cubeSet Q) fun (x : Vec d) => matVecMul (scalarMatrix sigma0) (w x) + F x) → ∀ (i : Fin d) (g : Vec d → ℝ), CubeBesovDualFullTest Q t 2 2 g → |cubeBesovPairing Q (fun (x : Vec d) => (matVecMul (scalarMatrix sigma0) (w x) + F x) i) g| ≤ Cpair * (1 + √(sharpBoundaryKernelLoss d t)) * t⁻¹ * cubeBesovScaleWeight (-t) Q * localizedFluxDefectNegativeBesovAverageTwo Q t F j) : ScalarSolutionComparisonGenuineDualityEstimateSharpLoss d (2 * ↑(Fintype.card (Fin d)) * Cpair)

Componentwise scalar full-dual pairing bounds with the sharp loss control the vector genuine-dual solution-comparison estimate with the same displayed loss.

theorem HCPolySupport.scalarSolutionComparisonGenuineDualityEstimateSharpLoss {d : ℕ} [NeZero d] {Cdir Cbridge Cpairing : ℝ} (hdir : DiscreteConstantCoefficientDirichletBesovFunctionSpacesUniform d Cdir) (hbridge : UnitFullDualCoordinateOverlappingBridgeSharpLoss d Cbridge) (hpair : LocalizedFluxDefectPositivePairingEstimate d Cpairing) : ScalarSolutionComparisonGenuineDualityEstimateSharpLoss d (2 * ↑(Fintype.card (Fin d)) * (Cpairing * (Cdir + 1) * Cbridge))

Close the genuine-dual scalar solution-comparison estimate from the restored LaTeX argument, but using the honest low-exponent coordinate bridge with the sharp-boundary loss displayed.

theorem HCPolySupport.ScalarSolutionComparisonGenuineDualityEstimateSharpLoss.to_halfExponentSharpLoss {d : ℕ} {C : ℝ} (hdual : ScalarSolutionComparisonGenuineDualityEstimateSharpLoss d C) : ScalarSolutionComparisonDualityEstimateHalfExponentSharpLoss d (110 * C)

Specialize the sharp-loss genuine-dual estimate to t = s / 2 and compose with the proved Ch1 dual-to-circ exponent-loss embedding.

theorem HCPolySupport.ScalarSolutionComparisonGenuineDualityEstimateSharpLoss.to_exponentLoss {d : ℕ} [NeZero d] {C : ℝ} (hdual : ScalarSolutionComparisonGenuineDualityEstimateSharpLoss d C) : ScalarSolutionComparisonDualityEstimateExponentLoss d (110 * sharpBoundaryKernelNoteConstant d * C)

Keep the two exponents exposed and absorb the sharp-boundary and dual-to-circ geometric factors into the note-facing s^{-1} t^{-2} (1/2 - t)^{-1} loss.

theorem HCPolySupport.solutionNegativeBesovLhs_le_of_halfExponentSharpLoss {d : ℕ} {C : ℝ} (hduality : ScalarSolutionComparisonDualityEstimateHalfExponentSharpLoss d C) (Q : TriadicCube d) (a : CoeffField d) (sigma0 : ℝ) (gradU gradV : Vec d → Vec d) {s : ℝ} (j : ℕ) (hsigma0 : 0 < sigma0) (hs_pos : 0 < s) (hs_lt_one : s < 1) (hF : MemVectorL2 (cubeSet Q) (fluxDefect a (scalarMatrix sigma0) gradU)) (hcomparison : IsHomogenizationComparisonPairOn (cubeSet Q) a (scalarMatrix sigma0) gradU gradV) : solutionComparisonNegativeBesovLhs Q s a (scalarMatrix sigma0) gradU gradV ≤ C * (1 + √(sharpBoundaryKernelLoss d (s / 2))) * s⁻¹ ^ 3 * localizedFluxDefectNegativeBesovAverageTwo Q (s / 2) (fluxDefect a (scalarMatrix sigma0) gradU) j

Use the sharp-loss half-exponent scalar-background duality estimate on a comparison pair.

theorem HCPolySupport.solutionComparisonNegativeBesovLhs_le_of_scalarSolutionComparisonDualityEstimateExponentLoss {d : ℕ} {C : ℝ} (hduality : ScalarSolutionComparisonDualityEstimateExponentLoss d C) (Q : TriadicCube d) (a : CoeffField d) (sigma0 : ℝ) (gradU gradV : Vec d → Vec d) {s t : ℝ} (j : ℕ) (hsigma0 : 0 < sigma0) (hs_pos : 0 < s) (ht_pos : 0 < t) (hts : t < s / 2) (hs_lt_one : s < 1) (hF : MemVectorL2 (cubeSet Q) (fluxDefect a (scalarMatrix sigma0) gradU)) (hcomparison : IsHomogenizationComparisonPairOn (cubeSet Q) a (scalarMatrix sigma0) gradU gradV) : solutionComparisonNegativeBesovLhs Q s a (scalarMatrix sigma0) gradU gradV ≤ C * s⁻¹ * t⁻¹ ^ 2 * (1 / 2 - t)⁻¹ * localizedFluxDefectNegativeBesovAverageTwo Q t (fluxDefect a (scalarMatrix sigma0) gradU) j

Use the two-exponent scalar-background duality estimate on a comparison pair.