Coarse-graining support: Support.Deterministic.CoarseFluxResponse.RHSConstantApex #

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

Constant-envelope one-cube RHS coarse-flux response apex #

This leaf composes the C-scaled correction wrappers with the split recomposition theorem. The remaining mathematical inputs are the analytic component budgets: the homogeneous energy correction and the zero-Dirichlet RHS weak-flux/Poincare budgets.

source

theorem HCPolySupport.negativeBesovSeminormTwo_fluxDefect_le_two_mul_const_mul_fluxRHSBound {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 : IsEllipticFieldOn lam Lam (cubeSet Q) a) (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) (hu_mem_desc : ∀ (R : TriadicCube d), (∃ (n : ℕ), R ∈ descendantsAtDepth Q n) → MemVectorL2 (cubeSet R) v.grad) (hg_mem_desc : ∀ (R : TriadicCube d), (∃ (n : ℕ), R ∈ descendantsAtDepth Q n) → MemVectorL2 (cubeSet R) g) (hC_desc : (R : TriadicCube d) → (∃ (n : ℕ), R ∈ descendantsAtDepth Q n) → H1CoerciveEstimate (cubeSet R)) (hData_desc : ∀ (R : TriadicCube d), (∃ (n : ℕ), R ∈ descendantsAtDepth Q n) → OpenCubeDescendantDeterministicCoarseData R 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 BweakEnergy BUtail BVtail BweakForce BPoincareEnergy BPoincareForce : ℝ} (hweakBdd : BddAbove (Set.range fun (n : ℕ) => weakFluxRHSScaledAveragedSeminormSq Q a s v.grad n)) (hData : OpenCubeDescendantDeterministicCoarseData Q a) (hsum_half : Summable fun (l : ℕ) => geometricWeight (s / 2) 2 l * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑l) a).rpow 1) (havg_parent_nonneg : 0 ≤ cubeAverage Q (coefficientEnergyDensity a v.grad)) (havg_nonneg : ∀ (n : ℕ), ∀ R ∈ descendantsAtDepth Q n, 0 ≤ cubeAverage R (coefficientEnergyDensity a v.grad)) (hint : MeasureTheory.IntegrableOn (coefficientEnergyDensity a v.grad) (cubeSet Q) MeasureTheory.volume) (hmem : ∀ (j : ℕ), ∀ S ∈ descendantsAtDepth Q j, MeasureTheory.MemLp g 2 (normalizedCubeMeasure S)) (hg : MeasureTheory.MemLp g 2 (normalizedCubeMeasure Q)) (hGlobalBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q s N g)) (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) (hfluxV_bdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N fun (x : Vec d) => matVecMul (a x) (v.grad x))) (ha0V_bdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N fun (x : Vec d) => matVecMul a0 (v.grad x))) (hgrad_bdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N v.grad)) (hweakEnergy : 50 * s⁻¹ ^ 2 * LambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a * cubeAverage Q (coefficientEnergyDensity a v.grad) ≤ 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) (hPoincareEnergy : matNorm a0 ^ 2 * (250 * s⁻¹ ^ 2 * (lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ * cubeAverage Q (coefficientEnergyDensity a v.grad)) ≤ 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

One-cube §3.2.4 RHS flux-response recomposition with a single nonnegative constant multiplying each compact component.

The theorem is intentionally still component-budget-facing: it records the formal route from the H¹ weak-solution estimates to the manuscript-shaped C(d) one-cube bound, while leaving the analytic energy/tail/forcing budget estimates as explicit hypotheses.

source

cubeBesovNegativeVectorSeminormTwo Q s (fluxDefect a a0 gradU) ≤ 2 * C * coarseFluxResponseRHSBound Q a a0 s gradU g

Same one-cube apex with the weak-flux and Poincare scalar sides stated as the exact expanded budget inequalities, rather than through auxiliary budget variables. This is the cleanest current note-facing surface: the remaining analytic work is precisely the two displayed scalar budget bounds plus the homogeneous energy-correction estimate.

source

cubeBesovNegativeVectorSeminormTwo Q s (fluxDefect a a0 gradU) ≤ 2 * C * coarseFluxResponseRHSBound Q a a0 s gradU g

Exact-budget one-cube apex with coefficient-energy average nonnegativity derived from the ellipticity hypotheses.

This is the cleaner note-facing surface after the average-nonnegativity bookkeeping has been moved into the RHS layer.

source

cubeBesovNegativeVectorSeminormTwo Q s (fluxDefect a a0 gradU) ≤ 2 * C * coarseFluxResponseRHSBound Q a a0 s gradU g

Exact-budget one-cube apex with the parent-cube ellipticity hypothesis derived from descendant ellipticity at depth zero.

This removes the redundant standalone IsEllipticFieldOn ... (cubeSet Q) a input when the caller already supplies ellipticity on all descendants of Q.

source

theorem HCPolySupport.negativeBesovFluxDefect_le_two_mul_fluxResponseRHSBound_of_exactComponentBudgets {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 : ℝ} (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) (hweakBudget : 50 * s⁻¹ ^ 2 * LambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a * cubeAverage Q (coefficientEnergyDensity a v.grad) + 5 * s⁻¹ * BU + 5 * s⁻¹ * BV + 2500 * s⁻¹ ^ 4 * LambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a ^ 2 * (↑d * (3 ^ (↑d + s) * √2)) ^ 2 * cubeBesovPositiveVectorSeminormTwo Q s g ^ 2 ≤ (C * coarseFluxResponseRHSWeakFluxCorrectionBound Q a s g) ^ 2) (hPoincareBudget : matNorm a0 ^ 2 * (250 * s⁻¹ ^ 2 * (lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ * cubeAverage Q (coefficientEnergyDensity a v.grad)) + 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) ≤ (C * coarseFluxResponseRHSPoincareCorrectionBound Q a a0 s g) ^ 2) :

cubeBesovNegativeVectorSeminormTwo Q s (fluxDefect a a0 gradU) ≤ 2 * C * coarseFluxResponseRHSBound Q a a0 s gradU g

Exact-budget one-cube apex with all parent depth-zero inputs derived from the corresponding descendant/global hypotheses.

Besides deriving self-cube ellipticity from descendant ellipticity, this wrapper also derives the descendant deterministic-data family from the single parent descendant-data hypothesis, the descendant MemVectorL2 v.grad family from the H¹ input, the parent a∇v partial boundedness from ellipticity and H¹ data, the parent v.grad and a₀∇v partial boundedness inputs from the descendant v.grad boundedness family, the parent MemLp g, the descendant MemVectorL2 g family, and the parent positive-Besov boundedness hypothesis from their descendant/global versions.

Documentation

LeanPool.HighContrastHomogenization.Support.Deterministic.CoarseFluxResponse.RHSConstantApex

Coarse-graining support: Support.Deterministic.CoarseFluxResponse.RHSConstantApex #

Constant-envelope one-cube RHS coarse-flux response apex #