Coarse-graining support:

Support.Deterministic.HomogenizationBlackBoxes.CoarseGrainingL2RHSComparison

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

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

Localized descendant L² average of the §3.2.4 energy component.

Equations

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

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

Localized descendant L² average of the §3.2.4 response correction.

Equations

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

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

Localized descendant L² average of the §3.2.4 weak-flux correction.

Equations

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

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

Localized descendant L² average of the §3.2.4 Poincare correction.

Equations

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

theorem HCPolySupport.localizedCoarseFluxResponseRHSEnergyBound_le_coarseGrainingL2FluxDefectEnergyTerm {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) {s : ℝ} (j : ℕ) (gradU : Vec d → Vec d) (hs : 0 < 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)) : localizedCoarseFluxResponseRHSEnergyBound Q a a0 s j gradU ≤ coarseGrainingL2FluxDefectEnergyTerm Q a a0 s j gradU

The localized L² average of the §3.2.4 RHS energy component is controlled by the parent-cube energy term in the §3.3.B flux-defect RHS.

theorem HCPolySupport.CoarseFluxRHSEnergyBound_le_coarseGrainingL2FluxDefectEnergyTerm {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) {s : ℝ} (j : ℕ) (gradU : 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) : localizedCoarseFluxResponseRHSEnergyBound Q a a0 s j gradU ≤ coarseGrainingL2FluxDefectEnergyTerm Q a a0 s j gradU

Ellipticity-facing version of localizedCoarseFluxResponseRHSEnergyBound_le_coarseGrainingL2FluxDefectEnergyTerm.

theorem HCPolySupport.localizedCoarseFluxResponseRHSResponseCorrectionBound_le_mul_of_pointwise_le {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) {s : ℝ} (j : ℕ) (g : Vec d → Vec d) {C A : ℝ} (hC_nonneg : 0 ≤ C) (hA_nonneg : 0 ≤ A) (hcomponent_nonneg : ∀ R ∈ descendantsAtDepth Q j, 0 ≤ coarseFluxResponseRHSResponseCorrectionBound R a a0 s g) (hpoint : ∀ R ∈ descendantsAtDepth Q j, coarseFluxResponseRHSResponseCorrectionBound R a a0 s g ≤ C * cubeBesovPositiveVectorSeminormTwo R s g) (havg : (descendantsAverage Q j fun (R : TriadicCube d) => cubeBesovPositiveVectorSeminormTwo R s g ^ 2) ≤ A ^ 2) : localizedCoarseFluxResponseRHSResponseCorrectionBound Q a a0 s j g ≤ C * A

Square-average wrapper for the localized response-correction component. The analytic inputs are a pointwise coefficient bound and the parent-scale localized positive-Besov square estimate.

theorem HCPolySupport.localizedCoarseFluxResponseRHSWeakFluxCorrectionBound_le_mul_of_pointwise_le {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) {s : ℝ} (j : ℕ) (g : Vec d → Vec d) {C A : ℝ} (hC_nonneg : 0 ≤ C) (hA_nonneg : 0 ≤ A) (hcomponent_nonneg : ∀ R ∈ descendantsAtDepth Q j, 0 ≤ coarseFluxResponseRHSWeakFluxCorrectionBound R a s g) (hpoint : ∀ R ∈ descendantsAtDepth Q j, coarseFluxResponseRHSWeakFluxCorrectionBound R a s g ≤ C * cubeBesovPositiveVectorSeminormTwo R s g) (havg : (descendantsAverage Q j fun (R : TriadicCube d) => cubeBesovPositiveVectorSeminormTwo R s g ^ 2) ≤ A ^ 2) : localizedCoarseFluxResponseRHSWeakFluxCorrectionBound Q a s j g ≤ C * A

Square-average wrapper for the localized weak-flux correction component.

theorem HCPolySupport.localizedCoarseFluxResponseRHSPoincareCorrectionBound_le_mul_of_pointwise_le {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) {s : ℝ} (j : ℕ) (g : Vec d → Vec d) {C A : ℝ} (hC_nonneg : 0 ≤ C) (hA_nonneg : 0 ≤ A) (hcomponent_nonneg : ∀ R ∈ descendantsAtDepth Q j, 0 ≤ coarseFluxResponseRHSPoincareCorrectionBound R a a0 s g) (hpoint : ∀ R ∈ descendantsAtDepth Q j, coarseFluxResponseRHSPoincareCorrectionBound R a a0 s g ≤ C * cubeBesovPositiveVectorSeminormTwo R s g) (havg : (descendantsAverage Q j fun (R : TriadicCube d) => cubeBesovPositiveVectorSeminormTwo R s g ^ 2) ≤ A ^ 2) : localizedCoarseFluxResponseRHSPoincareCorrectionBound Q a a0 s j g ≤ C * A

Square-average wrapper for the localized Poincare correction component.

theorem HCPolySupport.FluxForcingCorrectionBound_le_coeffSum_mul_PositiveBesovForcing {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) {s : ℝ} (j : ℕ) (g : Vec d → Vec d) {C₁ C₂ C₃ : ℝ} (hC₁_nonneg : 0 ≤ C₁) (hC₂_nonneg : 0 ≤ C₂) (hC₃_nonneg : 0 ≤ C₃) (hresponse_nonneg : ∀ R ∈ descendantsAtDepth Q j, 0 ≤ coarseFluxResponseRHSResponseCorrectionBound R a a0 s g) (hweak_nonneg : ∀ R ∈ descendantsAtDepth Q j, 0 ≤ coarseFluxResponseRHSWeakFluxCorrectionBound R a s g) (hpoincare_nonneg : ∀ R ∈ descendantsAtDepth Q j, 0 ≤ coarseFluxResponseRHSPoincareCorrectionBound R a a0 s g) (hresponse_point : ∀ R ∈ descendantsAtDepth Q j, coarseFluxResponseRHSResponseCorrectionBound R a a0 s g ≤ C₁ * cubeBesovPositiveVectorSeminormTwo R s g) (hweak_point : ∀ R ∈ descendantsAtDepth Q j, coarseFluxResponseRHSWeakFluxCorrectionBound R a s g ≤ C₂ * cubeBesovPositiveVectorSeminormTwo R s g) (hpoincare_point : ∀ R ∈ descendantsAtDepth Q j, coarseFluxResponseRHSPoincareCorrectionBound R a a0 s g ≤ C₃ * cubeBesovPositiveVectorSeminormTwo R s g) : localizedCoarseFluxResponseRHSResponseCorrectionBound Q a a0 s j g + localizedCoarseFluxResponseRHSWeakFluxCorrectionBound Q a s j g + localizedCoarseFluxResponseRHSPoincareCorrectionBound Q a a0 s j g ≤ (C₁ + C₂ + C₃) * localizedPositiveBesovForcingSeminormTwoAtDepth Q s j g

Component-average forcing correction bound with the descendant-localized positive-Besov forcing norm kept visible.

theorem HCPolySupport.FluxForcingCorrectionBound_le_coeffSum_mul_depthWeight_inv_mul_parent {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) {s : ℝ} (j : ℕ) (g : Vec d → Vec d) {C₁ C₂ C₃ : ℝ} (hC₁_nonneg : 0 ≤ C₁) (hC₂_nonneg : 0 ≤ C₂) (hC₃_nonneg : 0 ≤ C₃) (hGlobalBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q s N g)) (hLocalBdd : ∀ R ∈ descendantsAtDepth Q j, BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo R s N g)) (hresponse_nonneg : ∀ R ∈ descendantsAtDepth Q j, 0 ≤ coarseFluxResponseRHSResponseCorrectionBound R a a0 s g) (hweak_nonneg : ∀ R ∈ descendantsAtDepth Q j, 0 ≤ coarseFluxResponseRHSWeakFluxCorrectionBound R a s g) (hpoincare_nonneg : ∀ R ∈ descendantsAtDepth Q j, 0 ≤ coarseFluxResponseRHSPoincareCorrectionBound R a a0 s g) (hresponse_point : ∀ R ∈ descendantsAtDepth Q j, coarseFluxResponseRHSResponseCorrectionBound R a a0 s g ≤ C₁ * cubeBesovPositiveVectorSeminormTwo R s g) (hweak_point : ∀ R ∈ descendantsAtDepth Q j, coarseFluxResponseRHSWeakFluxCorrectionBound R a s g ≤ C₂ * cubeBesovPositiveVectorSeminormTwo R s g) (hpoincare_point : ∀ R ∈ descendantsAtDepth Q j, coarseFluxResponseRHSPoincareCorrectionBound R a a0 s g ≤ C₃ * cubeBesovPositiveVectorSeminormTwo R s g) : localizedCoarseFluxResponseRHSResponseCorrectionBound Q a a0 s j g + localizedCoarseFluxResponseRHSWeakFluxCorrectionBound Q a s j g + localizedCoarseFluxResponseRHSPoincareCorrectionBound Q a a0 s j g ≤ (C₁ + C₂ + C₃) * ((Real.rpow 3 (s * ↑j))⁻¹ * cubeBesovPositiveVectorSeminormTwo Q s g)

