Documentation

LeanPool.HighContrastHomogenization.Support.Deterministic.WeakFluxRHS.CorrectorEnergyAveraged

Coarse-graining support: Support.Deterministic.WeakFluxRHS.CorrectorEnergyAveraged #

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

Averaged corrector-energy input for the corrected weak-flux route #

This leaf turns the local Neumann-corrector force-scale estimate into the depth-weighted descendant average used by the corrected zero-Dirichlet weak-flux recurrence.

source
theorem HCPolySupport.weakFluxRHSCorrectorEnergyForceScale_mul_inv_one_sub_step_le_noteForceScale {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (g : Vec d → Vec d) {s : ℝ} (hs : 0 < s) (hs_le : s ≤ 1) :
1000 * (geometricDiscount s 2)⁻¹ * s⁻¹ ^ 2 * LambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a * (lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ * (↑d * (3 ^ (↑d + s) * √2)) ^ 2 * cubeBesovPositiveVectorSeminormTwo Q s g ^ 2 * (1 - Real.rpow 3 (-s))⁻¹ ≤ 2500 * s⁻¹ ^ 4 * LambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a * (lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ * (↑d * (3 ^ (↑d + s) * √2)) ^ 2 * cubeBesovPositiveVectorSeminormTwo Q s g ^ 2

The force-scale corrector-energy base fits in the displayed corrector allocation after summing the weak-flux geometric tail.

source
theorem HCPolySupport.weakFluxRHSDepthWeight_mul_correctorEnergyErrorAverage_le_forceScale {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (g : Vec d → Vec d) {s lam Lam : ℝ} (n : ℕ) (hs : 0 < s) (hs_le : s ≤ 1) (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hg : MeasureTheory.MemLp g 2 (normalizedCubeMeasure Q)) (hGlobalBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q s N g)) (z : TriadicCube d → Vec d → Vec d) (hz : ∀ R ∈ descendantsAtDepth Q n, ∃ (ω : MeanZeroNeumannCorrectorData R a fun (x : Vec d) => g x - cubeAverageVec R g), z R = fun (x : Vec d) => ω.toH1MeanZero.toH1Function.grad x) :
coarsePoincareRHSDepthWeight s n * weakFluxRHSLocalCorrectorEnergyErrorAverage Q a z s n ≤ 1000 * (geometricDiscount s 2)⁻¹ * s⁻¹ ^ 2 * LambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a * (lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ * (↑d * (3 ^ (↑d + s) * √2)) ^ 2 * cubeBesovPositiveVectorSeminormTwo Q s g ^ 2

Depth-weighted averaged control of the corrector-energy component in the corrected weak-flux RHS recurrence.

The proof combines:

  • half-scale localization of the weak-flux local coefficient,
  • half-scale localization of the descendant lambda^{-1} factor,
  • the local Neumann-corrector energy force-scale estimate for each selected descendant corrector, and
  • the global positive-Besov descendant averaging bound.