Coarse-graining support: Support.Deterministic.CoarseFluxResponse.RHSConstantApexZeroDirichletBV #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Averaged BV tail for the zero-Dirichlet RHS apex #
This leaf proves the averaged harmonic-remainder tail estimate actually
consumed by the weak-flux iteration. The pointwise BVEstimate package in
RHSConstantApexZeroDirichletEstimates remains available, but this theorem
targets the weaker averaged quantity appearing in the recurrence.
theorem
HCPolySupport.ZeroTraceDirichletCorrectorData.zeroTraceDirichletHarmonicRemainderSq_le_corrector_energy_and_neumann_young_terms
{d : ℕ}
[NeZero d]
{Q R : TriadicCube d}
{a : CoeffField d}
{g : Vec d → Vec d}
(ρ : ZeroTraceDirichletCorrectorData Q a g)
{j : ℕ}
(hR : R ∈ descendantsAtDepth Q j)
{s lam Lam : ℝ}
(hs : 0 < s)
(hs_le : s ≤ 1)
(hEllR : IsEllipticFieldOn lam Lam (cubeSet R) a)
(hgR : MeasureTheory.MemLp g 2 (normalizedCubeMeasure R))
(hgBdd :
BddAbove
(Set.range fun (N : ℕ) =>
cubeBesovPositiveVectorPartialSeminormTwo R s N fun (x : Vec d) => g x - cubeAverageVec R g))
(ω : MeanZeroNeumannCorrectorData R a fun (x : Vec d) => g x - cubeAverageVec R g)
(w0 : AHarmonicFunction a (cubeSet R))
(hdecomp : ∀ x ∈ cubeSet R, ρ.toH10.grad x = w0.toH1.grad x + ω.toH1MeanZero.toH1Function.grad x)
:
(cubeBesovNegativeVectorSeminormTwo R s fun (x : Vec d) => w0.toH1.grad x) ^ 2 ≤ 500 * s⁻¹ ^ 2 * (lambdaSq R (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ * cubeAverage R (coefficientEnergyDensity a fun (x : Vec d) => ρ.toH10.grad x) + (250 * s⁻¹ ^ 2 * (lambdaSq R (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ * (cubeBesovNegativeVectorSeminormTwo R s fun (x : Vec d) => ω.toH1MeanZero.toH1Function.grad x) ^ 2 + 250 * s⁻¹ ^ 2 * (lambdaSq R (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ * (↑d * (3 ^ (↑d + s) * cubeBesovPositiveVectorSeminormTwo R s fun (x : Vec d) => g x - cubeAverageVec R g)) ^ 2)
theorem
HCPolySupport.ZeroTraceDirichletCorrectorData.zeroTraceDirichletHarmonicRemainderRhoEnergyAverage_le_raw_lambdaInv_sq
{d : ℕ}
[NeZero d]
{Q : TriadicCube d}
{a : CoeffField d}
{g : Vec d → Vec d}
(ρ : ZeroTraceDirichletCorrectorData Q a g)
{s lam Lam : ℝ}
(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))
(j : ℕ)
:
(coarsePoincareRHSDepthWeight s j * descendantsAverage Q j fun (R : TriadicCube d) =>
500 * s⁻¹ ^ 2 * (lambdaSq R (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ * cubeAverage R (coefficientEnergyDensity a fun (x : Vec d) => ρ.toH10.grad x)) ≤ 325000 * (↑d * (3 ^ (↑d + s) * √2)) ^ 2 * (s⁻¹ ^ 4 * (lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ ^ 2 * cubeBesovPositiveVectorSeminormTwo Q s g ^ 2)
Raw averaged control of the zero-trace corrector-energy part of the harmonic
remainder BV budget.
This is the analytic rho component before converting the natural
lambda^{-2} scale produced by the energy envelope into the corrected
weak-flux compact Lambda * lambda^{-1} scale.
theorem
HCPolySupport.ZeroTraceDirichletCorrectorData.zeroTraceDirichletHarmonicRemainderScaledAveragedTail_le
{d : ℕ}
[NeZero d]
{Q : TriadicCube d}
{a : CoeffField d}
{g : Vec d → Vec d}
(ρ : ZeroTraceDirichletCorrectorData Q a g)
(s : ℝ)
{BV Bρ BωNeg BωForce lam Lam : ℝ}
(hs : 0 < s)
(hs_le : s ≤ 1)
(hEll_desc : ∀ (R : TriadicCube d), (∃ (n : ℕ), R ∈ descendantsAtDepth Q n) → IsEllipticFieldOn lam Lam (cubeSet R) a)
(hg_mem_desc : ∀ (j : ℕ), ∀ R ∈ descendantsAtDepth Q j, MeasureTheory.MemLp g 2 (normalizedCubeMeasure R))
(hgBdd_centered_desc :
∀ (j : ℕ),
∀ R ∈ descendantsAtDepth Q j,
BddAbove
(Set.range fun (N : ℕ) =>
cubeBesovPositiveVectorPartialSeminormTwo R s N fun (x : Vec d) => g x - cubeAverageVec R g))
(v : TriadicCube d → Vec d → Vec d)
(ω : (R : TriadicCube d) → MeanZeroNeumannCorrectorData R a fun (x : Vec d) => g x - cubeAverageVec R g)
(w0 : (R : TriadicCube d) → AHarmonicFunction a (cubeSet R))
(hv_eq : ∀ (j : ℕ), ∀ R ∈ descendantsAtDepth Q j, v R = fun (x : Vec d) => (w0 R).toH1.grad x)
(hdecomp :
∀ (j : ℕ),
∀ R ∈ descendantsAtDepth Q j,
∀ x ∈ cubeSet R, ρ.toH10.grad x = (w0 R).toH1.grad x + (ω R).toH1MeanZero.toH1Function.grad x)
(hρEnergyAvg :
∀ (j : ℕ),
(coarsePoincareRHSDepthWeight s j * descendantsAverage Q j fun (R : TriadicCube d) =>
500 * s⁻¹ ^ 2 * (lambdaSq R (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ * cubeAverage R (coefficientEnergyDensity a fun (x : Vec d) => ρ.toH10.grad x)) ≤ Bρ)
(hωNegSqAvg :
∀ (j : ℕ),
(coarsePoincareRHSDepthWeight s j * descendantsAverage Q j fun (R : TriadicCube d) =>
250 * s⁻¹ ^ 2 * (lambdaSq R (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ * (cubeBesovNegativeVectorSeminormTwo R s fun (x : Vec d) => (ω R).toH1MeanZero.toH1Function.grad x) ^ 2) ≤ BωNeg)
(hcenteredForceSqAvg :
∀ (j : ℕ),
(coarsePoincareRHSDepthWeight s j * descendantsAverage Q j fun (R : TriadicCube d) =>
250 * s⁻¹ ^ 2 * (lambdaSq R (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ * (↑d * (3 ^ (↑d + s) * cubeBesovPositiveVectorSeminormTwo R s fun (x : Vec d) => g x - cubeAverageVec R g)) ^ 2) ≤ BωForce)
(hbudget : Bρ + (BωNeg + BωForce) ≤ BV)
(j : ℕ)
: