Coarse-graining support: Support.Deterministic.CoarseFluxResponse.RHSConstantApexZeroDirichletTail #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Zero-Dirichlet tail input for the RHS coarse-flux response apex #
This leaf contains the zero-trace gradient-tail budget, the Poincare displayed
scalar budget, and the harmonic-remainder BV tail package used by the
corrected zero-Dirichlet §3.2.4 apex route.
noncomputable def
HCPolySupport.zeroTraceDirichletGradientTailBudget
{d : ℕ}
(Q : TriadicCube d)
(a : CoeffField d)
(s : ℝ)
(g : Vec d → Vec d)
:
The expanded note-constant tail budget for the zero-trace correction gradient.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
HCPolySupport.zeroTraceDirichletGradientTailBudget_nonneg
{d : ℕ}
(Q : TriadicCube d)
(a : CoeffField d)
{s : ℝ}
(g : Vec d → Vec d)
(hs : 0 < s)
:
noncomputable def
HCPolySupport.zeroTraceDirichletPoincareDisplayedScalarBudget
{d : ℕ}
(Q : TriadicCube d)
(a : CoeffField d)
(a0 : Mat d)
(s : ℝ)
(g : Vec d → Vec d)
:
The displayed Poincare scalar budget after inserting the zero-trace energy envelope.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
HCPolySupport.zeroTraceDirichletPoincareDisplayedScalarBudget_eq_scalarBudget
{d : ℕ}
(Q : TriadicCube d)
(a : CoeffField d)
(a0 : Mat d)
(s : ℝ)
(g : Vec d → Vec d)
:
zeroTraceDirichletPoincareDisplayedScalarBudget Q a a0 s g = zeroTraceDirichletPoincareScalarBudget Q a a0 s g
theorem
HCPolySupport.zeroTraceDirichletPoincareDisplayedScalarBudget_nonneg
{d : ℕ}
(Q : TriadicCube d)
(a : CoeffField d)
(a0 : Mat d)
(s : ℝ)
(g : Vec d → Vec d)
(hs : 0 < s)
:
theorem
HCPolySupport.ZeroTraceDirichletCorrectorData.coarsePoincareRHSSn_le_zeroTraceDirichletGradientTailBudget_noteConstants_expanded
{d : ℕ}
[NeZero d]
{Q : TriadicCube d}
{a : CoeffField d}
{g : Vec d → Vec d}
(ρ : ZeroTraceDirichletCorrectorData Q a g)
{s lam Lam : ℝ}
(hs : 0 < s)
(hs_le : s ≤ 1)
(hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a)
(hg : MeasureTheory.MemLp g 2 (normalizedCubeMeasure Q))
(hGlobalBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q s N g))
(m : ℕ)
:
coarsePoincareRHSSn Q s (fun (x : Vec d) => ρ.toH10.grad x) m ≤ zeroTraceDirichletGradientTailBudget Q a s g
The expanded coarse-Poincare RHS estimate gives a uniform S_k tail bound for
the zero-trace corrector gradient after inserting the zero-Dirichlet energy
envelope.
theorem
HCPolySupport.ZeroTraceDirichletCorrectorData.coarsePoincareRHSSn_tail_le_zeroTraceDirichletGradientTailBudget_noteConstants_expanded
{d : ℕ}
[NeZero d]
{Q : TriadicCube d}
{a : CoeffField d}
{g : Vec d → Vec d}
(ρ : ZeroTraceDirichletCorrectorData Q a g)
{s lam Lam : ℝ}
(hs : 0 < s)
(hs_le : s ≤ 1)
(hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a)
(hg : MeasureTheory.MemLp g 2 (normalizedCubeMeasure Q))
(hGlobalBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q s N g))
(k : ℕ)
:
coarsePoincareRHSSn Q s (fun (x : Vec d) => ρ.toH10.grad x) k ≤ zeroTraceDirichletGradientTailBudget Q a s g
def
HCPolySupport.ZeroTraceDirichletCorrectorData.zeroTraceDirichletHarmonicRemainderTailClose
{d : ℕ}
{Q : TriadicCube d}
{a : CoeffField d}
{g : Vec d → Vec d}
(ρ : ZeroTraceDirichletCorrectorData Q a g)
(s BV : ℝ)
:
The named BV tail package for the harmonic remainders constructed from the
centered Neumann corrector decomposition on descendants of the parent cube.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
HCPolySupport.ZeroTraceDirichletCorrectorData.zeroTraceDirichletHarmonicRemainderTailClose_nonneg
{d : ℕ}
{Q : TriadicCube d}
{a : CoeffField d}
{g : Vec d → Vec d}
{ρ : ZeroTraceDirichletCorrectorData Q a g}
{s BV : ℝ}
(h : ρ.zeroTraceDirichletHarmonicRemainderTailClose s BV)
:
theorem
HCPolySupport.ZeroTraceDirichletCorrectorData.zeroTraceDirichletHarmonicRemainderTailClose_constructed
{d : ℕ}
{Q : TriadicCube d}
{a : CoeffField d}
{g : Vec d → Vec d}
{ρ : ZeroTraceDirichletCorrectorData Q a g}
{s BV : ℝ}
(h : ρ.zeroTraceDirichletHarmonicRemainderTailClose s BV)
(j : ℕ)
(R : TriadicCube d)
:
R ∈ descendantsAtDepth Q j →
∀ (ω : MeanZeroNeumannCorrectorData R a fun (x : Vec d) => g x - cubeAverageVec R g)
(w0 : AHarmonicFunction a (cubeSet R)),
(∀ x ∈ cubeSet R, ρ.toH10.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
theorem
HCPolySupport.ZeroTraceDirichletCorrectorData.zeroTraceDirichletHarmonicRemainderTailClose_of_bounds
{d : ℕ}
{Q : TriadicCube d}
{a : CoeffField d}
{g : Vec d → Vec d}
(ρ : ZeroTraceDirichletCorrectorData Q a g)
{s BV : ℝ}
(hBV_nonneg : 0 ≤ BV)
(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, ρ.toH10.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)
: