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

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

theorem HCPolySupport.coarseFluxResponseRHSBound_eq_coarseGrainingL2FluxDefectBound_zero {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (s : ℝ) (gradU g : Vec d → Vec d) : coarseFluxResponseRHSBound Q a a0 s gradU g = coarseGrainingL2FluxDefectBound Q a a0 s 0 gradU g

At depth zero, the one-cube §3.2.4 RHS flux-response bound is exactly the flux-defect bound used by the Section 3.3.B coarse-graining wrapper.

theorem HCPolySupport.localizedCoarseFluxResponseRHSBound_eq_coarseGrainingL2FluxDefectBound_zero_of_nonneg {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (s : ℝ) (gradU g : Vec d → Vec d) (hbound_nonneg : 0 ≤ coarseFluxResponseRHSBound Q a a0 s gradU g) : localizedCoarseFluxResponseRHSBound Q a a0 s 0 gradU g = coarseGrainingL2FluxDefectBound Q a a0 s 0 gradU g

Depth-zero scalar comparison for the localized §3.2.4 RHS average. The nonnegativity hypothesis is exactly the sqrt (B^2) = B side condition.

theorem HCPolySupport.localizedCoarseFluxResponseRHSBound_eq_coarseGrainingL2FluxDefectBound_zero_of_bddAbove {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) {s : ℝ} (gradU g : Vec d → Vec d) (hs : 0 < s) (hgBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q s N g)) : localizedCoarseFluxResponseRHSBound Q a a0 s 0 gradU g = coarseGrainingL2FluxDefectBound Q a a0 s 0 gradU g

Depth-zero scalar comparison with the standard positive-Besov boundedness input for the forcing term.

theorem HCPolySupport.coarseGrainingL2FluxDefectEnergyTerm_nonneg {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) {s : ℝ} (j : ℕ) (gradU : Vec d → Vec d) (hs : 0 < s) : 0 ≤ coarseGrainingL2FluxDefectEnergyTerm Q a a0 s j gradU

The energy term in the Section 3.3.B flux-defect RHS is nonnegative.

theorem HCPolySupport.coarseGrainingL2FluxDefectBound_nonneg_of_bddAbove {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) {s : ℝ} (j : ℕ) (gradU g : Vec d → Vec d) (hs : 0 < s) (hgBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q s N g)) : 0 ≤ coarseGrainingL2FluxDefectBound Q a a0 s j gradU g

The full Section 3.3.B flux-defect RHS is nonnegative.