Component-average forcing correction bound with the inverse depth weight exposed after applying positive-Besov localization.

theorem HCPolySupport.FluxForcingCorrectionBound_le_coeffSum_mul_PositiveBesovForcing_forceExponent {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) {s t : ℝ} (j : ℕ) (g : Vec d → Vec d) {C₁ C₂ C₃ : ℝ} (hC₁_nonneg : 0 ≤ C₁) (hC₂_nonneg : 0 ≤ C₂) (hC₃_nonneg : 0 ≤ C₃) (hresponse_nonneg : ∀ R ∈ descendantsAtDepth Q j, 0 ≤ coarseFluxResponseRHSResponseCorrectionBound R a a0 s g) (hweak_nonneg : ∀ R ∈ descendantsAtDepth Q j, 0 ≤ coarseFluxResponseRHSWeakFluxCorrectionBound R a s g) (hpoincare_nonneg : ∀ R ∈ descendantsAtDepth Q j, 0 ≤ coarseFluxResponseRHSPoincareCorrectionBound R a a0 s g) (hresponse_point : ∀ R ∈ descendantsAtDepth Q j, coarseFluxResponseRHSResponseCorrectionBound R a a0 s g ≤ C₁ * cubeBesovPositiveVectorSeminormTwo R t g) (hweak_point : ∀ R ∈ descendantsAtDepth Q j, coarseFluxResponseRHSWeakFluxCorrectionBound R a s g ≤ C₂ * cubeBesovPositiveVectorSeminormTwo R t g) (hpoincare_point : ∀ R ∈ descendantsAtDepth Q j, coarseFluxResponseRHSPoincareCorrectionBound R a a0 s g ≤ C₃ * cubeBesovPositiveVectorSeminormTwo R t g) : localizedCoarseFluxResponseRHSResponseCorrectionBound Q a a0 s j g + localizedCoarseFluxResponseRHSWeakFluxCorrectionBound Q a s j g + localizedCoarseFluxResponseRHSPoincareCorrectionBound Q a a0 s j g ≤ (C₁ + C₂ + C₃) * localizedPositiveBesovForcingSeminormTwoAtDepth Q t j g

Two-exponent component-average forcing correction bound. The flux-response components are evaluated at exponent s, while the force is measured in the stronger positive-Besov seminorm at exponent t.

