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

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

Deterministic homogenization black boxes: general coarse graining in L²

This file contains the Section 3.3.B theorem surface from coarsegraining/chapters/ch3_deterministic_theory.tex, lines 3009--3253.

The theorem is stated as the deterministic composition step: once the local coarse flux-defect estimate from the preceding Chapter-3 files supplies the single hypothesis hcoarseFluxDefect, the duality lemma from Section 3.3.A turns it into the global comparison estimate. The right-hand side below is the manuscript expression in the existing Lean notation:

• coarseGrainingHomogenizationErrorAtDepth Q a a0 s j is 𝓔_{s,∞,1}(Q,n;a,a₀) with depth j = m - n;
• lambdaSq and LambdaSq are the scale-local multiscale ellipticity quantities, not the qualitative uniform ellipticity constants;
• cubeBesovPositiveVectorSeminormTwo is the note-normalized 3^{sm}[g]_{\underline B^s_{2,2}(Q)}.

noncomputable def HCPolySupport.coarseGrainingHomogenizationErrorAtDepth {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (s : ℝ) (j : ℕ) : ℝ

The truncated homogenization-error quantity 𝓔_{s,∞,1}(Q,n;a,a₀) from Proposition p.general.coarse.graining.p2.deterministic.theory.

In Lean, the parent cube is Q and the scale gap m - n is the descendant depth j, so the truncation is the supremum over descendants of Q at depth j.

Equations

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

@[simp]

theorem HCPolySupport.coarseGrainingHomogenizationErrorAtDepth_zero {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (s : ℝ) : coarseGrainingHomogenizationErrorAtDepth Q a a0 s 0 = HomogenizationErrorOnCube Q s MultiscaleExponent.infinity (MultiscaleExponent.finite 1) a a0

At depth zero the truncated homogenization error is the one-cube error.

theorem HCPolySupport.homogenizationErrorOnCube_infinity_one_nonneg {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) {s : ℝ} (hs : 0 ≤ s) : 0 ≤ HomogenizationErrorOnCube Q s MultiscaleExponent.infinity (MultiscaleExponent.finite 1) a a0

The q=1 homogenization error on one cube is nonnegative.

theorem HCPolySupport.homogenizationErrorOnCube_le_coarseGrainingHomogenizationErrorAtDepth {d : ℕ} {Q R : TriadicCube d} {a : CoeffField d} {a0 : Mat d} {s : ℝ} {j : ℕ} (hR : R ∈ descendantsAtDepth Q j) : HomogenizationErrorOnCube R s MultiscaleExponent.infinity (MultiscaleExponent.finite 1) a a0 ≤ coarseGrainingHomogenizationErrorAtDepth Q a a0 s j

Each descendant error is bounded by the depth-truncated parent error.

theorem HCPolySupport.coarseGrainingHomogenizationErrorAtDepth_nonneg {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) {s : ℝ} (j : ℕ) (hs : 0 ≤ s) : 0 ≤ coarseGrainingHomogenizationErrorAtDepth Q a a0 s j

The depth-truncated parent homogenization error is nonnegative.

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

The explicit right-hand side inside the dimension-only constant in the general coarse-graining estimate, manuscript lines 3026--3057.

This is intentionally separated from the final theorem so downstream callers can produce a bound on the local flux defect once and then compose it through solution_diff_l2_le_coarseGrainingL2Rhs_of_coarseFluxDefect_le.

Equations

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

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

The first, energy-only term in coarseGrainingL2FluxDefectBound.

Equations

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

noncomputable def HCPolySupport.coarseGrainingL2FluxDefectForcingTerm {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (s : ℝ) (j : ℕ) (g : Vec d → Vec d) : ℝ

The positive-Besov forcing tail in coarseGrainingL2FluxDefectBound.

Equations

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

noncomputable def HCPolySupport.coarseGrainingL2FluxDefectForcingTermTwoExponent {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (s t : ℝ) (j : ℕ) (g : Vec d → Vec d) : ℝ

Scale-separated positive-Besov forcing tail in the repaired Section 3.3.B RHS. The flux-response exponent is s, while the force is measured at the stronger positive exponent t.

Equations

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

noncomputable def HCPolySupport.coarseGrainingL2FluxDefectBoundTwoExponent {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (s t : ℝ) (j : ℕ) (gradU g : Vec d → Vec d) : ℝ

Repaired scale-separated local flux-defect RHS in Section 3.3.B.

Equations

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

theorem HCPolySupport.coarseGrainingL2FluxDefectBound_eq_energyTerm_add_forcingTerm {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (s : ℝ) (j : ℕ) (gradU g : Vec d → Vec d) : coarseGrainingL2FluxDefectBound Q a a0 s j gradU g = coarseGrainingL2FluxDefectEnergyTerm Q a a0 s j gradU + coarseGrainingL2FluxDefectForcingTerm Q a a0 s j g

theorem HCPolySupport.coarseGrainingL2FluxDefectBoundTwoExponent_eq_energyTerm_add_forcingTerm {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (s t : ℝ) (j : ℕ) (gradU g : Vec d → Vec d) : coarseGrainingL2FluxDefectBoundTwoExponent Q a a0 s t j gradU g = coarseGrainingL2FluxDefectEnergyTerm Q a a0 s j gradU + coarseGrainingL2FluxDefectForcingTermTwoExponent Q a a0 s t j g

theorem HCPolySupport.coarseGrainingL2FluxDefectEnergyTerm_le_coarseGrainingL2FluxDefectBound_of_forcingTerm_nonneg {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (s : ℝ) (j : ℕ) (gradU g : Vec d → Vec d) (hforcing_nonneg : 0 ≤ coarseGrainingL2FluxDefectForcingTerm Q a a0 s j g) : coarseGrainingL2FluxDefectEnergyTerm Q a a0 s j gradU ≤ coarseGrainingL2FluxDefectBound Q a a0 s j gradU g

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

The positive-Besov forcing tail in the Section 3.3.B RHS is nonnegative.

@[simp]

theorem HCPolySupport.coarseGrainingL2FluxDefectBound_depth_zero_zero_forcing {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (s : ℝ) (gradU : Vec d → Vec d) : coarseGrainingL2FluxDefectBound Q a a0 s 0 gradU 0 = s⁻¹ * √(matNorm a0) * HomogenizationErrorOnCube Q s MultiscaleExponent.infinity (MultiscaleExponent.finite 1) a a0 * √(cubeAverage Q (coefficientEnergyDensity a gradU))

With depth zero and zero forcing, the general Section 3.3.B flux-defect RHS collapses to the homogeneous RHS term from manuscript lines 3264--3292.

noncomputable def HCPolySupport.localizedCoarseFluxResponseAverageBound {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (s : ℝ) (j : ℕ) (energy : Vec d → ℝ) : ℝ

Localized q = 2 response-average bound produced by applying the q = 1 coarse-flux response estimate on each descendant cube.

This is the scalar quantity that still has to be localized into the manuscript coarseGrainingL2FluxDefectBound when assembling the fully internal Section 3.3.B wrapper.

Equations

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

theorem HCPolySupport.localizedCoarseFluxResponseAverageBound_le_const_mul_sqrt_of_descendantsAverage_energy_bound {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (s : ℝ) (j : ℕ) (energy : Vec d → ℝ) {C A : ℝ} (hC_nonneg : 0 ≤ C) (hpoint : ∀ R ∈ descendantsAtDepth Q j, ((geometricDiscount s 1)⁻¹ * HomogenizationErrorOnCube R s MultiscaleExponent.infinity (MultiscaleExponent.finite 1) a a0 * (√(4 * matNorm a0) * √(cubeAverage R energy))) ^ 2 ≤ C ^ 2 * cubeAverage R energy) (havg : (descendantsAverage Q j fun (R : TriadicCube d) => cubeAverage R energy) ≤ A) : localizedCoarseFluxResponseAverageBound Q a a0 s j energy ≤ C * √A

If the localized response square is pointwise bounded by a constant multiple of the local energy average, then the descendant L² response average is bounded by that constant times the square root of the averaged energy.

theorem HCPolySupport.localizedCoarseFluxResponseAverageBound_le_const_mul_sqrt_cubeAverage_of_pointwise_sq_bound {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (s : ℝ) (j : ℕ) (energy : Vec d → ℝ) {C : ℝ} (hC_nonneg : 0 ≤ C) (henergy_int : MeasureTheory.IntegrableOn energy (cubeSet Q) MeasureTheory.volume) (hpoint : ∀ R ∈ descendantsAtDepth Q j, ((geometricDiscount s 1)⁻¹ * HomogenizationErrorOnCube R s MultiscaleExponent.infinity (MultiscaleExponent.finite 1) a a0 * (√(4 * matNorm a0) * √(cubeAverage R energy))) ^ 2 ≤ C ^ 2 * cubeAverage R energy) : localizedCoarseFluxResponseAverageBound Q a a0 s j energy ≤ C * √(cubeAverage Q energy)

Parent-cube energy localization form of localizedCoarseFluxResponseAverageBound_le_const_mul_sqrt_of_descendantsAverage_energy_bound.

theorem HCPolySupport.CoarseFluxAverageBound_le_geometricError_mul_twoMatrixNorm_sqrtCubeAverage {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) {s : ℝ} (j : ℕ) (energy : Vec d → ℝ) (hs : 0 < s) (henergy_int : MeasureTheory.IntegrableOn energy (cubeSet Q) MeasureTheory.volume) (henergy_avg_nonneg : ∀ R ∈ descendantsAtDepth Q j, 0 ≤ cubeAverage R energy) (herror_nonneg : ∀ R ∈ descendantsAtDepth Q j, 0 ≤ HomogenizationErrorOnCube R s MultiscaleExponent.infinity (MultiscaleExponent.finite 1) a a0) : localizedCoarseFluxResponseAverageBound Q a a0 s j energy ≤ (geometricDiscount s 1)⁻¹ * coarseGrainingHomogenizationErrorAtDepth Q a a0 s j * √(4 * matNorm a0) * √(cubeAverage Q energy)

The localized response average is bounded by the parent depth-truncated homogenization error with the raw q=1 geometric prefactor.

theorem HCPolySupport.localizedCoarseFluxResponseAverageBound_le_ten_mul_energyTerm_of_invGeom_le {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) {s : ℝ} (j : ℕ) (energy : Vec d → ℝ) (hs : 0 < s) (hgeom_le : (geometricDiscount s 1)⁻¹ ≤ 5 * s⁻¹) (henergy_int : MeasureTheory.IntegrableOn energy (cubeSet Q) MeasureTheory.volume) (henergy_avg_nonneg : ∀ R ∈ descendantsAtDepth Q j, 0 ≤ cubeAverage R energy) (herror_nonneg : ∀ R ∈ descendantsAtDepth Q j, 0 ≤ HomogenizationErrorOnCube R s MultiscaleExponent.infinity (MultiscaleExponent.finite 1) a a0) : localizedCoarseFluxResponseAverageBound Q a a0 s j energy ≤ 10 * (s⁻¹ * √(matNorm a0) * coarseGrainingHomogenizationErrorAtDepth Q a a0 s j * √(cubeAverage Q energy))

Constant-adequacy form of the localized response average: once the scalar geometric reciprocal has been bounded by 5 * s⁻¹, the raw q=1 response prefactor is controlled by ten times the manuscript energy term.

theorem HCPolySupport.CoarseFluxAverageBound_coefficientEnergy_le_ten_mul_coarseGrainingFluxBound {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) {s : ℝ} (j : ℕ) (gradU g : Vec d → Vec d) (hs : 0 < s) (hgeom_le : (geometricDiscount s 1)⁻¹ ≤ 5 * s⁻¹) (henergy_int : MeasureTheory.IntegrableOn (coefficientEnergyDensity a gradU) (cubeSet Q) MeasureTheory.volume) (henergy_avg_nonneg : ∀ R ∈ descendantsAtDepth Q j, 0 ≤ cubeAverage R (coefficientEnergyDensity a gradU)) (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) : localizedCoarseFluxResponseAverageBound Q a a0 s j (coefficientEnergyDensity a gradU) ≤ 10 * coarseGrainingL2FluxDefectBound Q a a0 s j gradU g

For the coefficient-energy density, the ten-factor response control is absorbed by ten times the full Section 3.3.B flux-defect RHS whenever the forcing tail is nonnegative.

theorem HCPolySupport.negativeBesovFluxAverage_le_sqrt_descendantMean_sq_of_coarseFluxResponse {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (s : ℝ) (defect : Vec d → Vec d) (energy : Vec d → ℝ) (j : ℕ) (hs : 0 < s) (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 defect energy) (hpartialBdd : ∀ R ∈ descendantsAtDepth Q j, BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminorm R s N defect)) (hsum : ∀ R ∈ descendantsAtDepth Q j, Summable fun (n : ℕ) => geometricWeight s 1 n * scaleResponseAtScale R (R.scale - ↑n) MultiscaleExponent.infinity a a0) : localizedFluxDefectNegativeBesovAverageTwo Q s defect j ≤ √(descendantsAverage Q j fun (R : TriadicCube d) => ((geometricDiscount s 1)⁻¹ * HomogenizationErrorOnCube R s MultiscaleExponent.infinity (MultiscaleExponent.finite 1) a a0 * (√(4 * matNorm a0) * √(cubeAverage R energy))) ^ 2)

Localized q = 2 flux-defect bound obtained by applying the q = 1 coarse-flux response theorem on every descendant cube and then averaging the result.

This is the bridge between the Section 3.2 flux-response estimates and the single localized flux-defect hypothesis consumed by the Section 3.3.B coarse-graining apex.

theorem HCPolySupport.negativeBesovFluxAverage_le_sqrt_descendantMean_sq {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (s : ℝ) (defect : Vec d → Vec d) (energy : Vec d → ℝ) (j : ℕ) {lam0 Lam0 : ℝ} (hs : 0 < s) (ha0 : IsEllipticMatrix lam0 Lam0 a0) (ha0symm : Matrix.IsSymm a0) (hdesc : ∀ R ∈ descendantsAtDepth Q j, DescendantScalarCanonicalFluxDefectData R a a0 defect energy) (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) (hpartialBdd : ∀ R ∈ descendantsAtDepth Q j, BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminorm R s N defect)) (hsum : ∀ R ∈ descendantsAtDepth Q j, Summable fun (n : ℕ) => geometricWeight s 1 n * scaleResponseAtScale R (R.scale - ↑n) MultiscaleExponent.infinity a a0) : localizedFluxDefectNegativeBesovAverageTwo Q s defect j ≤ √(descendantsAverage Q j fun (R : TriadicCube d) => ((geometricDiscount s 1)⁻¹ * HomogenizationErrorOnCube R s MultiscaleExponent.infinity (MultiscaleExponent.finite 1) a a0 * (√(4 * matNorm a0) * √(cubeAverage R energy))) ^ 2)

Localized flux-defect bridge with the existing descendant canonical response data package exposed directly.

theorem HCPolySupport.negativeBesovFluxAverage_le_coarseFluxAverageBound_of_coarseFluxResponse {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (s : ℝ) (defect : Vec d → Vec d) (energy : Vec d → ℝ) (j : ℕ) (hs : 0 < s) (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 defect energy) (hpartialBdd : ∀ R ∈ descendantsAtDepth Q j, BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminorm R s N defect)) (hsum : ∀ R ∈ descendantsAtDepth Q j, Summable fun (n : ℕ) => geometricWeight s 1 n * scaleResponseAtScale R (R.scale - ↑n) MultiscaleExponent.infinity a a0) : localizedFluxDefectNegativeBesovAverageTwo Q s defect j ≤ localizedCoarseFluxResponseAverageBound Q a a0 s j energy

Named response-average version of negativeBesovFluxAverage_le_sqrt_descendantMean_sq_of_coarseFluxResponse.

theorem HCPolySupport.negativeBesovFluxAverage_le_coarseFluxAverageBound {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (s : ℝ) (defect : Vec d → Vec d) (energy : Vec d → ℝ) (j : ℕ) {lam0 Lam0 : ℝ} (hs : 0 < s) (ha0 : IsEllipticMatrix lam0 Lam0 a0) (ha0symm : Matrix.IsSymm a0) (hdesc : ∀ R ∈ descendantsAtDepth Q j, DescendantScalarCanonicalFluxDefectData R a a0 defect energy) (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) (hpartialBdd : ∀ R ∈ descendantsAtDepth Q j, BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminorm R s N defect)) (hsum : ∀ R ∈ descendantsAtDepth Q j, Summable fun (n : ℕ) => geometricWeight s 1 n * scaleResponseAtScale R (R.scale - ↑n) MultiscaleExponent.infinity a a0) : localizedFluxDefectNegativeBesovAverageTwo Q s defect j ≤ localizedCoarseFluxResponseAverageBound Q a a0 s j energy

Named response-average version with descendant scalar-canonical data.

noncomputable def HCPolySupport.coarseGrainingL2Rhs {d : ℕ} (Cdual : ℝ) (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (s : ℝ) (j : ℕ) (gradU g : Vec d → Vec d) : ℝ

The full Section 3.3.B right-hand side after applying the duality constant.

Equations

• HCPolySupport.coarseGrainingL2Rhs Cdual Q a a0 s j gradU g = Cdual * s⁻¹ * HCPolySupport.coarseGrainingL2FluxDefectBound Q a a0 s j gradU g

@[simp]

theorem HCPolySupport.coarseGrainingL2Rhs_depth_zero_zero_forcing {d : ℕ} (Cdual : ℝ) (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (s : ℝ) (gradU : Vec d → Vec d) : coarseGrainingL2Rhs Cdual Q a a0 s 0 gradU 0 = Cdual * s⁻¹ * (s⁻¹ * √(matNorm a0) * HomogenizationErrorOnCube Q s MultiscaleExponent.infinity (MultiscaleExponent.finite 1) a a0 * √(cubeAverage Q (coefficientEnergyDensity a gradU)))

With depth zero and zero forcing, the full Section 3.3.B RHS collapses to the homogeneous RHS after multiplication by the duality constant.

theorem HCPolySupport.solution_diff_l2_le_coarseGrainingL2Rhs_of_coarseFluxDefect_le {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 : ℝ} (hsigma0 : 0 < sigma0) (ha0eq : a0 = scalarMatrix sigma0) (hs_pos : 0 < s) (hs_lt_one : s < 1) (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hcomparison : IsHomogenizationComparisonPairOn (cubeSet Q) a a0 gradU gradV) (hcoarseFluxDefect : localizedFluxDefectNegativeBesovAverageTwo Q s (fluxDefect a a0 gradU) j ≤ coarseGrainingL2FluxDefectBound Q a a0 s j gradU g) : solutionComparisonNegativeBesovLhs Q s a a0 gradU gradV ≤ coarseGrainingL2Rhs Cdual Q a a0 s j gradU g

Note-facing general coarse-graining apex for coarsegraining/chapters/ch3_deterministic_theory.tex, lines 3009--3253.

This is Proposition p.general.coarse.graining.p2.deterministic.theory in the project's modular form. The displayed PDE equations for u and v are represented by the equivalent weak comparison predicate IsHomogenizationComparisonPairOn; the local Section-3.2.3 operator estimate is represented by the single hypothesis hcoarseFluxDefect. No quantitative uniform ellipticity constants appear in the conclusion.

theorem HCPolySupport.solution_diff_l2_le_coarseGrainingL2Rhs_mul_const_of_coarseFluxDefect_le {d : ℕ} {Cdual K : ℝ} (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 : ℝ} (hsigma0 : 0 < sigma0) (ha0eq : a0 = scalarMatrix sigma0) (hs_pos : 0 < s) (hs_lt_one : s < 1) (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hcomparison : IsHomogenizationComparisonPairOn (cubeSet Q) a a0 gradU gradV) (hcoarseFluxDefect : localizedFluxDefectNegativeBesovAverageTwo Q s (fluxDefect a a0 gradU) j ≤ K * coarseGrainingL2FluxDefectBound Q a a0 s j gradU g) : solutionComparisonNegativeBesovLhs Q s a a0 gradU gradV ≤ coarseGrainingL2Rhs (Cdual * K) Q a a0 s j gradU g

Constant-envelope version of solution_diff_l2_le_coarseGrainingL2Rhs_of_coarseFluxDefect_le.

This is the form needed when the local flux-defect theorem supplies a dimension-only multiple of the displayed Section 3.3.B flux-defect RHS.

theorem HCPolySupport.solution_diff_l2_le_dualityConstant_mul_coarseGrainingBound_of_coarseFluxDefect_le {d : ℕ} {Cdual : ℝ} (hdual : ScalarSolutionComparisonDualityEstimate d Cdual) (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (sigma0 : ℝ) (gradU gradV g : Vec d → Vec d) {s coarseGrainingBound : ℝ} (j : ℕ) {lam Lam : ℝ} (hsigma0 : 0 < sigma0) (ha0eq : a0 = scalarMatrix sigma0) (hs_pos : 0 < s) (hs_lt_one : s < 1) (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hcomparison : IsHomogenizationComparisonPairOn (cubeSet Q) a a0 gradU gradV) (hcoarseFluxDefect : localizedFluxDefectNegativeBesovAverageTwo Q s (fluxDefect a a0 gradU) j ≤ coarseGrainingL2FluxDefectBound Q a a0 s j gradU g) (hcoarseGrainingBound : coarseGrainingL2FluxDefectBound Q a a0 s j gradU g ≤ coarseGrainingBound) : solutionComparisonNegativeBesovLhs Q s a a0 gradU gradV ≤ Cdual * s⁻¹ * coarseGrainingBound

General coarse-graining comparison with a caller-supplied scalar upper bound for the Section 3.3.B flux-defect RHS.

This is a downstream-friendly reformulation of manuscript lines 3009--3253: once the local coarse flux-defect estimate gives the note RHS and the caller has bounded that RHS by coarseGrainingBound, the comparison estimate is immediate with the same dimension-only duality constant.

theorem HCPolySupport.solution_diff_l2_le_coarseGrainingL2Rhs_of_sameRhs_of_coarseFluxDefect_le {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 : ℝ} (hsigma0 : 0 < sigma0) (ha0eq : a0 = scalarMatrix 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 a0) (cubeSet Q) v g) (hzeroTrace : IsPotentialZeroTraceOn (cubeSet Q) fun (x : Vec d) => u.grad x - v.grad x) (hcoarseFluxDefect : localizedFluxDefectNegativeBesovAverageTwo Q s (fluxDefect a a0 u.grad) j ≤ 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

Note-facing general coarse-graining apex with the manuscript PDE hypotheses exposed directly.

This is Proposition p.general.coarse.graining.p2.deterministic.theory, manuscript lines 3009--3253. The equations -div(a∇u)=div g and -div(a₀∇v)=div g are represented by the H¹ weak solution predicates below, while the boundary condition is the zero-trace potentiality of ∇u - ∇v. The local Section-3.2.3 flux-defect estimate still enters as the single quantitative hypothesis hcoarseFluxDefect.

theorem HCPolySupport.solution_diff_l2_le_coarseGrainingL2Rhs_mul_const_of_sameRhs_of_coarseFluxDefect_le {d : ℕ} {Cdual K : ℝ} (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 : ℝ} (hsigma0 : 0 < sigma0) (ha0eq : a0 = scalarMatrix 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 a0) (cubeSet Q) v g) (hzeroTrace : IsPotentialZeroTraceOn (cubeSet Q) fun (x : Vec d) => u.grad x - v.grad x) (hcoarseFluxDefect : localizedFluxDefectNegativeBesovAverageTwo Q s (fluxDefect a a0 u.grad) j ≤ K * coarseGrainingL2FluxDefectBound Q a a0 s j u.grad g) : solutionComparisonNegativeBesovLhs Q s a a0 u.grad v.grad ≤ coarseGrainingL2Rhs (Cdual * K) Q a a0 s j u.grad g

Same-right-hand-side version with a caller-supplied nonnegative constant in the local flux-defect bound.

theorem HCPolySupport.solution_diff_l2_le_dualityConstant_mul_coarseGrainingBound_of_sameRhs_of_coarseFluxDefect_le {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 coarseGrainingBound : ℝ} (j : ℕ) {lam Lam : ℝ} (hsigma0 : 0 < sigma0) (ha0eq : a0 = scalarMatrix 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 a0) (cubeSet Q) v g) (hzeroTrace : IsPotentialZeroTraceOn (cubeSet Q) fun (x : Vec d) => u.grad x - v.grad x) (hcoarseFluxDefect : localizedFluxDefectNegativeBesovAverageTwo Q s (fluxDefect a a0 u.grad) j ≤ coarseGrainingL2FluxDefectBound Q a a0 s j u.grad g) (hcoarseGrainingBound : coarseGrainingL2FluxDefectBound Q a a0 s j u.grad g ≤ coarseGrainingBound) : solutionComparisonNegativeBesovLhs Q s a a0 u.grad v.grad ≤ Cdual * s⁻¹ * coarseGrainingBound

Same-right-hand-side general coarse-graining comparison with a caller-supplied scalar upper bound for the Section 3.3.B flux-defect RHS.