theorem HCPolySupport.solution_diff_l2_le_coarseGrainingL2Rhs_of_descendant_coarseFluxResponse {d : ℕ} {Cdual : ℝ} (hdual : ScalarSolutionComparisonDualityEstimate d Cdual) (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (sigma0 : ℝ) (gradU gradV g : Vec d → Vec d) (energy : Vec d → ℝ) {s : ℝ} (j : ℕ) {lam Lam lam0 Lam0 : ℝ} (hs_pos : 0 < s) (hs_lt_one : s < 1) (hsigma0 : 0 < sigma0) (ha0eq : a0 = scalarMatrix sigma0) (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (ha0 : IsEllipticMatrix lam0 Lam0 a0) (ha0symm : Matrix.IsSymm a0) (hcomparison : IsHomogenizationComparisonPairOn (cubeSet Q) a a0 gradU gradV) (henergy_nonneg : ∀ R ∈ descendantsAtDepth Q j, ∀ x ∈ cubeSet R, 0 ≤ energy x) (henergy_int : ∀ R ∈ descendantsAtDepth Q j, MeasureTheory.IntegrableOn energy (cubeSet R) MeasureTheory.volume) (hresp : ∀ R ∈ descendantsAtDepth Q j, CubeAverageFluxResponseControl R a a0 (fluxDefect a a0 gradU) energy) (hpartialBdd : ∀ R ∈ descendantsAtDepth Q j, BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminorm R s N (fluxDefect a a0 gradU))) (hsum : ∀ R ∈ descendantsAtDepth Q j, Summable fun (n : ℕ) => geometricWeight s 1 n * scaleResponseAtScale R (R.scale - ↑n) MultiscaleExponent.infinity a a0) (hresponseBound : localizedCoarseFluxResponseAverageBound Q a a0 s j energy ≤ coarseGrainingL2FluxDefectBound Q a a0 s j gradU g) : solutionComparisonNegativeBesovLhs Q s a a0 gradU gradV ≤ coarseGrainingL2Rhs Cdual Q a a0 s j gradU g

General coarse-graining comparison where the localized flux-defect hypothesis is derived from descendant coarse-flux response data.

The remaining scalar input hresponseBound is the localization/Minkowski step that compares the descendant response average with the manuscript RHS coarseGrainingL2FluxDefectBound.

theorem HCPolySupport.solution_diff_l2_le_coarseGrainingL2Rhs_of_sameRhs_of_descendant_coarseFluxResponse {d : ℕ} {Cdual : ℝ} (hdual : ScalarSolutionComparisonDualityEstimate d Cdual) (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (sigma0 : ℝ) (u v : H1Function (cubeSet Q)) (g : Vec d → Vec d) (energy : Vec d → ℝ) {s : ℝ} (j : ℕ) {lam Lam lam0 Lam0 : ℝ} (hs_pos : 0 < s) (hs_lt_one : s < 1) (hsigma0 : 0 < sigma0) (ha0eq : a0 = scalarMatrix sigma0) (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (ha0 : IsEllipticMatrix lam0 Lam0 a0) (ha0symm : Matrix.IsSymm a0) (hu : IsH1DirichletRhsWeakSolutionOn a (cubeSet Q) u g) (hv : IsH1DirichletRhsWeakSolutionOn (constantCoeffField a0) (cubeSet Q) v g) (hzeroTrace : IsPotentialZeroTraceOn (cubeSet Q) fun (x : Vec d) => u.grad x - v.grad x) (henergy_nonneg : ∀ R ∈ descendantsAtDepth Q j, ∀ x ∈ cubeSet R, 0 ≤ energy x) (henergy_int : ∀ R ∈ descendantsAtDepth Q j, MeasureTheory.IntegrableOn energy (cubeSet R) MeasureTheory.volume) (hresp : ∀ R ∈ descendantsAtDepth Q j, CubeAverageFluxResponseControl R a a0 (fluxDefect a a0 u.grad) energy) (hpartialBdd : ∀ R ∈ descendantsAtDepth Q j, BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminorm R s N (fluxDefect a a0 u.grad))) (hsum : ∀ R ∈ descendantsAtDepth Q j, Summable fun (n : ℕ) => geometricWeight s 1 n * scaleResponseAtScale R (R.scale - ↑n) MultiscaleExponent.infinity a a0) (hresponseBound : localizedCoarseFluxResponseAverageBound Q a a0 s j energy ≤ coarseGrainingL2FluxDefectBound Q a a0 s j u.grad g) : solutionComparisonNegativeBesovLhs Q s a a0 u.grad v.grad ≤ coarseGrainingL2Rhs Cdual Q a a0 s j u.grad g

Same-right-hand-side coarse-graining wrapper with the local flux-defect bound derived from descendant coarse-flux response data instead of supplied as hcoarseFluxDefect.

theorem HCPolySupport.solution_diff_l2_le_coarseGrainingL2Rhs_of_descendant_coarseFluxResponseRHSBound {d : ℕ} {Cdual : ℝ} (hdual : ScalarSolutionComparisonDualityEstimate d Cdual) (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (sigma0 : ℝ) (gradU gradV g : Vec d → Vec d) {s : ℝ} (j : ℕ) {lam Lam lam0 Lam0 : ℝ} (hs_pos : 0 < s) (hs_lt_one : s < 1) (hsigma0 : 0 < sigma0) (ha0eq : a0 = scalarMatrix sigma0) (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (ha0 : IsEllipticMatrix lam0 Lam0 a0) (ha0symm : Matrix.IsSymm a0) (hcomparison : IsHomogenizationComparisonPairOn (cubeSet Q) a a0 gradU gradV) (hdefect_bdd : ∀ R ∈ descendantsAtDepth Q j, BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo R s N (fluxDefect a a0 gradU))) (hRhs : ∀ R ∈ descendantsAtDepth Q j, cubeBesovNegativeVectorSeminormTwo R s (fluxDefect a a0 gradU) ≤ coarseFluxResponseRHSBound R a a0 s gradU g) (hresponseBound : localizedCoarseFluxResponseRHSBound Q a a0 s j gradU g ≤ coarseGrainingL2FluxDefectBound Q a a0 s j gradU g) : solutionComparisonNegativeBesovLhs Q s a a0 gradU gradV ≤ coarseGrainingL2Rhs Cdual Q a a0 s j gradU g

General coarse-graining comparison where the localized flux-defect hypothesis is derived from descendant one-cube §3.2.4 RHS flux-response bounds.

The remaining scalar input hresponseBound is exactly the comparison between the descendant ℓ² average of the §3.2.4 RHS and the manuscript §3.3.B coarseGrainingL2FluxDefectBound.

theorem HCPolySupport.solution_diff_l2_le_coarseGrainingL2Rhs_of_sameRhs_of_descendant_coarseFluxResponseRHSBound {d : ℕ} {Cdual : ℝ} (hdual : ScalarSolutionComparisonDualityEstimate d Cdual) (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (sigma0 : ℝ) (u v : H1Function (cubeSet Q)) (g : Vec d → Vec d) {s : ℝ} (j : ℕ) {lam Lam lam0 Lam0 : ℝ} (hs_pos : 0 < s) (hs_lt_one : s < 1) (hsigma0 : 0 < sigma0) (ha0eq : a0 = scalarMatrix sigma0) (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (ha0 : IsEllipticMatrix lam0 Lam0 a0) (ha0symm : Matrix.IsSymm a0) (hu : IsH1DirichletRhsWeakSolutionOn a (cubeSet Q) u g) (hv : IsH1DirichletRhsWeakSolutionOn (constantCoeffField a0) (cubeSet Q) v g) (hzeroTrace : IsPotentialZeroTraceOn (cubeSet Q) fun (x : Vec d) => u.grad x - v.grad x) (hdefect_bdd : ∀ R ∈ descendantsAtDepth Q j, BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo R s N (fluxDefect a a0 u.grad))) (hRhs : ∀ R ∈ descendantsAtDepth Q j, cubeBesovNegativeVectorSeminormTwo R s (fluxDefect a a0 u.grad) ≤ coarseFluxResponseRHSBound R a a0 s u.grad g) (hresponseBound : localizedCoarseFluxResponseRHSBound Q a a0 s j u.grad g ≤ coarseGrainingL2FluxDefectBound Q a a0 s j u.grad g) : solutionComparisonNegativeBesovLhs Q s a a0 u.grad v.grad ≤ coarseGrainingL2Rhs Cdual Q a a0 s j u.grad g

Same-right-hand-side version of solution_diff_l2_le_coarseGrainingL2Rhs_of_descendant_coarseFluxResponseRHSBound.

theorem HCPolySupport.coarseFluxResponseRHSBound_le_coarseGrainingL2FluxDefectBound_of_component_bounds {d : ℕ} (Q R : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (s : ℝ) (j : ℕ) (gradU g : Vec d → Vec d) (henergy : coarseFluxResponseRHSEnergyBound R a a0 s gradU ≤ coarseGrainingL2FluxDefectEnergyTerm Q a a0 s j gradU) (hforcing : coarseFluxResponseRHSResponseCorrectionBound R a a0 s g + coarseFluxResponseRHSWeakFluxCorrectionBound R a s g + coarseFluxResponseRHSPoincareCorrectionBound R a a0 s g ≤ coarseGrainingL2FluxDefectForcingTerm Q a a0 s j g) : coarseFluxResponseRHSBound R a a0 s gradU g ≤ coarseGrainingL2FluxDefectBound Q a a0 s j gradU g

Pointwise component envelope for the scalar comparison between a one-cube §3.2.4 RHS and the parent §3.3.B flux-defect RHS.

The remaining analytic scalar work is exactly the two hypotheses below: localize the energy component into the parent energy term, and localize the three correction components into the parent forcing term.

theorem HCPolySupport.localizedCoarseFluxResponseRHSBound_le_coarseGrainingL2FluxDefectBound_of_descendant_bound {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (s : ℝ) (j : ℕ) (gradU g : Vec d → Vec d) (hcoarse_nonneg : 0 ≤ coarseGrainingL2FluxDefectBound Q a a0 s j gradU g) (hbound_nonneg : ∀ R ∈ descendantsAtDepth Q j, 0 ≤ coarseFluxResponseRHSBound R a a0 s gradU g) (hpoint : ∀ R ∈ descendantsAtDepth Q j, coarseFluxResponseRHSBound R a a0 s gradU g ≤ coarseGrainingL2FluxDefectBound Q a a0 s j gradU g) : localizedCoarseFluxResponseRHSBound Q a a0 s j gradU g ≤ coarseGrainingL2FluxDefectBound Q a a0 s j gradU g

Scalar §3.3 RHS comparison from a pointwise descendant scalar envelope. This converts the remaining L² descendant-average comparison into the componentwise task of bounding every one-cube §3.2.4 RHS by the parent coarseGrainingL2FluxDefectBound.

theorem HCPolySupport.CoarseFluxRHSBound_le_coarseGrainingFluxBound_of_boundedAbove_of_boundedAbove {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) {s : ℝ} (j : ℕ) (gradU g : Vec d → Vec d) (hs : 0 < s) (hcoarse_nonneg : 0 ≤ coarseGrainingL2FluxDefectBound Q a a0 s j gradU g) (hgBdd : ∀ R ∈ descendantsAtDepth Q j, BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo R s N g)) (hpoint : ∀ R ∈ descendantsAtDepth Q j, coarseFluxResponseRHSBound R a a0 s gradU g ≤ coarseGrainingL2FluxDefectBound Q a a0 s j gradU g) : localizedCoarseFluxResponseRHSBound Q a a0 s j gradU g ≤ coarseGrainingL2FluxDefectBound Q a a0 s j gradU g

Bounded-positive-Besov version of the pointwise descendant scalar-envelope comparison.

theorem HCPolySupport.CoarseFluxRHSBound_le_coarseGrainingFluxBound {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (s : ℝ) (j : ℕ) (gradU g : Vec d → Vec d) (hcoarse_nonneg : 0 ≤ coarseGrainingL2FluxDefectBound Q a a0 s j gradU g) (hbound_nonneg : ∀ R ∈ descendantsAtDepth Q j, 0 ≤ coarseFluxResponseRHSBound R a a0 s gradU g) (henergy : ∀ R ∈ descendantsAtDepth Q j, coarseFluxResponseRHSEnergyBound R a a0 s gradU ≤ coarseGrainingL2FluxDefectEnergyTerm Q a a0 s j gradU) (hforcing : ∀ R ∈ descendantsAtDepth Q j, coarseFluxResponseRHSResponseCorrectionBound R a a0 s g + coarseFluxResponseRHSWeakFluxCorrectionBound R a s g + coarseFluxResponseRHSPoincareCorrectionBound R a a0 s g ≤ coarseGrainingL2FluxDefectForcingTerm Q a a0 s j g) : localizedCoarseFluxResponseRHSBound Q a a0 s j gradU g ≤ coarseGrainingL2FluxDefectBound Q a a0 s j gradU g

Localized scalar §3.3 RHS comparison from descendant component envelopes.

theorem HCPolySupport.CoarseFluxRHSBound_le_coarseGrainingFluxBound_of_componentBounds {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) {s : ℝ} (j : ℕ) (gradU g : Vec d → Vec d) (hs : 0 < s) (hgBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q s N g)) (hgBdd_desc : ∀ R ∈ descendantsAtDepth Q j, BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo R s N g)) (henergy : ∀ R ∈ descendantsAtDepth Q j, coarseFluxResponseRHSEnergyBound R a a0 s gradU ≤ coarseGrainingL2FluxDefectEnergyTerm Q a a0 s j gradU) (hforcing : ∀ R ∈ descendantsAtDepth Q j, coarseFluxResponseRHSResponseCorrectionBound R a a0 s g + coarseFluxResponseRHSWeakFluxCorrectionBound R a s g + coarseFluxResponseRHSPoincareCorrectionBound R a a0 s g ≤ coarseGrainingL2FluxDefectForcingTerm Q a a0 s j g) : localizedCoarseFluxResponseRHSBound Q a a0 s j gradU g ≤ coarseGrainingL2FluxDefectBound Q a a0 s j gradU g

Bounded-positive-Besov version of the descendant component-envelope scalar comparison.

theorem HCPolySupport.solutionDifference_l2_le_coarseGrainingRhs_of_descendantFluxBounds {d : ℕ} {Cdual : ℝ} (hdual : ScalarSolutionComparisonDualityEstimate d Cdual) (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (sigma0 : ℝ) (gradU gradV g : Vec d → Vec d) {s : ℝ} (j : ℕ) {lam Lam lam0 Lam0 : ℝ} (hs_pos : 0 < s) (hs_lt_one : s < 1) (hsigma0 : 0 < sigma0) (ha0eq : a0 = scalarMatrix sigma0) (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (ha0 : IsEllipticMatrix lam0 Lam0 a0) (ha0symm : Matrix.IsSymm a0) (hcomparison : IsHomogenizationComparisonPairOn (cubeSet Q) a a0 gradU gradV) (hdefect_bdd : ∀ R ∈ descendantsAtDepth Q j, BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo R s N (fluxDefect a a0 gradU))) (hRhs : ∀ R ∈ descendantsAtDepth Q j, cubeBesovNegativeVectorSeminormTwo R s (fluxDefect a a0 gradU) ≤ coarseFluxResponseRHSBound R a a0 s gradU g) (hcoarse_nonneg : 0 ≤ coarseGrainingL2FluxDefectBound Q a a0 s j gradU g) (hbound_nonneg : ∀ R ∈ descendantsAtDepth Q j, 0 ≤ coarseFluxResponseRHSBound R a a0 s gradU g) (hpoint : ∀ R ∈ descendantsAtDepth Q j, coarseFluxResponseRHSBound R a a0 s gradU g ≤ coarseGrainingL2FluxDefectBound Q a a0 s j gradU g) : solutionComparisonNegativeBesovLhs Q s a a0 gradU gradV ≤ coarseGrainingL2Rhs Cdual Q a a0 s j gradU g

§3.3 wrapper where the scalar RHS-average comparison is supplied in pointwise descendant-envelope form.

theorem HCPolySupport.solution_diff_l2_le_coarseGrainingL2Rhs_of_descendant_fluxRHSBound_of_component {d : ℕ} {Cdual : ℝ} (hdual : ScalarSolutionComparisonDualityEstimate d Cdual) (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (sigma0 : ℝ) (gradU gradV g : Vec d → Vec d) {s : ℝ} (j : ℕ) {lam Lam lam0 Lam0 : ℝ} (hs_pos : 0 < s) (hs_lt_one : s < 1) (hsigma0 : 0 < sigma0) (ha0eq : a0 = scalarMatrix sigma0) (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (ha0 : IsEllipticMatrix lam0 Lam0 a0) (ha0symm : Matrix.IsSymm a0) (hcomparison : IsHomogenizationComparisonPairOn (cubeSet Q) a a0 gradU gradV) (hdefect_bdd : ∀ R ∈ descendantsAtDepth Q j, BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo R s N (fluxDefect a a0 gradU))) (hRhs : ∀ R ∈ descendantsAtDepth Q j, cubeBesovNegativeVectorSeminormTwo R s (fluxDefect a a0 gradU) ≤ coarseFluxResponseRHSBound R a a0 s gradU g) (hcoarse_nonneg : 0 ≤ coarseGrainingL2FluxDefectBound Q a a0 s j gradU g) (hbound_nonneg : ∀ R ∈ descendantsAtDepth Q j, 0 ≤ coarseFluxResponseRHSBound R a a0 s gradU g) (henergy : ∀ R ∈ descendantsAtDepth Q j, coarseFluxResponseRHSEnergyBound R a a0 s gradU ≤ coarseGrainingL2FluxDefectEnergyTerm Q a a0 s j gradU) (hforcing : ∀ R ∈ descendantsAtDepth Q j, coarseFluxResponseRHSResponseCorrectionBound R a a0 s g + coarseFluxResponseRHSWeakFluxCorrectionBound R a s g + coarseFluxResponseRHSPoincareCorrectionBound R a a0 s g ≤ coarseGrainingL2FluxDefectForcingTerm Q a a0 s j g) : solutionComparisonNegativeBesovLhs Q s a a0 gradU gradV ≤ coarseGrainingL2Rhs Cdual Q a a0 s j gradU g

§3.3 wrapper where the scalar RHS-average comparison is supplied by descendant component envelopes.

theorem HCPolySupport.solution_diff_l2_le_coarseGrainingL2Rhs_of_descendant_fluxRHSBound_of_descendant {d : ℕ} {Cdual : ℝ} (hdual : ScalarSolutionComparisonDualityEstimate d Cdual) (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (sigma0 : ℝ) (gradU gradV g : Vec d → Vec d) {s : ℝ} (j : ℕ) {lam Lam lam0 Lam0 : ℝ} (hs_pos : 0 < s) (hs_lt_one : s < 1) (hsigma0 : 0 < sigma0) (ha0eq : a0 = scalarMatrix sigma0) (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (ha0 : IsEllipticMatrix lam0 Lam0 a0) (ha0symm : Matrix.IsSymm a0) (hcomparison : IsHomogenizationComparisonPairOn (cubeSet Q) a a0 gradU gradV) (hdefect_bdd : ∀ R ∈ descendantsAtDepth Q j, BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo R s N (fluxDefect a a0 gradU))) (hRhs : ∀ R ∈ descendantsAtDepth Q j, cubeBesovNegativeVectorSeminormTwo R s (fluxDefect a a0 gradU) ≤ coarseFluxResponseRHSBound R a a0 s gradU g) (hgBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q s N g)) (hgBdd_desc : ∀ R ∈ descendantsAtDepth Q j, BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo R s N g)) (henergy : ∀ R ∈ descendantsAtDepth Q j, coarseFluxResponseRHSEnergyBound R a a0 s gradU ≤ coarseGrainingL2FluxDefectEnergyTerm Q a a0 s j gradU) (hforcing : ∀ R ∈ descendantsAtDepth Q j, coarseFluxResponseRHSResponseCorrectionBound R a a0 s g + coarseFluxResponseRHSWeakFluxCorrectionBound R a s g + coarseFluxResponseRHSPoincareCorrectionBound R a a0 s g ≤ coarseGrainingL2FluxDefectForcingTerm Q a a0 s j g) : solutionComparisonNegativeBesovLhs Q s a a0 gradU gradV ≤ coarseGrainingL2Rhs Cdual Q a a0 s j gradU g

Bounded-positive-Besov version of the descendant component-envelope §3.3 wrapper.

theorem HCPolySupport.solution_diff_l2_le_coarseGrainingL2Rhs_of_coarseFluxResponseRHSBound_zero {d : ℕ} {Cdual : ℝ} (hdual : ScalarSolutionComparisonDualityEstimate d Cdual) (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (sigma0 : ℝ) (gradU gradV g : Vec d → Vec d) {s lam Lam lam0 Lam0 : ℝ} (hs_pos : 0 < s) (hs_lt_one : s < 1) (hsigma0 : 0 < sigma0) (ha0eq : a0 = scalarMatrix sigma0) (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (ha0 : IsEllipticMatrix lam0 Lam0 a0) (ha0symm : Matrix.IsSymm a0) (hcomparison : IsHomogenizationComparisonPairOn (cubeSet Q) a a0 gradU gradV) (hdefect_bdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N (fluxDefect a a0 gradU))) (hRhs : cubeBesovNegativeVectorSeminormTwo Q s (fluxDefect a a0 gradU) ≤ coarseFluxResponseRHSBound Q a a0 s gradU g) (hgBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q s N g)) : solutionComparisonNegativeBesovLhs Q s a a0 gradU gradV ≤ coarseGrainingL2Rhs Cdual Q a a0 s 0 gradU g

Depth-zero §3.3 wrapper through the one-cube §3.2.4 RHS flux-response bound. At depth zero the scalar descendant-average comparison is closed internally.

theorem HCPolySupport.solution_diff_l2_le_coarseGrainingL2Rhs_of_sameRhs_of_coarseFluxResponseRHSBound_zero {d : ℕ} {Cdual : ℝ} (hdual : ScalarSolutionComparisonDualityEstimate d Cdual) (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (sigma0 : ℝ) (u v : H1Function (cubeSet Q)) (g : Vec d → Vec d) {s lam Lam lam0 Lam0 : ℝ} (hs_pos : 0 < s) (hs_lt_one : s < 1) (hsigma0 : 0 < sigma0) (ha0eq : a0 = scalarMatrix sigma0) (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (ha0 : IsEllipticMatrix lam0 Lam0 a0) (ha0symm : Matrix.IsSymm a0) (hu : IsH1DirichletRhsWeakSolutionOn a (cubeSet Q) u g) (hv : IsH1DirichletRhsWeakSolutionOn (constantCoeffField a0) (cubeSet Q) v g) (hzeroTrace : IsPotentialZeroTraceOn (cubeSet Q) fun (x : Vec d) => u.grad x - v.grad x) (hdefect_bdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N (fluxDefect a a0 u.grad))) (hRhs : cubeBesovNegativeVectorSeminormTwo Q s (fluxDefect a a0 u.grad) ≤ coarseFluxResponseRHSBound Q a a0 s u.grad g) (hgBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q s N g)) : solutionComparisonNegativeBesovLhs Q s a a0 u.grad v.grad ≤ coarseGrainingL2Rhs Cdual Q a a0 s 0 u.grad g

Same-right-hand-side depth-zero wrapper through the one-cube §3.2.4 RHS flux-response bound.

theorem HCPolySupport.solution_diff_l2_le_ten_mul_coarseGrainingL2Rhs_of_descendant_coarseFluxResponse_energy {d : ℕ} {Cdual : ℝ} (hdual : ScalarSolutionComparisonDualityEstimate d Cdual) (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (sigma0 : ℝ) (gradU gradV g : Vec d → Vec d) {s : ℝ} (j : ℕ) {lam Lam lam0 Lam0 : ℝ} (hs_pos : 0 < s) (hs_lt_one : s < 1) (hgeom_le : (geometricDiscount s 1)⁻¹ ≤ 5 * s⁻¹) (hsigma0 : 0 < sigma0) (ha0eq : a0 = scalarMatrix sigma0) (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (ha0 : IsEllipticMatrix lam0 Lam0 a0) (ha0symm : Matrix.IsSymm a0) (hcomparison : IsHomogenizationComparisonPairOn (cubeSet Q) a a0 gradU gradV) (henergy_int : MeasureTheory.IntegrableOn (coefficientEnergyDensity a gradU) (cubeSet Q) MeasureTheory.volume) (hresp : ∀ R ∈ descendantsAtDepth Q j, CubeAverageFluxResponseControl R a a0 (fluxDefect a a0 gradU) (coefficientEnergyDensity a gradU)) (hpartialBdd : ∀ R ∈ descendantsAtDepth Q j, BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminorm R s N (fluxDefect a a0 gradU))) (hsum : ∀ R ∈ descendantsAtDepth Q j, Summable fun (n : ℕ) => geometricWeight s 1 n * scaleResponseAtScale R (R.scale - ↑n) MultiscaleExponent.infinity a a0) (herror_nonneg : ∀ R ∈ descendantsAtDepth Q j, 0 ≤ HomogenizationErrorOnCube R s MultiscaleExponent.infinity (MultiscaleExponent.finite 1) a a0) (hforcing_nonneg : 0 ≤ coarseGrainingL2FluxDefectForcingTerm Q a a0 s j g) : solutionComparisonNegativeBesovLhs Q s a a0 gradU gradV ≤ 10 * coarseGrainingL2Rhs Cdual Q a a0 s j gradU g

General coarse-graining comparison where the localized flux-defect hypothesis is derived from descendant coarse-flux response data and the scalar response average is absorbed into the Section 3.3.B RHS with the explicit ten-factor constant.

The assumptions hgeom_le, herror_nonneg, and hforcing_nonneg are the remaining scalar side conditions needed to keep this wrapper import-light: the note-constant file supplies hgeom_le, while later positivity wrappers can close the two nonnegativity inputs.

theorem HCPolySupport.solutionDifference_l2_le_ten_coarseGrainingRhs_of_energyBounds {d : ℕ} {Cdual : ℝ} (hdual : ScalarSolutionComparisonDualityEstimate d Cdual) (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (sigma0 : ℝ) (gradU gradV g : Vec d → Vec d) {s : ℝ} (j : ℕ) {lam Lam lam0 Lam0 : ℝ} (hs_pos : 0 < s) (hs_lt_one : s < 1) (hsigma0 : 0 < sigma0) (ha0eq : a0 = scalarMatrix sigma0) (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (ha0 : IsEllipticMatrix lam0 Lam0 a0) (ha0symm : Matrix.IsSymm a0) (hcomparison : IsHomogenizationComparisonPairOn (cubeSet Q) a a0 gradU gradV) (henergy_int : MeasureTheory.IntegrableOn (coefficientEnergyDensity a gradU) (cubeSet Q) MeasureTheory.volume) (hresp : ∀ R ∈ descendantsAtDepth Q j, CubeAverageFluxResponseControl R a a0 (fluxDefect a a0 gradU) (coefficientEnergyDensity a gradU)) (hpartialBdd : ∀ R ∈ descendantsAtDepth Q j, BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminorm R s N (fluxDefect a a0 gradU))) (hsum : ∀ R ∈ descendantsAtDepth Q j, Summable fun (n : ℕ) => geometricWeight s 1 n * scaleResponseAtScale R (R.scale - ↑n) MultiscaleExponent.infinity a a0) (hgBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q s N g)) : solutionComparisonNegativeBesovLhs Q s a a0 gradU gradV ≤ 10 * coarseGrainingL2Rhs Cdual Q a a0 s j gradU g

Import-light side conditions in the response-data apex discharged from the standard manuscript range and the global positive-Besov boundedness of g.