Coarse-graining support: Support.Deterministic.WeakFluxRHS.AbsorbedNoteApex #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
theorem
HCPolySupport.negativeBesovFluxAverage_matrixVectorMultiply_le_sqrt_of_noteBase
{d : ℕ}
(Q : TriadicCube d)
(a : CoeffField d)
(u g : Vec d → Vec d)
{s : ℝ}
(hs : 0 < s)
(hs_le : s ≤ 1)
(m : ℕ)
{BU BV : ℝ}
(havg_nonneg : 0 ≤ cubeAverage Q (coefficientEnergyDensity a u))
(hBU_nonneg : 0 ≤ BU)
(hBV_nonneg : 0 ≤ BV)
(hmain :
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))⁻¹)))
:
localizedFluxDefectNegativeBesovAverageTwo Q s (fun (x : Vec d) => matVecMul (a x) (u x)) m ≤ √((coarsePoincareRHSDepthWeight s m)⁻¹ * (50 * s⁻¹ ^ 2 * LambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a * cubeAverage Q (coefficientEnergyDensity a u) + 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))
Square-root bridge from the note-base weak-flux apex to the expanded note-constant energy/seminorm forcing RHS.
theorem
HCPolySupport.negativeBesovFluxAverage_matVecMul_le_sqrt_of_constructedRemainder
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : CoeffField d)
(s : ℝ)
(u g : Vec d → Vec d)
{lam Lam : ℝ}
(hs : 0 < s)
(hs_le : s ≤ 1)
(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)⁻¹ * (50 * s⁻¹ ^ 2 * LambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a * cubeAverage Q (coefficientEnergyDensity a u) + 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))
Parent potential/solenoidal note-facing weak-flux RHS apex with the absorbed base expanded into the manuscript energy/seminorm forcing RHS.
theorem
HCPolySupport.negativeBesovFluxAverage_matVecMul_le_sqrt_of_weakSolution
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : CoeffField d)
(s : ℝ)
(g : Vec d → Vec d)
(u : H1Function (cubeSet Q))
{lam Lam : ℝ}
(hs : 0 < s)
(hs_le : s ≤ 1)
(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)⁻¹ * (50 * s⁻¹ ^ 2 * LambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a * cubeAverage Q (coefficientEnergyDensity a u.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))
H¹ weak-solution note-facing weak-flux RHS apex with the absorbed base expanded into the manuscript energy/seminorm forcing RHS.
theorem
HCPolySupport.negativeBesovFluxAverage_matVecMul_le_sqrt_of_weakSolution_of_BesovRegularity
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : CoeffField d)
(s : ℝ)
(g : Vec d → Vec d)
(u : H1Function (cubeSet Q))
{lam Lam : ℝ}
(hs : 0 < s)
(hs_le : s ≤ 1)
(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)
(hg : CubeVectorBesovHRegularity Q s 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)⁻¹ * (50 * s⁻¹ ^ 2 * LambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a * cubeAverage Q (coefficientEnergyDensity a u.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))
H¹ weak-solution note-facing weak-flux RHS apex with the RHS H^s regularity
data compressed to the manuscript-facing package.