theorem HCPolySupport.FluxForcingCorrectionBound_le_coeffSum_mul_depthWeight_inv_mul_parentExponent {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) {s t : ℝ} (j : ℕ) (g : Vec d → Vec d) {C₁ C₂ C₃ : ℝ} (hC₁_nonneg : 0 ≤ C₁) (hC₂_nonneg : 0 ≤ C₂) (hC₃_nonneg : 0 ≤ C₃) (hGlobalBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q t N g)) (hLocalBdd : ∀ R ∈ descendantsAtDepth Q j, BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo R t N g)) (hresponse_nonneg : ∀ R ∈ descendantsAtDepth Q j, 0 ≤ coarseFluxResponseRHSResponseCorrectionBound R a a0 s g) (hweak_nonneg : ∀ R ∈ descendantsAtDepth Q j, 0 ≤ coarseFluxResponseRHSWeakFluxCorrectionBound R a s g) (hpoincare_nonneg : ∀ R ∈ descendantsAtDepth Q j, 0 ≤ coarseFluxResponseRHSPoincareCorrectionBound R a a0 s g) (hresponse_point : ∀ R ∈ descendantsAtDepth Q j, coarseFluxResponseRHSResponseCorrectionBound R a a0 s g ≤ C₁ * cubeBesovPositiveVectorSeminormTwo R t g) (hweak_point : ∀ R ∈ descendantsAtDepth Q j, coarseFluxResponseRHSWeakFluxCorrectionBound R a s g ≤ C₂ * cubeBesovPositiveVectorSeminormTwo R t g) (hpoincare_point : ∀ R ∈ descendantsAtDepth Q j, coarseFluxResponseRHSPoincareCorrectionBound R a a0 s g ≤ C₃ * cubeBesovPositiveVectorSeminormTwo R t g) : localizedCoarseFluxResponseRHSResponseCorrectionBound Q a a0 s j g + localizedCoarseFluxResponseRHSWeakFluxCorrectionBound Q a s j g + localizedCoarseFluxResponseRHSPoincareCorrectionBound Q a a0 s j g ≤ (C₁ + C₂ + C₃) * ((Real.rpow 3 (t * ↑j))⁻¹ * cubeBesovPositiveVectorSeminormTwo Q t g)

Two-exponent component-average forcing correction bound with the inverse depth weight exposed at the force exponent.

theorem HCPolySupport.FluxForcingCorrectionBound_le_coarseGrainingL2FluxDefectForcingTerm_of_coeff {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) {s : ℝ} (j : ℕ) (g : Vec d → Vec d) (hs : 0 < s) (hB_nonneg : 0 ≤ cubeBesovPositiveVectorSeminormTwo Q s g) (havg : (descendantsAverage Q j fun (R : TriadicCube d) => cubeBesovPositiveVectorSeminormTwo R s g ^ 2) ≤ cubeBesovPositiveVectorSeminormTwo Q s g ^ 2) (hresponse_nonneg : ∀ R ∈ descendantsAtDepth Q j, 0 ≤ coarseFluxResponseRHSResponseCorrectionBound R a a0 s g) (hweak_nonneg : ∀ R ∈ descendantsAtDepth Q j, 0 ≤ coarseFluxResponseRHSWeakFluxCorrectionBound R a s g) (hpoincare_nonneg : ∀ R ∈ descendantsAtDepth Q j, 0 ≤ coarseFluxResponseRHSPoincareCorrectionBound R a a0 s g) (hresponse_point : ∀ R ∈ descendantsAtDepth Q j, 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) (hweak_point : ∀ R ∈ descendantsAtDepth Q j, 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) (hpoincare_point : ∀ R ∈ descendantsAtDepth Q j, 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) : 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

The three localized forcing-correction averages are absorbed by the §3.3.B forcing term once their pointwise descendant coefficients are bounded by the corresponding parent coefficients and the local positive-Besov squares average back to the parent seminorm.

theorem HCPolySupport.fluxForcingCorrectionBound_le_coarseGrainingForcingTerm_of_parentBounds {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)) (hresponse_point : ∀ R ∈ descendantsAtDepth Q j, 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) (hweak_point : ∀ R ∈ descendantsAtDepth Q j, 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) (hpoincare_point : ∀ R ∈ descendantsAtDepth Q j, 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) : 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

Bounded-positive-Besov version of FluxForcingCorrectionBound_le_coarseGrainingL2FluxDefectForcingTerm_of_coeff.

