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

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

Deterministic homogenization black boxes: duality

This file contains the Section 3.3.A deterministic duality surface from coarsegraining/chapters/ch3_deterministic_theory.tex, lines 2804--3008.

The Lean statement is written on an arbitrary triadic cube Q and a descendant depth j. This is the existing codebase's scale convention: j represents the manuscript scale gap m - n, and the quantities cubeBesovNegativeVectorSeminormTwo are already note-normalized, i.e. they include the displayed factors 3^{-sm} and 3^{-sn}.

@[reducible, inline]

abbrev HCPolySupport.constantCoeffField {d : ℕ} (a0 : Mat d) : CoeffField d

Constant coefficient field associated to a matrix.

Equations

• HCPolySupport.constantCoeffField a0 x✝ = a0

theorem HCPolySupport.isEllipticFieldOn_constantCoeffField {d : ℕ} {U : Set (Vec d)} {a0 : Mat d} {lam0 Lam0 : ℝ} (hU : MeasurableSet U) (ha0 : IsEllipticMatrix lam0 Lam0 a0) : IsEllipticFieldOn lam0 Lam0 U (constantCoeffField a0)

A constant elliptic matrix defines an elliptic coefficient field on every measurable set.

noncomputable def HCPolySupport.fluxDefect {d : ℕ} (a : CoeffField d) (a0 : Mat d) (gradU : Vec d → Vec d) : Vec d → Vec d

The flux defect (a - a₀)∇u, written in terms of the gradient field.

Equations

• HCPolySupport.fluxDefect a a0 gradU x = HCPolySupport.matVecMul (a x) (gradU x) - HCPolySupport.matVecMul a0 (gradU x)

noncomputable def HCPolySupport.constantGradientComparison {d : ℕ} (a0 : Mat d) (gradU gradV : Vec d → Vec d) : Vec d → Vec d

The constant-coefficient gradient comparison field a₀(∇u - ∇v).

Equations

• HCPolySupport.constantGradientComparison a0 gradU gradV x = HCPolySupport.matVecMul a0 (gradU x - gradV x)

noncomputable def HCPolySupport.fluxComparison {d : ℕ} (a : CoeffField d) (a0 : Mat d) (gradU gradV : Vec d → Vec d) : Vec d → Vec d

The full flux comparison a∇u - a₀∇v.

Equations

• HCPolySupport.fluxComparison a a0 gradU gradV x = HCPolySupport.matVecMul (a x) (gradU x) - HCPolySupport.matVecMul a0 (gradV x)

def HCPolySupport.IsH1DirichletRhsWeakSolutionOn {d : ℕ} (a : CoeffField d) (U : Set (Vec d)) (u : H1Function U) (g : Vec d → Vec d) : Prop

Weak H¹ formulation of - div (a ∇u) = div g on U, tested against zero-trace functions.

Unlike IsZeroTraceDirichletRhsWeakSolution, this predicate does not impose a zero boundary condition on u; it matches the comparison hypotheses in manuscript lines 3020--3029, where only u - v ∈ H¹₀ is prescribed.

Equations

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

theorem HCPolySupport.IsH1DirichletRhsWeakSolutionOn.of_isSolenoidalOn_zero {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} {u : H1Function U} (hsol : IsSolenoidalOn U fun (x : Vec d) => matVecMul (a x) (u.grad x)) : IsH1DirichletRhsWeakSolutionOn a U u 0

An H¹ function whose flux is solenoidal solves the zero-right-hand-side weak Dirichlet equation.

theorem HCPolySupport.IsH1DirichletRhsWeakSolutionOn.of_aHarmonicFunction {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} (u : AHarmonicFunction a U) : IsH1DirichletRhsWeakSolutionOn a U u.toH1 0

A packaged a-harmonic function solves the zero-right-hand-side weak equation.

theorem HCPolySupport.IsH1DirichletRhsWeakSolutionOn.residual_solenoidal {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} {u : H1Function U} {g : Vec d → Vec d} {lam Lam : ℝ} (h : IsH1DirichletRhsWeakSolutionOn a U u g) (hEll : IsEllipticFieldOn lam Lam U a) (hg : MemVectorL2 U g) : IsSolenoidalOn U fun (x : Vec d) => matVecMul (a x) (u.grad x) - g x

