Documentation

LeanPool.HighContrastHomogenization.Support.Deterministic.WeakFluxRHS.AbsorbedApex

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

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

source
theorem HCPolySupport.exists_negativeBesovFluxAverage_matrixVectorMultiply_le_sqrt_of_parent_potential {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (s η : ℝ) (u g : Vec d → Vec d) {lam Lam : ℝ} (hs : 0 < s) (hη : 0 < η) (hu_potential : IsPotentialOn (cubeSet Q) u) (hu_residual : IsSolenoidalOn (cubeSet Q) fun (x : Vec d) => matVecMul (a x) (u x) - g 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) u) (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) (u x))) (huBdd_desc : ∀ (R : TriadicCube d), (∃ (n : ℕ), R ∈ descendantsAtDepth Q n) → BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo R s N u)) (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)) (m : ℕ) {BU BV : ℝ} (hBdd : BddAbove (Set.range fun (n : ℕ) => weakFluxRHSScaledAveragedSeminormSq Q a s u 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 u)) (havg_nonneg : ∀ (n : ℕ), ∀ R ∈ descendantsAtDepth Q n, 0 ≤ cubeAverage R (coefficientEnergyDensity a u)) (hint : MeasureTheory.IntegrableOn (coefficientEnergyDensity a u) (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 : ∀ (k : ℕ), coarsePoincareRHSSn Q s u (m + k) ≤ BU) :
∃ (v : TriadicCube d → Vec d → Vec d), (∀ (R : TriadicCube d), (∃ (n : ℕ), R ∈ descendantsAtDepth Q n) → BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo R s N (v R))) → (∀ (k : ℕ), weakFluxRHSHarmonicRemainderScaledAveragedSeminormSq Q s v (m + k) ≤ BV) → localizedFluxDefectNegativeBesovAverageTwo Q s (fun (x : Vec d) => matVecMul (a x) (u x)) m ≤ √((coarsePoincareRHSDepthWeight s m)⁻¹ * ((weakFluxRHSWeightedCoefficientEnergyBase Q a u s + η * BU + η * BV + weakFluxRHSWeightedGlobalForceBase Q a g s η m) * (1 - Real.rpow 3 (-s))⁻¹))

Global localized weak-flux estimate with the local absorbed recurrence derived from parent potential/solenoidal data on descendant cubes.

This removes the anonymous hlocal recurrence hypothesis from negativeBesovFluxAverage_matrixVectorMultiply_le_sqrt. The selected harmonic remainders still expose their local boundedness and global tail bound, which are the next closure obligations for the note-facing weak-flux RHS apex.

source
theorem HCPolySupport.exists_negativeBesovFluxAverage_matrixAction_le_sqrt_of_descendantRemainderBound {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (s η : ℝ) (u g : Vec d → Vec d) {lam Lam : ℝ} (hs : 0 < s) (hη : 0 < η) (hu_potential : IsPotentialOn (cubeSet Q) u) (hu_residual : IsSolenoidalOn (cubeSet Q) fun (x : Vec d) => matVecMul (a x) (u x) - g 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) u) (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) (u x))) (huBdd_desc : ∀ (R : TriadicCube d), (∃ (n : ℕ), R ∈ descendantsAtDepth Q n) → BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo R s N u)) (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)) (m : ℕ) {BU BV : ℝ} (hBdd : BddAbove (Set.range fun (n : ℕ) => weakFluxRHSScaledAveragedSeminormSq Q a s u 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 u)) (havg_nonneg : ∀ (n : ℕ), ∀ R ∈ descendantsAtDepth Q n, 0 ≤ cubeAverage R (coefficientEnergyDensity a u)) (hint : MeasureTheory.IntegrableOn (coefficientEnergyDensity a u) (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 : ∀ (k : ℕ), coarsePoincareRHSSn Q s u (m + k) ≤ BU) :
∃ (v : TriadicCube d → Vec d → Vec d), (∀ (R : TriadicCube d), (∃ (n : ℕ), R ∈ descendantsAtDepth Q n) → BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo R s N (v R))) → (∀ (k : ℕ), ∀ R ∈ descendantsAtDepth Q (m + k), cubeBesovNegativeVectorSeminormTwo R s (v R) ^ 2 ≤ (coarsePoincareRHSDepthWeight s (m + k))⁻¹ * BV) → localizedFluxDefectNegativeBesovAverageTwo Q s (fun (x : Vec d) => matVecMul (a x) (u x)) m ≤ √((coarsePoincareRHSDepthWeight s m)⁻¹ * ((weakFluxRHSWeightedCoefficientEnergyBase Q a u s + η * BU + η * BV + weakFluxRHSWeightedGlobalForceBase Q a g s η m) * (1 - Real.rpow 3 (-s))⁻¹))