theorem HCPolySupport.localizedCoarseFluxResponseRHSBound_le_component_average_sum {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) {s : ℝ} (j : ℕ) (gradU g : Vec d → Vec d) (henergy_nonneg : ∀ R ∈ descendantsAtDepth Q j, 0 ≤ coarseFluxResponseRHSEnergyBound R a a0 s gradU) (hresponse_nonneg : ∀ R ∈ descendantsAtDepth Q j, 0 ≤ coarseFluxResponseRHSResponseCorrectionBound R a a0 s g) (hweak_nonneg : ∀ R ∈ descendantsAtDepth Q j, 0 ≤ coarseFluxResponseRHSWeakFluxCorrectionBound R a s g) (hpoincare_nonneg : ∀ R ∈ descendantsAtDepth Q j, 0 ≤ coarseFluxResponseRHSPoincareCorrectionBound R a a0 s g) : localizedCoarseFluxResponseRHSBound Q a a0 s j gradU g ≤ localizedCoarseFluxResponseRHSEnergyBound Q a a0 s j gradU + localizedCoarseFluxResponseRHSResponseCorrectionBound Q a a0 s j g + localizedCoarseFluxResponseRHSWeakFluxCorrectionBound Q a s j g + localizedCoarseFluxResponseRHSPoincareCorrectionBound Q a a0 s j g

Minkowski split of the localized one-cube §3.2.4 RHS average into its four component averages.

theorem HCPolySupport.localizedCoarseFluxResponseRHSBound_le_energy_add_forcing_of_component_average_bounds {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) {s : ℝ} (j : ℕ) (gradU g : Vec d → Vec d) {E F : ℝ} (henergy_nonneg : ∀ R ∈ descendantsAtDepth Q j, 0 ≤ coarseFluxResponseRHSEnergyBound R a a0 s gradU) (hresponse_nonneg : ∀ R ∈ descendantsAtDepth Q j, 0 ≤ coarseFluxResponseRHSResponseCorrectionBound R a a0 s g) (hweak_nonneg : ∀ R ∈ descendantsAtDepth Q j, 0 ≤ coarseFluxResponseRHSWeakFluxCorrectionBound R a s g) (hpoincare_nonneg : ∀ R ∈ descendantsAtDepth Q j, 0 ≤ coarseFluxResponseRHSPoincareCorrectionBound R a a0 s g) (henergy : localizedCoarseFluxResponseRHSEnergyBound Q a a0 s j gradU ≤ E) (hforcing : localizedCoarseFluxResponseRHSResponseCorrectionBound Q a a0 s j g + localizedCoarseFluxResponseRHSWeakFluxCorrectionBound Q a s j g + localizedCoarseFluxResponseRHSPoincareCorrectionBound Q a a0 s j g ≤ F) : localizedCoarseFluxResponseRHSBound Q a a0 s j gradU g ≤ E + F

Generic recomposition of the localized one-cube RHS average from an energy bound and a forcing-correction bound.

theorem HCPolySupport.CoarseFluxRHSBound_le_energy_add_coeffSum_mul_depthWeight_inv_mul_parent {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) {s : ℝ} (j : ℕ) (gradU g : Vec d → Vec d) {E C₁ C₂ C₃ : ℝ} (hC₁_nonneg : 0 ≤ C₁) (hC₂_nonneg : 0 ≤ C₂) (hC₃_nonneg : 0 ≤ C₃) (hGlobalBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q s N g)) (hLocalBdd : ∀ R ∈ descendantsAtDepth Q j, BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo R s N g)) (henergy_nonneg : ∀ R ∈ descendantsAtDepth Q j, 0 ≤ coarseFluxResponseRHSEnergyBound R a a0 s gradU) (hresponse_nonneg : ∀ R ∈ descendantsAtDepth Q j, 0 ≤ coarseFluxResponseRHSResponseCorrectionBound R a a0 s g) (hweak_nonneg : ∀ R ∈ descendantsAtDepth Q j, 0 ≤ coarseFluxResponseRHSWeakFluxCorrectionBound R a s g) (hpoincare_nonneg : ∀ R ∈ descendantsAtDepth Q j, 0 ≤ coarseFluxResponseRHSPoincareCorrectionBound R a a0 s g) (henergy : localizedCoarseFluxResponseRHSEnergyBound Q a a0 s j gradU ≤ E) (hresponse_point : ∀ R ∈ descendantsAtDepth Q j, coarseFluxResponseRHSResponseCorrectionBound R a a0 s g ≤ C₁ * cubeBesovPositiveVectorSeminormTwo R s g) (hweak_point : ∀ R ∈ descendantsAtDepth Q j, coarseFluxResponseRHSWeakFluxCorrectionBound R a s g ≤ C₂ * cubeBesovPositiveVectorSeminormTwo R s g) (hpoincare_point : ∀ R ∈ descendantsAtDepth Q j, coarseFluxResponseRHSPoincareCorrectionBound R a a0 s g ≤ C₃ * cubeBesovPositiveVectorSeminormTwo R s g) : localizedCoarseFluxResponseRHSBound Q a a0 s j gradU g ≤ E + (C₁ + C₂ + C₃) * ((Real.rpow 3 (s * ↑j))⁻¹ * cubeBesovPositiveVectorSeminormTwo Q s g)

