Coarse-graining support: Support.Deterministic.CoarseFluxResponse.RHSCorrections

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

RHS correction components for the coarse-flux response split

This file contains the first correction-component bridge in manuscript §3.2.4. The core split algebra stays in CoarseFluxResponse.RHS; here we import the heavier §3.2.3 weak-flux RHS apex only where it is actually used.

noncomputable def HCPolySupport.coarseFluxResponseRHSWeakFluxExpandedBound {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (g gradV : Vec d → Vec d) (m : ℕ) (BU BV : ℝ) : ℝ

The expanded note-facing §3.2.3 weak-flux RHS used before it is absorbed into the compact §3.2.4 weak-flux correction component.

Equations

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

theorem HCPolySupport.negativeBesovSeminormTwo_matrixVectorMultiply_le_weakFluxCorrectionBound {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (gradV g : Vec d → Vec d) {BU BV : ℝ} (hfluxV_bdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N fun (x : Vec d) => matVecMul (a x) (gradV x))) (hlocalized : localizedFluxDefectNegativeBesovAverageTwo Q s (fun (x : Vec d) => matVecMul (a x) (gradV x)) 0 ≤ coarseFluxResponseRHSWeakFluxExpandedBound Q a s g gradV 0 BU BV) (hscalar : coarseFluxResponseRHSWeakFluxExpandedBound Q a s g gradV 0 BU BV ≤ coarseFluxResponseRHSWeakFluxCorrectionBound Q a s g) : (cubeBesovNegativeVectorSeminormTwo Q s fun (x : Vec d) => matVecMul (a x) (gradV x)) ≤ coarseFluxResponseRHSWeakFluxCorrectionBound Q a s g

Depth-zero bridge from the localized §3.2.3 weak-flux output to the one-cube q = 2 component estimate used in the §3.2.4 split.

theorem HCPolySupport.negativeBesovSeminormTwo_matrixVectorMultiply_grad_le_weakFluxCorrectionBound {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (g : Vec d → Vec d) (v : H1Function (cubeSet Q)) {lam Lam : ℝ} (hs : 0 < s) (hs_le : s ≤ 1) (hweak : IsH1DirichletRhsWeakSolutionOn a (cubeSet Q) v g) (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 : ℝ} (hBdd : BddAbove (Set.range fun (n : ℕ) => weakFluxRHSScaledAveragedSeminormSq Q a s v.grad n)) (hEll_open : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (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)) (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) (w : AHarmonicFunction a (cubeSet R)), (∀ x ∈ cubeSet R, v.grad x = w.toH1.grad x + ω.toH1MeanZero.toH1Function.grad x) → BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo R s N fun (x : Vec d) => w.toH1.grad x) ∧ (cubeBesovNegativeVectorSeminormTwo R s fun (x : Vec d) => w.toH1.grad x) ^ 2 ≤ (coarsePoincareRHSDepthWeight s j)⁻¹ * BV) (hfluxV_bdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N fun (x : Vec d) => matVecMul (a x) (v.grad x))) (hscalar : coarseFluxResponseRHSWeakFluxExpandedBound Q a s g v.grad 0 BU BV ≤ coarseFluxResponseRHSWeakFluxCorrectionBound Q a s g) : (cubeBesovNegativeVectorSeminormTwo Q s fun (x : Vec d) => matVecMul (a x) (v.grad x)) ≤ coarseFluxResponseRHSWeakFluxCorrectionBound Q a s g

The a∇v correction component in the §3.2.4 split, discharged from the note-facing H¹ §3.2.3 weak-flux RHS apex. The remaining scalar hypothesis is the manuscript constant-absorption step comparing the expanded weak-flux RHS with the compact §3.2.4 component.

theorem HCPolySupport.vecNormSq_matVecMul_le_matNormSq_mul_vecNormSq {d : ℕ} (A : Mat d) (ξ : Vec d) : vecNormSq (matVecMul A ξ) ≤ matNormSq A * vecNormSq ξ

Frobenius control of a constant matrix acting on a vector. This is the pointwise algebraic core used to move a constant coarse matrix through the note-normalized negative seminorm.

theorem HCPolySupport.cubeAverageVec_matVecMul_const {d : ℕ} (Q : TriadicCube d) (A : Mat d) (u : Vec d → Vec d) (hu : MemVectorL2 (cubeSet Q) u) : (cubeAverageVec Q fun (x : Vec d) => matVecMul A (u x)) = matVecMul A (cubeAverageVec Q u)

The cube average commutes with applying a constant matrix to a vector field.

theorem HCPolySupport.cubeBesovNegativeVectorDepthAverage_constMatMul_le {d : ℕ} (Q : TriadicCube d) (A : Mat d) (u : Vec d → Vec d) (j : ℕ) (hu_desc : ∀ R ∈ descendantsAtDepth Q j, MemVectorL2 (cubeSet R) u) : cubeBesovNegativeVectorDepthAverage Q (fun (x : Vec d) => matVecMul A (u x)) j ≤ matNormSq A * cubeBesovNegativeVectorDepthAverage Q u j