The weak equation -div(a grad u) = div g, in the codebase's sign convention, says exactly that the residual flux a grad u - g is solenoidal.

def HCPolySupport.IsHomogenizationComparisonPairOn {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) (a0 : Mat d) (gradU gradV : Vec d → Vec d) : Prop

Weak formulation of the comparison system in Lemma l.duality.from.flux.defect.deterministic.theory.

The manuscript states div (a∇u - a₀∇v) = 0 and u - v ∈ H¹₀. The existing PDE layer represents these exactly as solenoidality of the flux comparison and zero-trace potentiality of the gradient difference.

Equations

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

theorem HCPolySupport.IsHomogenizationComparisonPairOn.of_aHarmonicFunctions {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {a0 : Mat d} {lam Lam lam0 Lam0 : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (ha0 : IsEllipticMatrix lam0 Lam0 a0) (u : AHarmonicFunction a U) (v : AHarmonicFunction (constantCoeffField a0) U) (hzeroTrace : IsPotentialZeroTraceOn U fun (x : Vec d) => u.toH1.grad x - v.toH1.grad x) : IsHomogenizationComparisonPairOn U a a0 u.toH1.grad v.toH1.grad

Build the comparison-pair hypothesis for a harmonic function and its constant-coefficient harmonic replacement from the manuscript boundary condition u - v ∈ H¹₀.

theorem HCPolySupport.IsHomogenizationComparisonPairOn.of_sameRhs_h1Functions {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {a0 : Mat d} {lam Lam lam0 Lam0 : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (ha0 : IsEllipticMatrix lam0 Lam0 a0) (u v : H1Function U) (g : Vec d → Vec d) (hu : IsH1DirichletRhsWeakSolutionOn a U u g) (hv : IsH1DirichletRhsWeakSolutionOn (constantCoeffField a0) U v g) (hzeroTrace : IsPotentialZeroTraceOn U fun (x : Vec d) => u.grad x - v.grad x) : IsHomogenizationComparisonPairOn U a a0 u.grad v.grad

Build the comparison-pair hypothesis from the Section 3.3.B weak equations with common right-hand side and the manuscript boundary condition u - v ∈ H¹₀.

noncomputable def HCPolySupport.solutionComparisonNegativeBesovLhs {d : ℕ} (Q : TriadicCube d) (s : ℝ) (a : CoeffField d) (a0 : Mat d) (gradU gradV : Vec d → Vec d) : ℝ

The left-hand side of the duality estimate: [a₀(∇u-∇v)]_{B^{-s}_{2,2}} + [a∇u-a₀∇v]_{B^{-s}_{2,2}}, with the note normalization already included in each cube seminorm.

Equations

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

noncomputable def HCPolySupport.localizedFluxDefectNegativeBesovAverageTwo {d : ℕ} (Q : TriadicCube d) (s : ℝ) (defect : Vec d → Vec d) (j : ℕ) : ℝ

The localized ℓ² average of the local flux-defect negative Besov seminorms. For a parent cube of scale m, depth j = m - n corresponds to the manuscript average over 3^n ℤ^d ∩ □_m.

Equations

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

theorem HCPolySupport.localizedFluxDefectNegativeBesovAverageTwo_nonneg {d : ℕ} (Q : TriadicCube d) (s : ℝ) (defect : Vec d → Vec d) (j : ℕ) : 0 ≤ localizedFluxDefectNegativeBesovAverageTwo Q s defect j

@[simp]

theorem HCPolySupport.localizedFluxDefectNegativeBesovAverageTwo_depth_zero_abs {d : ℕ} (Q : TriadicCube d) (s : ℝ) (defect : Vec d → Vec d) : localizedFluxDefectNegativeBesovAverageTwo Q s defect 0 = |cubeBesovNegativeVectorSeminormTwo Q s defect|

At depth zero the localized flux-defect average is the absolute value of the one-cube negative Besov seminorm. Later callers may remove the absolute value when they have the usual boundedness or L² hypotheses giving nonnegativity of the seminorm.

theorem HCPolySupport.localizedFluxDefectNegativeBesovAverageTwo_depth_zero_of_nonneg {d : ℕ} (Q : TriadicCube d) (s : ℝ) (defect : Vec d → Vec d) (hdefect_nonneg : 0 ≤ cubeBesovNegativeVectorSeminormTwo Q s defect) : localizedFluxDefectNegativeBesovAverageTwo Q s defect 0 = cubeBesovNegativeVectorSeminormTwo Q s defect

At depth zero, if the one-cube negative Besov seminorm is known nonnegative, the localized flux-defect average is exactly that seminorm.

theorem HCPolySupport.localizedFluxDefectNegativeBesovAverageTwo_le_sqrt_descendantsAverage_sq_of_pointwiseBound {d : ℕ} (Q : TriadicCube d) (s : ℝ) (defect : Vec d → Vec d) (j : ℕ) (B : TriadicCube d → ℝ) (hseminorm_nonneg : ∀ R ∈ descendantsAtDepth Q j, 0 ≤ cubeBesovNegativeVectorSeminormTwo R s defect) (hbound : ∀ R ∈ descendantsAtDepth Q j, cubeBesovNegativeVectorSeminormTwo R s defect ≤ B R) : localizedFluxDefectNegativeBesovAverageTwo Q s defect j ≤ √(descendantsAverage Q j fun (R : TriadicCube d) => B R ^ 2)

Localized q = 2 flux-defect averages inherit pointwise bounds on every descendant cube.

theorem HCPolySupport.localizedFluxDefectNegativeBesovAverageTwo_le_sqrt_descendantsAverage_sq_of_qonePartialBound {d : ℕ} (Q : TriadicCube d) (s : ℝ) (defect : Vec d → Vec d) (j : ℕ) (B : TriadicCube d → ℝ) (hpartial : ∀ R ∈ descendantsAtDepth Q j, ∀ (N : ℕ), cubeBesovNegativeVectorPartialSeminorm R s N defect ≤ B R) : localizedFluxDefectNegativeBesovAverageTwo Q s defect j ≤ √(descendantsAverage Q j fun (R : TriadicCube d) => B R ^ 2)

Localized q = 2 flux-defect averages from descendantwise q = 1 partial seminorm bounds. This is the handoff shape used by coarse-flux response estimates before they are averaged over descendants.

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

Direct arbitrary-matrix solution-comparison duality estimate.

This is the active deterministic interface for Lemma l.duality.from.flux.defect.deterministic.theory: the comparison fields are controlled directly by the localized flux defect. It deliberately does not depend on the abandoned Ch1 route.

Equations

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

theorem HCPolySupport.solutionComparisonNegativeBesovLhs_eq_comparisonPair {d : ℕ} (Q : TriadicCube d) (s : ℝ) (a : CoeffField d) (a0 : Mat d) (gradU gradV : Vec d → Vec d) : solutionComparisonNegativeBesovLhs Q s a a0 gradU gradV = (cubeBesovNegativeVectorSeminormTwo Q s fun (x : Vec d) => matVecMul a0 (gradU x - gradV x)) + cubeBesovNegativeVectorSeminormTwo Q s fun (x : Vec d) => matVecMul a0 (gradU x - gradV x) + fluxDefect a a0 gradU x

The comparison-pair left-hand side is exactly the pair (a₀(∇u-∇v), a₀(∇u-∇v) + (a-a₀)∇u).

theorem HCPolySupport.IsHomogenizationComparisonPairOn.comparisonPair_solenoidal {d : ℕ} {Q : TriadicCube d} {a : CoeffField d} {a0 : Mat d} {gradU gradV : Vec d → Vec d} (hcomparison : IsHomogenizationComparisonPairOn (cubeSet Q) a a0 gradU gradV) : IsSolenoidalOn (cubeSet Q) fun (x : Vec d) => matVecMul a0 (gradU x - gradV x) + fluxDefect a a0 gradU x

The solenoidal part of a homogenization comparison pair has the normal form a₀(∇u-∇v) + (a-a₀)∇u.

theorem HCPolySupport.solutionComparisonNegativeBesovLhs_le_of_solutionComparisonDualityEstimate {d : ℕ} {C : ℝ} (hduality : SolutionComparisonDualityEstimate d C) (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (gradU gradV : Vec d → Vec d) {s : ℝ} (j : ℕ) {lam0 Lam0 : ℝ} (hs_pos : 0 < s) (hs_lt_one : s < 1) (ha0 : IsEllipticMatrix lam0 Lam0 a0) (ha0symm : Matrix.IsSymm a0) (hcomparison : IsHomogenizationComparisonPairOn (cubeSet Q) a a0 gradU gradV) : solutionComparisonNegativeBesovLhs Q s a a0 gradU gradV ≤ C * localizedFluxDefectNegativeBesovAverageTwo Q s (fluxDefect a a0 gradU) j

Use the direct arbitrary-matrix solution-comparison duality estimate on a homogenization comparison pair.

theorem HCPolySupport.exists_solutionComparisonNegativeBesovLhsBound_of_solutionComparisonDualityEstimate (d : ℕ) (hduality : ∃ (C : ℝ), SolutionComparisonDualityEstimate d C) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (gradU gradV : Vec d → Vec d) {s : ℝ} (j : ℕ) {lam Lam lam0 Lam0 : ℝ}, 0 < s → s < 1 → IsEllipticFieldOn lam Lam (cubeSet Q) a → IsEllipticMatrix lam0 Lam0 a0 → Matrix.IsSymm a0 → IsHomogenizationComparisonPairOn (cubeSet Q) a a0 gradU gradV → solutionComparisonNegativeBesovLhs Q s a a0 gradU gradV ≤ C * localizedFluxDefectNegativeBesovAverageTwo Q s (fluxDefect a a0 gradU) j

Existence of a dimension-only direct duality constant gives the arbitrary-matrix Section 3.3.A duality estimate surface.

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

Direct scalar-background solution-comparison duality estimate.

This is the scalar form consumed by the existing Chapter 3 coarse-graining wrappers. It is a direct flux-defect duality input, not a proof obligation about the abandoned Ch1 route.

Equations

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

theorem HCPolySupport.SolutionComparisonDualityEstimate.to_scalar {d : ℕ} {C : ℝ} (hduality : SolutionComparisonDualityEstimate d C) : ScalarSolutionComparisonDualityEstimate d C

The arbitrary-matrix direct duality estimate specializes to the scalar route.

theorem HCPolySupport.exists_scalarSolutionComparisonDualityEstimate_of_solutionComparisonDualityEstimate {d : ℕ} (hduality : ∃ (C : ℝ), SolutionComparisonDualityEstimate d C) : ∃ (C : ℝ), ScalarSolutionComparisonDualityEstimate d C

Existence of the arbitrary-matrix direct duality constant implies the scalar one.

theorem HCPolySupport.solutionComparisonNegativeBesovLhs_le_of_scalarSolutionComparisonDualityEstimate {d : ℕ} {C : ℝ} (hduality : ScalarSolutionComparisonDualityEstimate 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) (hcomparison : IsHomogenizationComparisonPairOn (cubeSet Q) a (scalarMatrix sigma0) gradU gradV) : solutionComparisonNegativeBesovLhs Q s a (scalarMatrix sigma0) gradU gradV ≤ C * s⁻¹ * localizedFluxDefectNegativeBesovAverageTwo Q s (fluxDefect a (scalarMatrix sigma0) gradU) j

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

theorem HCPolySupport.exists_scalarSolutionComparisonDualityConstant_of_scalarSolutionComparisonDualityEstimate (d : ℕ) (hduality : ∃ (C : ℝ), ScalarSolutionComparisonDualityEstimate d C) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (Q : TriadicCube d) (a : CoeffField d) (sigma0 : ℝ) (gradU gradV : Vec d → Vec d) {s : ℝ} (j : ℕ) {lam Lam : ℝ}, 0 < sigma0 → 0 < s → s < 1 → IsEllipticFieldOn lam Lam (cubeSet Q) a → IsHomogenizationComparisonPairOn (cubeSet Q) a (scalarMatrix sigma0) gradU gradV → solutionComparisonNegativeBesovLhs Q s a (scalarMatrix sigma0) gradU gradV ≤ C * s⁻¹ * localizedFluxDefectNegativeBesovAverageTwo Q s (fluxDefect a (scalarMatrix sigma0) gradU) j

Existence of the scalar direct duality constant gives the corrected scalar-background Section 3.3.A duality surface.

theorem HCPolySupport.solution_diff_l2_le_dualityConstant_mul_localizedFluxDefect_of_fluxDefect_negativeBesov_le {d : ℕ} {Cdual : ℝ} (hdual : ScalarSolutionComparisonDualityEstimate d Cdual) (Q : TriadicCube d) (a : CoeffField d) (sigma0 : ℝ) (gradU gradV : Vec d → Vec d) {s : ℝ} (j : ℕ) {lam Lam : ℝ} (hsigma0 : 0 < sigma0) (hs_pos : 0 < s) (hs_lt_one : s < 1) (_hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hcomparison : IsHomogenizationComparisonPairOn (cubeSet Q) a (scalarMatrix sigma0) gradU gradV) : solutionComparisonNegativeBesovLhs Q s a (scalarMatrix sigma0) gradU gradV ≤ Cdual * s⁻¹ * localizedFluxDefectNegativeBesovAverageTwo Q s (fluxDefect a (scalarMatrix sigma0) gradU) j

Scalar-background duality apex for coarsegraining/chapters/ch3_deterministic_theory.tex, lines 2804--3008.

The corrected route exposes the remaining analytic input directly: hdual is the scalar solution-comparison duality estimate. No arbitrary-matrix dimension-only theorem data is assumed here.

theorem HCPolySupport.solution_diff_l2_le_dualityConstant_mul_fluxDefectBound_of_localizedFluxDefect_le {d : ℕ} {Cdual : ℝ} (hdual : ScalarSolutionComparisonDualityEstimate d Cdual) (Q : TriadicCube d) (a : CoeffField d) (sigma0 : ℝ) (gradU gradV : Vec d → Vec d) {s fluxDefectBound : ℝ} (j : ℕ) {lam Lam : ℝ} (hsigma0 : 0 < sigma0) (hs_pos : 0 < s) (hs_lt_one : s < 1) (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hcomparison : IsHomogenizationComparisonPairOn (cubeSet Q) a (scalarMatrix sigma0) gradU gradV) (hfluxDefectBound : localizedFluxDefectNegativeBesovAverageTwo Q s (fluxDefect a (scalarMatrix sigma0) gradU) j ≤ fluxDefectBound) : solutionComparisonNegativeBesovLhs Q s a (scalarMatrix sigma0) gradU gradV ≤ Cdual * s⁻¹ * fluxDefectBound

Scalar-background duality bound with an arbitrary caller-supplied upper bound on the localized flux defect.

theorem HCPolySupport.solution_diff_l2_le_dualityConstant_mul_cubeBesovNegativeFluxDefectBound_of_depth_zero_of_nonneg {d : ℕ} {Cdual : ℝ} (hdual : ScalarSolutionComparisonDualityEstimate d Cdual) (Q : TriadicCube d) (a : CoeffField d) (sigma0 : ℝ) (gradU gradV : Vec d → Vec d) {s fluxDefectBound lam Lam : ℝ} (hsigma0 : 0 < sigma0) (hs_pos : 0 < s) (hs_lt_one : s < 1) (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hcomparison : IsHomogenizationComparisonPairOn (cubeSet Q) a (scalarMatrix sigma0) gradU gradV) (hdefect_nonneg : 0 ≤ cubeBesovNegativeVectorSeminormTwo Q s (fluxDefect a (scalarMatrix sigma0) gradU)) (hfluxDefectBound : cubeBesovNegativeVectorSeminormTwo Q s (fluxDefect a (scalarMatrix sigma0) gradU) ≤ fluxDefectBound) : solutionComparisonNegativeBesovLhs Q s a (scalarMatrix sigma0) gradU gradV ≤ Cdual * s⁻¹ * fluxDefectBound

Scalar-background depth-zero duality bound from a direct one-cube negative Besov bound on the flux defect, with nonnegativity supplied separately.

theorem HCPolySupport.solution_diff_l2_le_dualityConstant_mul_localizedFluxDefect_of_sameRhs {d : ℕ} {Cdual : ℝ} (hdual : ScalarSolutionComparisonDualityEstimate d Cdual) (Q : TriadicCube d) (a : CoeffField d) (sigma0 : ℝ) (u v : H1Function (cubeSet Q)) (g : Vec d → Vec d) {s : ℝ} (j : ℕ) {lam Lam : ℝ} (hsigma0 : 0 < sigma0) (hs_pos : 0 < s) (hs_lt_one : s < 1) (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hu : IsH1DirichletRhsWeakSolutionOn a (cubeSet Q) u g) (hv : IsH1DirichletRhsWeakSolutionOn (constantCoeffField (scalarMatrix sigma0)) (cubeSet Q) v g) (hzeroTrace : IsPotentialZeroTraceOn (cubeSet Q) fun (x : Vec d) => u.grad x - v.grad x) : solutionComparisonNegativeBesovLhs Q s a (scalarMatrix sigma0) u.grad v.grad ≤ Cdual * s⁻¹ * localizedFluxDefectNegativeBesovAverageTwo Q s (fluxDefect a (scalarMatrix sigma0) u.grad) j

Scalar-background duality apex with the Section 3.3.B PDE hypotheses exposed directly.

theorem HCPolySupport.solution_diff_l2_le_dualityConstant_mul_fluxDefectBound_of_sameRhs_of_localizedFluxDefect_le {d : ℕ} {Cdual : ℝ} (hdual : ScalarSolutionComparisonDualityEstimate d Cdual) (Q : TriadicCube d) (a : CoeffField d) (sigma0 : ℝ) (u v : H1Function (cubeSet Q)) (g : Vec d → Vec d) {s fluxDefectBound : ℝ} (j : ℕ) {lam Lam : ℝ} (hsigma0 : 0 < sigma0) (hs_pos : 0 < s) (hs_lt_one : s < 1) (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hu : IsH1DirichletRhsWeakSolutionOn a (cubeSet Q) u g) (hv : IsH1DirichletRhsWeakSolutionOn (constantCoeffField (scalarMatrix sigma0)) (cubeSet Q) v g) (hzeroTrace : IsPotentialZeroTraceOn (cubeSet Q) fun (x : Vec d) => u.grad x - v.grad x) (hfluxDefectBound : localizedFluxDefectNegativeBesovAverageTwo Q s (fluxDefect a (scalarMatrix sigma0) u.grad) j ≤ fluxDefectBound) : solutionComparisonNegativeBesovLhs Q s a (scalarMatrix sigma0) u.grad v.grad ≤ Cdual * s⁻¹ * fluxDefectBound

Scalar-background same-right-hand-side duality bound with a supplied localized flux-defect upper bound.

theorem HCPolySupport.solution_diff_l2_le_dualityConstant_mul_cubeBesovNegativeFluxDefectBound {d : ℕ} {Cdual : ℝ} (hdual : ScalarSolutionComparisonDualityEstimate d Cdual) (Q : TriadicCube d) (a : CoeffField d) (sigma0 : ℝ) (u v : H1Function (cubeSet Q)) (g : Vec d → Vec d) {s fluxDefectBound lam Lam : ℝ} (hsigma0 : 0 < sigma0) (hs_pos : 0 < s) (hs_lt_one : s < 1) (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hu : IsH1DirichletRhsWeakSolutionOn a (cubeSet Q) u g) (hv : IsH1DirichletRhsWeakSolutionOn (constantCoeffField (scalarMatrix sigma0)) (cubeSet Q) v g) (hzeroTrace : IsPotentialZeroTraceOn (cubeSet Q) fun (x : Vec d) => u.grad x - v.grad x) (hdefect_nonneg : 0 ≤ cubeBesovNegativeVectorSeminormTwo Q s (fluxDefect a (scalarMatrix sigma0) u.grad)) (hfluxDefectBound : cubeBesovNegativeVectorSeminormTwo Q s (fluxDefect a (scalarMatrix sigma0) u.grad) ≤ fluxDefectBound) : solutionComparisonNegativeBesovLhs Q s a (scalarMatrix sigma0) u.grad v.grad ≤ Cdual * s⁻¹ * fluxDefectBound

Scalar-background same-right-hand-side depth-zero duality bound from a direct one-cube negative Besov bound on the flux defect.