Coarse-graining support: Support.Deterministic.CoarseFluxResponse.RHSConstantApexEnergy #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Energy-envelope one-cube RHS coarse-flux response apex #
This leaf keeps the component-budget apex available with one shared coefficient-energy envelope. It is the formal socket that the zero-Dirichlet energy estimate from the notes should eventually feed.
theorem
HCPolySupport.negativeBesovFluxDefect_le_two_mul_fluxResponseRHSBound_of_energyEnvelope
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : CoeffField d)
(a0 : Mat d)
(s : ℝ)
(gradU g : Vec d → Vec d)
(v : H1Function (cubeSet Q))
(w : AHarmonicFunction a (cubeSet Q))
(C : ℝ)
{lam Lam lam0 Lam0 : ℝ}
(hC_nonneg : 0 ≤ C)
(hs : 0 < s)
(hs_le : s ≤ 1)
(hEll_open : IsEllipticFieldOn lam Lam (openCubeSet Q) a)
(ha0 : IsEllipticMatrix lam0 Lam0 a0)
(ha0symm : Matrix.IsSymm a0)
(hweak : IsH1DirichletRhsWeakSolutionOn a (cubeSet Q) v g)
(hgrad : ∀ x ∈ cubeSet Q, gradU x = w.toH1.grad x + v.grad x)
(hEll_desc : ∀ (R : TriadicCube d), (∃ (n : ℕ), R ∈ descendantsAtDepth Q n) → IsEllipticFieldOn lam Lam (cubeSet R) a)
(hC_desc : (R : TriadicCube d) → (∃ (n : ℕ), R ∈ descendantsAtDepth Q n) → H1CoerciveEstimate (cubeSet R))
(hData : OpenCubeDescendantDeterministicCoarseData Q a)
(hsum_desc :
∀ (R : TriadicCube d),
(∃ (n : ℕ), R ∈ descendantsAtDepth Q n) →
Summable fun (m : ℕ) => geometricWeight s 2 m * maxDescendantBBlockNormAtScale R (R.scale - ↑m) a)
(hchildBdd :
∀ (R : TriadicCube d),
(∃ (n : ℕ), R ∈ descendantsAtDepth Q n) →
∀ S ∈ descendantsAtDepth R 1,
BddAbove
(Set.range fun (N : ℕ) =>
cubeBesovNegativeVectorPartialSeminormTwo S s N fun (x : Vec d) => matVecMul (a x) (v.grad x)))
(huBdd_desc :
∀ (R : TriadicCube d),
(∃ (n : ℕ), R ∈ descendantsAtDepth Q n) →
BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo R s N v.grad))
(hgBdd_centered_desc :
∀ (R : TriadicCube d),
(∃ (n : ℕ), R ∈ descendantsAtDepth Q n) →
BddAbove
(Set.range fun (N : ℕ) =>
cubeBesovPositiveVectorPartialSeminormTwo R s N fun (x : Vec d) => g x - cubeAverageVec R g))
{BU BV BEnergy BweakEnergy BUtail BVtail BweakForce BPoincareEnergy BPoincareForce : ℝ}
(hweakBdd : BddAbove (Set.range fun (n : ℕ) => weakFluxRHSScaledAveragedSeminormSq Q a s v.grad n))
(hsum_half :
Summable fun (l : ℕ) => geometricWeight (s / 2) 2 l * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑l) a).rpow 1)
(hint : MeasureTheory.IntegrableOn (coefficientEnergyDensity a v.grad) (cubeSet Q) MeasureTheory.volume)
(hmem : ∀ (j : ℕ), ∀ S ∈ descendantsAtDepth Q j, MeasureTheory.MemLp g 2 (normalizedCubeMeasure S))
(hLocalBdd :
∀ (n : ℕ),
∀ R ∈ descendantsAtDepth Q n, BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo R s N g))
(hBU_nonneg : 0 ≤ BU)
(hBV_nonneg : 0 ≤ BV)
(hu_tail : ∀ (k : ℕ), coarsePoincareRHSSn Q s v.grad k ≤ BU)
(hvConstructed :
∀ (j : ℕ),
∀ R ∈ descendantsAtDepth Q j,
∀ (ω : MeanZeroNeumannCorrectorData R a fun (x : Vec d) => g x - cubeAverageVec R g)
(w0 : AHarmonicFunction a (cubeSet R)),
(∀ x ∈ cubeSet R, v.grad x = w0.toH1.grad x + ω.toH1MeanZero.toH1Function.grad x) →
BddAbove
(Set.range fun (N : ℕ) =>
cubeBesovNegativeVectorPartialSeminormTwo R s N fun (x : Vec d) => w0.toH1.grad x) ∧ (cubeBesovNegativeVectorSeminormTwo R s fun (x : Vec d) => w0.toH1.grad x) ^ 2 ≤ (coarsePoincareRHSDepthWeight s j)⁻¹ * BV)
(hdefectW_partialBdd :
BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminorm Q s N (fluxDefect a a0 w.toH1.grad)))
(hresponseSum :
Summable fun (n : ℕ) =>
geometricWeight s 1 n * scaleResponseAtScale Q (Q.scale - ↑n) MultiscaleExponent.infinity a a0)
(hhomogeneous :
coarseFluxResponseQOneBound Q a a0 s w ≤ C * coarseFluxResponseRHSHomogeneousSplitBound Q a a0 s gradU g)
(henergyEnvelope : cubeAverage Q (coefficientEnergyDensity a v.grad) ≤ BEnergy)
(hweakEnergyBudget : 50 * s⁻¹ ^ 2 * LambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a * BEnergy ≤ BweakEnergy)
(hBU : 5 * s⁻¹ * BU ≤ BUtail)
(hBV : 5 * s⁻¹ * BV ≤ BVtail)
(hweakForce :
2500 * s⁻¹ ^ 4 * LambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a ^ 2 * (↑d * (3 ^ (↑d + s) * √2)) ^ 2 * cubeBesovPositiveVectorSeminormTwo Q s g ^ 2 ≤ BweakForce)
(hweakBudget :
BweakEnergy + BUtail + BVtail + BweakForce ≤ (C * coarseFluxResponseRHSWeakFluxCorrectionBound Q a s g) ^ 2)
(hPoincareEnergyBudget :
matNorm a0 ^ 2 * (250 * s⁻¹ ^ 2 * (lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ * BEnergy) ≤ BPoincareEnergy)
(hPoincareForce :
matNorm a0 ^ 2 * (15000 * s⁻¹ ^ 4 * (lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ ^ 2 * (↑d * (3 ^ (↑d + s) * √2)) ^ 2 * cubeBesovPositiveVectorSeminormTwo Q s g ^ 2) ≤ BPoincareForce)
(hPoincareBudget : BPoincareEnergy + BPoincareForce ≤ (C * coarseFluxResponseRHSPoincareCorrectionBound Q a a0 s g) ^ 2)
:
cubeBesovNegativeVectorSeminormTwo Q s (fluxDefect a a0 gradU) ≤ 2 * C * coarseFluxResponseRHSBound Q a a0 s gradU g
Component-budget one-cube apex where the weak-flux and Poincare energy components are both derived from a single parent cube-energy envelope.
The remaining tail and force component budgets stay explicit: those are different analytic estimates in the notes. The common energy envelope is the piece supplied by the zero-Dirichlet RHS energy estimate.