Depthwise action of a constant matrix on the q = 2 negative Besov descendant-average quantity.

theorem HCPolySupport.cubeBesovNegativeVectorPartialSeminormTwo_constMatMul_le {d : ℕ} (Q : TriadicCube d) (s : ℝ) (A : Mat d) (u : Vec d → Vec d) (N : ℕ) (hu_desc : ∀ j ∈ Finset.range (N + 1), ∀ R ∈ descendantsAtDepth Q j, MemVectorL2 (cubeSet R) u) : (cubeBesovNegativeVectorPartialSeminormTwo Q s N fun (x : Vec d) => matVecMul A (u x)) ≤ matNorm A * cubeBesovNegativeVectorPartialSeminormTwo Q s N u

Finite q = 2 negative seminorm control under a constant matrix action.

theorem HCPolySupport.cubeBesovNegativeVectorSeminormTwo_constMatMul_le {d : ℕ} (Q : TriadicCube d) (s : ℝ) (A : Mat d) (u : Vec d → Vec d) (hu_desc : ∀ (j : ℕ), ∀ R ∈ descendantsAtDepth Q j, MemVectorL2 (cubeSet R) u) (huBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N u)) : (cubeBesovNegativeVectorSeminormTwo Q s fun (x : Vec d) => matVecMul A (u x)) ≤ matNorm A * cubeBesovNegativeVectorSeminormTwo Q s u

Full q = 2 negative seminorm control under a constant matrix action.

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

The expanded note-facing RHS Poincare bound before the constant-coefficient correction a₀∇v is absorbed into the compact §3.2.4 Poincare component.

Equations

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

theorem HCPolySupport.negativeBesovSeminormTwo_constMatMul_le_fluxPoincareCorrectionBound {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (s : ℝ) (gradV g : Vec d → Vec d) {Bgrad : ℝ} (hmat : (cubeBesovNegativeVectorSeminormTwo Q s fun (x : Vec d) => matVecMul a0 (gradV x)) ≤ matNorm a0 * cubeBesovNegativeVectorSeminormTwo Q s gradV) (hgrad : cubeBesovNegativeVectorSeminormTwo Q s gradV ≤ Bgrad) (hscalar : matNorm a0 * Bgrad ≤ coarseFluxResponseRHSPoincareCorrectionBound Q a a0 s g) : (cubeBesovNegativeVectorSeminormTwo Q s fun (x : Vec d) => matVecMul a0 (gradV x)) ≤ coarseFluxResponseRHSPoincareCorrectionBound Q a a0 s g

Poincare-correction bridge from a gradient RHS Poincare bound plus a constant-matrix action estimate to the a₀∇v component in the §3.2.4 split.

theorem HCPolySupport.negativeBesovSeminormTwo_matrixAction_le_poincareCorrection_of_scalarBound {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (s : ℝ) (gradV g : Vec d → Vec d) {Bgrad : ℝ} (hgrad_mem_desc : ∀ (j : ℕ), ∀ R ∈ descendantsAtDepth Q j, MemVectorL2 (cubeSet R) gradV) (hgrad_bdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N gradV)) (hgrad : cubeBesovNegativeVectorSeminormTwo Q s gradV ≤ Bgrad) (hscalar : matNorm a0 * Bgrad ≤ coarseFluxResponseRHSPoincareCorrectionBound Q a a0 s g) : (cubeBesovNegativeVectorSeminormTwo Q s fun (x : Vec d) => matVecMul a0 (gradV x)) ≤ coarseFluxResponseRHSPoincareCorrectionBound Q a a0 s g

Poincare-correction bridge where the constant-matrix action is discharged from descendant-local L² data plus bounded finite negative seminorms.

theorem HCPolySupport.negativeBesovSeminormTwo_constMatMul_grad_le_fluxPoincareCorrectionBound {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (s : ℝ) (g : Vec d → Vec d) (v : H1Function (cubeSet Q)) {lam Lam : ℝ} (hs : 0 < s) (hs_le : s ≤ 1) (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hweak : IsH1DirichletRhsWeakSolutionOn a (cubeSet Q) v g) (hg : MeasureTheory.MemLp g 2 (normalizedCubeMeasure Q)) (hGlobalBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q s N g)) (hgrad_mem_desc : ∀ (j : ℕ), ∀ R ∈ descendantsAtDepth Q j, MemVectorL2 (cubeSet R) v.grad) (hgrad_bdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N v.grad)) (hscalar : matNorm a0 * coarseFluxResponseRHSPoincareExpandedBound Q a s g v.grad ≤ coarseFluxResponseRHSPoincareCorrectionBound Q a a0 s g) : (cubeBesovNegativeVectorSeminormTwo Q s fun (x : Vec d) => matVecMul a0 (v.grad x)) ≤ coarseFluxResponseRHSPoincareCorrectionBound Q a a0 s g

The a₀∇v correction component routed through the H¹ RHS Poincare theorem. The constant-matrix action is discharged by the seminorm bridge above; the remaining scalar hypothesis is the compact-manuscript absorption step.