Scale-sharp localized RHS comparison with an arbitrary nonnegative descendant coefficient envelope for the three forcing correction components.

theorem HCPolySupport.CoarseFluxRHSBound_le_energy_add_coeffSum_mul_depthWeight_inv_mul_parentExponent {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) {s t : ℝ} (j : ℕ) (gradU g : Vec d → Vec d) {E C₁ C₂ C₃ : ℝ} (hC₁_nonneg : 0 ≤ C₁) (hC₂_nonneg : 0 ≤ C₂) (hC₃_nonneg : 0 ≤ C₃) (hGlobalBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q t N g)) (hLocalBdd : ∀ R ∈ descendantsAtDepth Q j, BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo R t N g)) (henergy_nonneg : ∀ R ∈ descendantsAtDepth Q j, 0 ≤ coarseFluxResponseRHSEnergyBound R a a0 s gradU) (hresponse_nonneg : ∀ R ∈ descendantsAtDepth Q j, 0 ≤ coarseFluxResponseRHSResponseCorrectionBound R a a0 s g) (hweak_nonneg : ∀ R ∈ descendantsAtDepth Q j, 0 ≤ coarseFluxResponseRHSWeakFluxCorrectionBound R a s g) (hpoincare_nonneg : ∀ R ∈ descendantsAtDepth Q j, 0 ≤ coarseFluxResponseRHSPoincareCorrectionBound R a a0 s g) (henergy : localizedCoarseFluxResponseRHSEnergyBound Q a a0 s j gradU ≤ E) (hresponse_point : ∀ R ∈ descendantsAtDepth Q j, coarseFluxResponseRHSResponseCorrectionBound R a a0 s g ≤ C₁ * cubeBesovPositiveVectorSeminormTwo R t g) (hweak_point : ∀ R ∈ descendantsAtDepth Q j, coarseFluxResponseRHSWeakFluxCorrectionBound R a s g ≤ C₂ * cubeBesovPositiveVectorSeminormTwo R t g) (hpoincare_point : ∀ R ∈ descendantsAtDepth Q j, coarseFluxResponseRHSPoincareCorrectionBound R a a0 s g ≤ C₃ * cubeBesovPositiveVectorSeminormTwo R t g) : localizedCoarseFluxResponseRHSBound Q a a0 s j gradU g ≤ E + (C₁ + C₂ + C₃) * ((Real.rpow 3 (t * ↑j))⁻¹ * cubeBesovPositiveVectorSeminormTwo Q t g)

Two-exponent scale-sharp localized RHS comparison with an arbitrary nonnegative descendant coefficient envelope for the forcing correction components.

theorem HCPolySupport.solution_diff_l2_le_dualityConstant_mul_energy_add_weightedParent {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 E C₁ C₂ C₃ : ℝ} (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) (hC₁_nonneg : 0 ≤ C₁) (hC₂_nonneg : 0 ≤ C₂) (hC₃_nonneg : 0 ≤ C₃) (hGlobalBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q s N g)) (hLocalBdd : ∀ R ∈ descendantsAtDepth Q j, BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo R s N g)) (henergy : localizedCoarseFluxResponseRHSEnergyBound Q a a0 s j gradU ≤ E) (hresponse_point : ∀ R ∈ descendantsAtDepth Q j, coarseFluxResponseRHSResponseCorrectionBound R a a0 s g ≤ C₁ * cubeBesovPositiveVectorSeminormTwo R s g) (hweak_point : ∀ R ∈ descendantsAtDepth Q j, coarseFluxResponseRHSWeakFluxCorrectionBound R a s g ≤ C₂ * cubeBesovPositiveVectorSeminormTwo R s g) (hpoincare_point : ∀ R ∈ descendantsAtDepth Q j, coarseFluxResponseRHSPoincareCorrectionBound R a a0 s g ≤ C₃ * cubeBesovPositiveVectorSeminormTwo R s g) : solutionComparisonNegativeBesovLhs Q s a a0 gradU gradV ≤ Cdual * s⁻¹ * (E + (C₁ + C₂ + C₃) * ((Real.rpow 3 (s * ↑j))⁻¹ * cubeBesovPositiveVectorSeminormTwo Q s g))