Global localized weak-flux estimate with the selected harmonic-remainder tail derived from descendantwise squared control.

This is the same parent potential/solenoidal wrapper as exists_negativeBesovFluxAverage_matrixVectorMultiply_le_sqrt_of_parent_potential, but it asks for pointwise descendant control of the selected remainders at the reciprocal depth-weight scale instead of an already-averaged tail bound.

source
theorem HCPolySupport.negativeBesovFluxAverage_matVecMul_le_sqrt_of_parent_potential_solenoidal {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (s η : ℝ) (u g : Vec d → Vec d) {lam Lam : ℝ} (hs : 0 < s) (hη : 0 < η) (hu_potential : IsPotentialOn (cubeSet Q) u) (hu_residual : IsSolenoidalOn (cubeSet Q) fun (x : Vec d) => matVecMul (a x) (u x) - g 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) u) (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) (u x))) (huBdd_desc : ∀ (R : TriadicCube d), (∃ (n : ℕ), R ∈ descendantsAtDepth Q n) → BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo R s N u)) (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)) (m : ℕ) {BU BV : ℝ} (hBdd : BddAbove (Set.range fun (n : ℕ) => weakFluxRHSScaledAveragedSeminormSq Q a s u 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 u)) (havg_nonneg : ∀ (n : ℕ), ∀ R ∈ descendantsAtDepth Q n, 0 ≤ cubeAverage R (coefficientEnergyDensity a u)) (hint : MeasureTheory.IntegrableOn (coefficientEnergyDensity a u) (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 : ∀ (k : ℕ), coarsePoincareRHSSn Q s u (m + 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, u 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) :
localizedFluxDefectNegativeBesovAverageTwo Q s (fun (x : Vec d) => matVecMul (a x) (u x)) m ≤ √((coarsePoincareRHSDepthWeight s m)⁻¹ * ((weakFluxRHSWeightedCoefficientEnergyBase Q a u s + η * BU + η * BV + weakFluxRHSWeightedGlobalForceBase Q a g s η m) * (1 - Real.rpow 3 (-s))⁻¹))

Global localized weak-flux estimate with the selected harmonic-remainder boundedness and square tail both discharged from bounds on every local harmonic remainder produced by the centered Neumann-corrector construction.

source
theorem HCPolySupport.negativeBesovFluxAverage_matVecMul_le_sqrt_of_parent_potential_of_constructed {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (u g : Vec d → Vec d) {lam Lam : ℝ} (hs : 0 < s) (hu_potential : IsPotentialOn (cubeSet Q) u) (hu_residual : IsSolenoidalOn (cubeSet Q) fun (x : Vec d) => matVecMul (a x) (u x) - g 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) u) (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) (u x))) (huBdd_desc : ∀ (R : TriadicCube d), (∃ (n : ℕ), R ∈ descendantsAtDepth Q n) → BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo R s N u)) (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)) (m : ℕ) {BU BV : ℝ} (hBdd : BddAbove (Set.range fun (n : ℕ) => weakFluxRHSScaledAveragedSeminormSq Q a s u 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 u)) (havg_nonneg : ∀ (n : ℕ), ∀ R ∈ descendantsAtDepth Q n, 0 ≤ cubeAverage R (coefficientEnergyDensity a u)) (hint : MeasureTheory.IntegrableOn (coefficientEnergyDensity a u) (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 : ∀ (k : ℕ), coarsePoincareRHSSn Q s u (m + 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, u 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) :
localizedFluxDefectNegativeBesovAverageTwo Q s (fun (x : Vec d) => matVecMul (a x) (u x)) m ≤ √((coarsePoincareRHSDepthWeight s m)⁻¹ * (weakFluxRHSAbsorbedLocalizedNoteBase Q a u g s m BU BV * (1 - Real.rpow 3 (-s))⁻¹))

Note-eta form of the constructed harmonic-remainder parent wrapper.

This fixes the absorption parameter to the manuscript choice coarsePoincareRHSNoteEta s and packages the component base as weakFluxRHSAbsorbedLocalizedNoteBase.

source
theorem HCPolySupport.exists_negativeBesovFluxAverage_matrixVectorMultiply_le_sqrt {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (s η : ℝ) (g : Vec d → Vec d) (u : H1Function (cubeSet Q)) {lam Lam : ℝ} (hs : 0 < s) (hη : 0 < η) (hweak : IsH1DirichletRhsWeakSolutionOn a (cubeSet Q) u 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) u.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) (u.grad x))) (huBdd_desc : ∀ (R : TriadicCube d), (∃ (n : ℕ), R ∈ descendantsAtDepth Q n) → BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo R s N u.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)) (m : ℕ) {BU BV : ℝ} (hBdd : BddAbove (Set.range fun (n : ℕ) => weakFluxRHSScaledAveragedSeminormSq Q a s u.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 u.grad)) (havg_nonneg : ∀ (n : ℕ), ∀ R ∈ descendantsAtDepth Q n, 0 ≤ cubeAverage R (coefficientEnergyDensity a u.grad)) (hint : MeasureTheory.IntegrableOn (coefficientEnergyDensity a u.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 u.grad (m + k) ≤ BU) :
∃ (v : TriadicCube d → Vec d → Vec d), (∀ (R : TriadicCube d), (∃ (n : ℕ), R ∈ descendantsAtDepth Q n) → BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo R s N (v R))) → (∀ (k : ℕ), weakFluxRHSHarmonicRemainderScaledAveragedSeminormSq Q s v (m + k) ≤ BV) → localizedFluxDefectNegativeBesovAverageTwo Q s (fun (x : Vec d) => matVecMul (a x) (u.grad x)) m ≤ √((coarsePoincareRHSDepthWeight s m)⁻¹ * ((weakFluxRHSWeightedCoefficientEnergyBase Q a u.grad s + η * BU + η * BV + weakFluxRHSWeightedGlobalForceBase Q a g s η m) * (1 - Real.rpow 3 (-s))⁻¹))

