Coarse-graining support:

Support.Deterministic.HomogenizationBlackBoxes.CoarseGrainingL2RHSCoefficientLocalization

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

theorem HCPolySupport.coarseFluxResponseRHSResponseCorrectionBound_le_parent_coeff_of_mem_descendantsAtDepth {d : ℕ} {Q R : TriadicCube d} (a : CoeffField d) (a0 : Mat d) {s : ℝ} {j : ℕ} (g : Vec d → Vec d) (hs : 0 < s) (hR : R ∈ descendantsAtDepth Q j) (hgBddR : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo R s N g)) (hsumSigma : Summable fun (n : ℕ) => geometricWeight (s / 2) 2 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (2 / 2)) : coarseFluxResponseRHSResponseCorrectionBound R a a0 s g ≤ s.rpow (-(5 / 2)) * √(matNorm a0) * Real.rpow 3 (s / 2 * ↑j) * √(lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ * coarseGrainingHomogenizationErrorAtDepth Q a a0 s j * cubeBesovPositiveVectorSeminormTwo R s g

Pointwise descendant-to-parent coefficient localization for the §3.2.4 homogeneous response-correction component.

theorem HCPolySupport.coarseFluxResponseRHSWeakFluxCorrectionBound_le_parent_coeff_of_mem_descendantsAtDepth {d : ℕ} {Q R : TriadicCube d} (a : CoeffField d) {s : ℝ} {j : ℕ} (g : Vec d → Vec d) (hs : 0 < s) (hR : R ∈ descendantsAtDepth Q j) (hgBddR : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo R s N g)) (hsumB : Summable fun (n : ℕ) => geometricWeight (s / 2) 2 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (2 / 2)) (hsumSigma : Summable fun (n : ℕ) => geometricWeight (s / 2) 2 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (2 / 2)) : coarseFluxResponseRHSWeakFluxCorrectionBound R a s g ≤ s.rpow (-(5 / 2)) * Real.rpow 3 (s * ↑j) * √(LambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a) * √(lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ * cubeBesovPositiveVectorSeminormTwo R s g

Pointwise descendant-to-parent coefficient localization for the §3.2.4 weak-flux correction component.

theorem HCPolySupport.coarseFluxResponseRHSPoincareCorrectionBound_le_parent_coeff_of_mem_descendantsAtDepth {d : ℕ} {Q R : TriadicCube d} (a : CoeffField d) (a0 : Mat d) {s : ℝ} {j : ℕ} (g : Vec d → Vec d) (hs : 0 < s) (hR : R ∈ descendantsAtDepth Q j) (hgBddR : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo R s N g)) (hsumSigma : Summable fun (n : ℕ) => geometricWeight (s / 2) 2 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (2 / 2)) : coarseFluxResponseRHSPoincareCorrectionBound R a a0 s g ≤ s.rpow (-3) * Real.rpow 3 (s * ↑j) * matNorm a0 * (lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ * cubeBesovPositiveVectorSeminormTwo R s g

Pointwise descendant-to-parent coefficient localization for the §3.2.4 Poincare correction component.

theorem HCPolySupport.coarseFluxResponse_rhsResponseCorrection_le_parentExponent {d : ℕ} {Q R : TriadicCube d} (a : CoeffField d) (a0 : Mat d) {s t : ℝ} {j : ℕ} (g : Vec d → Vec d) (hs : 0 < s) (hst : s ≤ t) (hR : R ∈ descendantsAtDepth Q j) (hgBddR : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo R t N g)) (hsumSigma : Summable fun (n : ℕ) => geometricWeight (s / 2) 2 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (2 / 2)) : coarseFluxResponseRHSResponseCorrectionBound R a a0 s g ≤ s.rpow (-(5 / 2)) * √(matNorm a0) * Real.rpow 3 (s / 2 * ↑j) * √(lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ * coarseGrainingHomogenizationErrorAtDepth Q a a0 s j * cubeBesovPositiveVectorSeminormTwo R t g

Two-exponent descendant-to-parent coefficient localization for the response correction component. The local flux-response exponent is s, while the force is measured at the stronger positive exponent t.

theorem HCPolySupport.coarseFluxResponse_weakFluxCorrection_le_parentExponent {d : ℕ} {Q R : TriadicCube d} (a : CoeffField d) {s t : ℝ} {j : ℕ} (g : Vec d → Vec d) (hs : 0 < s) (hst : s ≤ t) (hR : R ∈ descendantsAtDepth Q j) (hgBddR : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo R t N g)) (hsumB : Summable fun (n : ℕ) => geometricWeight (s / 2) 2 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (2 / 2)) (hsumSigma : Summable fun (n : ℕ) => geometricWeight (s / 2) 2 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (2 / 2)) : coarseFluxResponseRHSWeakFluxCorrectionBound R a s g ≤ s.rpow (-(5 / 2)) * Real.rpow 3 (s * ↑j) * √(LambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a) * √(lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ * cubeBesovPositiveVectorSeminormTwo R t g

Two-exponent descendant-to-parent coefficient localization for the weak-flux correction component.

theorem HCPolySupport.coarseFluxResponse_poincareCorrection_le_parentExponent {d : ℕ} {Q R : TriadicCube d} (a : CoeffField d) (a0 : Mat d) {s t : ℝ} {j : ℕ} (g : Vec d → Vec d) (hs : 0 < s) (hst : s ≤ t) (hR : R ∈ descendantsAtDepth Q j) (hgBddR : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo R t N g)) (hsumSigma : Summable fun (n : ℕ) => geometricWeight (s / 2) 2 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (2 / 2)) : coarseFluxResponseRHSPoincareCorrectionBound R a a0 s g ≤ s.rpow (-3) * Real.rpow 3 (s * ↑j) * matNorm a0 * (lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ * cubeBesovPositiveVectorSeminormTwo R t g

Two-exponent descendant-to-parent coefficient localization for the Poincare correction component.

theorem HCPolySupport.FluxForcingCorrectionBound_le_coarseGrainingL2FluxDefectForcingTerm {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)) (hgBdd_desc : ∀ R ∈ descendantsAtDepth Q j, BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo R s N g)) (hsumB : Summable fun (n : ℕ) => geometricWeight (s / 2) 2 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (2 / 2)) (hsumSigma : Summable fun (n : ℕ) => geometricWeight (s / 2) 2 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (2 / 2)) : localizedCoarseFluxResponseRHSResponseCorrectionBound Q a a0 s j g + localizedCoarseFluxResponseRHSWeakFluxCorrectionBound Q a s j g + localizedCoarseFluxResponseRHSPoincareCorrectionBound Q a a0 s j g ≤ coarseGrainingL2FluxDefectForcingTerm Q a a0 s j g