End-to-end localized comparison corridor with the scale-sharp forcing localization kept in the final scalar bound.

theorem HCPolySupport.localizedCoarseFluxRhs_le_fluxDefect_of_componentAverages {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) {s : ℝ} (j : ℕ) (gradU g : Vec d → Vec d) (henergy_nonneg : ∀ R ∈ descendantsAtDepth Q j, 0 ≤ coarseFluxResponseRHSEnergyBound R a a0 s gradU) (hresponse_nonneg : ∀ R ∈ descendantsAtDepth Q j, 0 ≤ coarseFluxResponseRHSResponseCorrectionBound R a a0 s g) (hweak_nonneg : ∀ R ∈ descendantsAtDepth Q j, 0 ≤ coarseFluxResponseRHSWeakFluxCorrectionBound R a s g) (hpoincare_nonneg : ∀ R ∈ descendantsAtDepth Q j, 0 ≤ coarseFluxResponseRHSPoincareCorrectionBound R a a0 s g) (henergy : localizedCoarseFluxResponseRHSEnergyBound Q a a0 s j gradU ≤ coarseGrainingL2FluxDefectEnergyTerm Q a a0 s j gradU) (hforcing : 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) : localizedCoarseFluxResponseRHSBound Q a a0 s j gradU g ≤ coarseGrainingL2FluxDefectBound Q a a0 s j gradU g

Scalar §3.3 RHS comparison from localized component-average bounds. This is the L² version of the component-envelope bridge, and is weaker than asking for pointwise descendant domination.

theorem HCPolySupport.CoarseFluxRHSBound_le_coarseGrainingFluxBound_of_boundedAbove {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) {s : ℝ} (j : ℕ) (gradU g : Vec d → Vec d) (hs : 0 < s) (hgBdd : ∀ R ∈ descendantsAtDepth Q j, BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo R s N g)) (henergy : localizedCoarseFluxResponseRHSEnergyBound Q a a0 s j gradU ≤ coarseGrainingL2FluxDefectEnergyTerm Q a a0 s j gradU) (hforcing : 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) : localizedCoarseFluxResponseRHSBound Q a a0 s j gradU g ≤ coarseGrainingL2FluxDefectBound Q a a0 s j gradU g

Bounded-positive-Besov version of the localized component-average scalar comparison.

theorem HCPolySupport.solution_diff_l2_le_coarseGrainingL2Rhs_of_descendant_fluxRHSBound_of_average {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) (henergy_nonneg : ∀ R ∈ descendantsAtDepth Q j, 0 ≤ coarseFluxResponseRHSEnergyBound R a a0 s gradU) (hresponse_nonneg : ∀ R ∈ descendantsAtDepth Q j, 0 ≤ coarseFluxResponseRHSResponseCorrectionBound R a a0 s g) (hweak_nonneg : ∀ R ∈ descendantsAtDepth Q j, 0 ≤ coarseFluxResponseRHSWeakFluxCorrectionBound R a s g) (hpoincare_nonneg : ∀ R ∈ descendantsAtDepth Q j, 0 ≤ coarseFluxResponseRHSPoincareCorrectionBound R a a0 s g) (henergy : localizedCoarseFluxResponseRHSEnergyBound Q a a0 s j gradU ≤ coarseGrainingL2FluxDefectEnergyTerm Q a a0 s j gradU) (hforcing : 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) : 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 localized component-average bounds.