H¹ weak-solution wrapper for the global localized weak-flux estimate.

The PDE hypothesis -div(a grad u) = div g supplies the parent potential field and residual solenoidal flux required by exists_negativeBesovFluxAverage_matrixVectorMultiply_le_sqrt_of_parent_potential.

source
theorem HCPolySupport.exists_negativeBesovFluxAverage_matrixVectorMultiply_le_sqrt_of_descendant {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (s η : ℝ) (g : Vec d → Vec d) (u : H1Function (cubeSet Q)) {lam Lam : ℝ} (hs : 0 < s) (hη : 0 < η) (hweak : IsH1DirichletRhsWeakSolutionOn a (cubeSet Q) u 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) u.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) (u.grad x))) (huBdd_desc : ∀ (R : TriadicCube d), (∃ (n : ℕ), R ∈ descendantsAtDepth Q n) → BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo R s N u.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)) (m : ℕ) {BU BV : ℝ} (hBdd : BddAbove (Set.range fun (n : ℕ) => weakFluxRHSScaledAveragedSeminormSq Q a s u.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 u.grad)) (havg_nonneg : ∀ (n : ℕ), ∀ R ∈ descendantsAtDepth Q n, 0 ≤ cubeAverage R (coefficientEnergyDensity a u.grad)) (hint : MeasureTheory.IntegrableOn (coefficientEnergyDensity a u.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 u.grad (m + k) ≤ BU) :
∃ (v : TriadicCube d → Vec d → Vec d), (∀ (R : TriadicCube d), (∃ (n : ℕ), R ∈ descendantsAtDepth Q n) → BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo R s N (v R))) → (∀ (k : ℕ), ∀ R ∈ descendantsAtDepth Q (m + k), cubeBesovNegativeVectorSeminormTwo R s (v R) ^ 2 ≤ (coarsePoincareRHSDepthWeight s (m + k))⁻¹ * BV) → localizedFluxDefectNegativeBesovAverageTwo Q s (fun (x : Vec d) => matVecMul (a x) (u.grad x)) m ≤ √((coarsePoincareRHSDepthWeight s m)⁻¹ * ((weakFluxRHSWeightedCoefficientEnergyBase Q a u.grad s + η * BU + η * BV + weakFluxRHSWeightedGlobalForceBase Q a g s η m) * (1 - Real.rpow 3 (-s))⁻¹))