Localized forcing correction absorbed into the §3.3.B forcing term, with the three pointwise coefficient localizations discharged from descendant multiscale-ellipticity summability.

theorem HCPolySupport.FluxForcingCorrectionBound_le_coeff_mul_depthWeight_inv_forceExponent {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) {s t : ℝ} (j : ℕ) (g : Vec d → Vec d) (hs : 0 < s) (hst : s ≤ t) (hgBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q t N g)) (hgBdd_desc : ∀ R ∈ descendantsAtDepth Q j, BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo R t N g)) (hsumB : Summable fun (n : ℕ) => geometricWeight (s / 2) 2 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (2 / 2)) (hsumSigma : Summable fun (n : ℕ) => geometricWeight (s / 2) 2 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (2 / 2)) : localizedCoarseFluxResponseRHSResponseCorrectionBound Q a a0 s j g + localizedCoarseFluxResponseRHSWeakFluxCorrectionBound Q a s j g + localizedCoarseFluxResponseRHSPoincareCorrectionBound Q a a0 s j g ≤ (s.rpow (-(5 / 2)) * √(matNorm a0) * Real.rpow 3 (s / 2 * ↑j) * √(lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ * coarseGrainingHomogenizationErrorAtDepth Q a a0 s j + s.rpow (-(5 / 2)) * Real.rpow 3 (s * ↑j) * √(LambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a) * √(lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ + s.rpow (-3) * Real.rpow 3 (s * ↑j) * matNorm a0 * (lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a)⁻¹) * ((Real.rpow 3 (t * ↑j))⁻¹ * cubeBesovPositiveVectorSeminormTwo Q t g)

Two-exponent localized forcing correction with parent coefficient localization and the inverse force-depth weight kept visible.

theorem HCPolySupport.CoarseFluxRHSBound_le_coarseGrainingFluxBoundTwoExponent {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) {s t : ℝ} (j : ℕ) (gradU g : Vec d → Vec d) {lam Lam : ℝ} (hs : 0 < s) (hst : s ≤ t) (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (henergy_int : MeasureTheory.IntegrableOn (coefficientEnergyDensity a gradU) (cubeSet Q) MeasureTheory.volume) (hgBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q t N g)) (hgBdd_desc : ∀ R ∈ descendantsAtDepth Q j, BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo R t N g)) (hsumB : Summable fun (n : ℕ) => geometricWeight (s / 2) 2 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (2 / 2)) (hsumSigma : Summable fun (n : ℕ) => geometricWeight (s / 2) 2 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (2 / 2)) : localizedCoarseFluxResponseRHSBound Q a a0 s j gradU g ≤ coarseGrainingL2FluxDefectBoundTwoExponent Q a a0 s t j gradU g

Scalar §3.3 RHS comparison with the localized energy average and the scale-separated two-exponent forcing correction.

theorem HCPolySupport.CoarseFluxRHSBound_le_coarseGrainingFluxBound_of_boundedAbove_of_summable {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) {s : ℝ} (j : ℕ) (gradU g : Vec d → Vec d) {lam Lam : ℝ} (hs : 0 < s) (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (henergy_int : MeasureTheory.IntegrableOn (coefficientEnergyDensity a gradU) (cubeSet Q) MeasureTheory.volume) (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)) (hsumB : Summable fun (n : ℕ) => geometricWeight (s / 2) 2 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (2 / 2)) (hsumSigma : Summable fun (n : ℕ) => geometricWeight (s / 2) 2 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (2 / 2)) : localizedCoarseFluxResponseRHSBound Q a a0 s j gradU g ≤ coarseGrainingL2FluxDefectBound Q a a0 s j gradU g

Scalar §3.3 RHS comparison with the localized energy average and the three forcing-correction coefficient localizations discharged internally.

theorem HCPolySupport.solution_diff_l2_le_coarseGrainingL2Rhs_of_descendant_fluxRHSBound {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) (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)) (hsumB : Summable fun (n : ℕ) => geometricWeight (s / 2) 2 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (2 / 2)) (hsumSigma : Summable fun (n : ℕ) => geometricWeight (s / 2) 2 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (2 / 2)) : solutionComparisonNegativeBesovLhs Q s a a0 gradU gradV ≤ coarseGrainingL2Rhs Cdual Q a a0 s j gradU g

§3.3 wrapper through descendant one-cube §3.2.4 RHS bounds, with the scalar RHS comparison closed from the coefficient-localization hypotheses.

theorem HCPolySupport.solution_diff_l2_le_coarseGrainingL2Rhs_of_sameRhs_descendant_of_fluxRHSBound {d : ℕ} [NeZero 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) (hData : OpenCubeDescendantDeterministicCoarseData 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) (hRhs : ∀ R ∈ descendantsAtDepth Q j, cubeBesovNegativeVectorSeminormTwo R s (fluxDefect a a0 u.grad) ≤ coarseFluxResponseRHSBound R a a0 s u.grad g) (hg : CubeVectorBesovHRegularity Q s g) : solutionComparisonNegativeBesovLhs Q s a a0 u.grad v.grad ≤ coarseGrainingL2Rhs Cdual Q a a0 s j u.grad g

Same-RHS §3.3 wrapper deriving the half-scale coefficient summability inputs from the descendant deterministic coarse-data package.