H¹ weak-solution wrapper whose selected harmonic-remainder tail is supplied by descendantwise squared bounds rather than an averaged tail hypothesis.

source
theorem HCPolySupport.negativeBesovFluxAverage_matVecMul_le_sqrt_of_h1DirichletRhsWeakSolutionOn {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (s η : ℝ) (g : Vec d → Vec d) (u : H1Function (cubeSet Q)) {lam Lam : ℝ} (hs : 0 < s) (hη : 0 < η) (hweak : IsH1DirichletRhsWeakSolutionOn a (cubeSet Q) u 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) u.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) (u.grad x))) (huBdd_desc : ∀ (R : TriadicCube d), (∃ (n : ℕ), R ∈ descendantsAtDepth Q n) → BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo R s N u.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)) (m : ℕ) {BU BV : ℝ} (hBdd : BddAbove (Set.range fun (n : ℕ) => weakFluxRHSScaledAveragedSeminormSq Q a s u.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 u.grad)) (havg_nonneg : ∀ (n : ℕ), ∀ R ∈ descendantsAtDepth Q n, 0 ≤ cubeAverage R (coefficientEnergyDensity a u.grad)) (hint : MeasureTheory.IntegrableOn (coefficientEnergyDensity a u.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 u.grad (m + 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, u.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) :
localizedFluxDefectNegativeBesovAverageTwo Q s (fun (x : Vec d) => matVecMul (a x) (u.grad x)) m ≤ √((coarsePoincareRHSDepthWeight s m)⁻¹ * ((weakFluxRHSWeightedCoefficientEnergyBase Q a u.grad s + η * BU + η * BV + weakFluxRHSWeightedGlobalForceBase Q a g s η m) * (1 - Real.rpow 3 (-s))⁻¹))

H¹ weak-solution form of the constructed harmonic-remainder bound wrapper.

source
theorem HCPolySupport.negativeBesovFluxAverage_matVecMul_le_sqrt_of_of_h1DirichletRhsWeakSolutionOn {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (g : Vec d → Vec d) (u : H1Function (cubeSet Q)) {lam Lam : ℝ} (hs : 0 < s) (hweak : IsH1DirichletRhsWeakSolutionOn a (cubeSet Q) u 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) u.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) (u.grad x))) (huBdd_desc : ∀ (R : TriadicCube d), (∃ (n : ℕ), R ∈ descendantsAtDepth Q n) → BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo R s N u.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)) (m : ℕ) {BU BV : ℝ} (hBdd : BddAbove (Set.range fun (n : ℕ) => weakFluxRHSScaledAveragedSeminormSq Q a s u.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 u.grad)) (havg_nonneg : ∀ (n : ℕ), ∀ R ∈ descendantsAtDepth Q n, 0 ≤ cubeAverage R (coefficientEnergyDensity a u.grad)) (hint : MeasureTheory.IntegrableOn (coefficientEnergyDensity a u.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 u.grad (m + 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, u.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) :
localizedFluxDefectNegativeBesovAverageTwo Q s (fun (x : Vec d) => matVecMul (a x) (u.grad x)) m ≤ √((coarsePoincareRHSDepthWeight s m)⁻¹ * (weakFluxRHSAbsorbedLocalizedNoteBase Q a u.grad g s m BU BV * (1 - Real.rpow 3 (-s))⁻¹))

H¹ weak-solution note-eta form of the constructed harmonic-remainder wrapper.