Coarse-graining support: #
Support.Deterministic.CoarseFluxResponse.RHSConstantApexZeroDirichletEstimates
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Split estimate targets for the zero-Dirichlet RHS flux-response apex #
This leaf separates the remaining analytic inputs to the §3.2.4 zero-Dirichlet one-cube apex into the two pieces supplied by the manuscript:
- the harmonic-remainder
BVtail estimate; - the displayed weak-flux and Poincare component inequalities.
theorem
HCPolySupport.ZeroTraceDirichletCorrectorData.coarseFluxResponseRHSWeakFluxCorrectionBound_sq_eq
{d : ℕ}
(Q : TriadicCube d)
(a : CoeffField d)
{s : ℝ}
(g : Vec d → Vec d)
(hs : 0 < s)
:
coarseFluxResponseRHSWeakFluxCorrectionBound Q a s g ^ 2 = s.rpow (-(5 / 2)) ^ 2 * LambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a * (lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ * cubeBesovPositiveVectorSeminormTwo Q s g ^ 2
Square expansion for the compact weak-flux correction factor. This is the scalar core needed by the displayed weak-flux radicand estimate.
theorem
HCPolySupport.ZeroTraceDirichletCorrectorData.const_mul_coarseFluxResponseRHSWeakFluxCorrectionBound_sq_eq
{d : ℕ}
(Q : TriadicCube d)
(a : CoeffField d)
(C : ℝ)
{s : ℝ}
(g : Vec d → Vec d)
(hs : 0 < s)
:
Square expansion for the constant-multiplied compact weak-flux correction
factor. This is the exact right-hand side shape of the displayed weak-flux
radicand estimate after the manuscript's constant C(d) is inserted.
theorem
HCPolySupport.ZeroTraceDirichletCorrectorData.coarseFluxResponseRHSPoincareCorrectionBound_sq_eq
{d : ℕ}
(Q : TriadicCube d)
(a : CoeffField d)
(a0 : Mat d)
(s : ℝ)
(g : Vec d → Vec d)
:
Square expansion for the compact Poincare correction factor. This is the scalar core needed by the displayed Poincare radicand estimate.
theorem
HCPolySupport.ZeroTraceDirichletCorrectorData.const_mul_coarseFluxResponseRHSPoincareCorrectionBound_sq_eq
{d : ℕ}
(Q : TriadicCube d)
(a : CoeffField d)
(a0 : Mat d)
(C s : ℝ)
(g : Vec d → Vec d)
:
Square expansion for the constant-multiplied compact Poincare correction
factor. This is the exact right-hand side shape of the displayed Poincare
radicand estimate after the manuscript's constant C(d) is inserted.
def
HCPolySupport.ZeroTraceDirichletCorrectorData.zeroTraceDirichletHarmonicRemainderTailBounded
{d : ℕ}
{Q : TriadicCube d}
{a : CoeffField d}
{g : Vec d → Vec d}
(ρ : ZeroTraceDirichletCorrectorData Q a g)
(s : ℝ)
:
Boundedness side of the harmonic-remainder tail package.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
HCPolySupport.ZeroTraceDirichletCorrectorData.zeroTraceDirichletHarmonicRemainderBVEstimate
{d : ℕ}
{Q : TriadicCube d}
{a : CoeffField d}
{g : Vec d → Vec d}
(ρ : ZeroTraceDirichletCorrectorData Q a g)
(s BV : ℝ)
:
Squared BV estimate side of the harmonic-remainder tail package.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
HCPolySupport.ZeroTraceDirichletCorrectorData.zeroTraceDirichletHarmonicRemainderBVEstimate_mono
{d : ℕ}
{Q : TriadicCube d}
{a : CoeffField d}
{g : Vec d → Vec d}
{ρ : ZeroTraceDirichletCorrectorData Q a g}
{s BV BV' : ℝ}
(hBV : BV ≤ BV')
(hestimate : ρ.zeroTraceDirichletHarmonicRemainderBVEstimate s BV)
:
theorem
HCPolySupport.ZeroTraceDirichletCorrectorData.zeroTraceDirichletHarmonicRemainderTailBounded_of_pos
{d : ℕ}
{Q : TriadicCube d}
{a : CoeffField d}
{g : Vec d → Vec d}
(ρ : ZeroTraceDirichletCorrectorData Q a g)
{s : ℝ}
(hs : 0 < s)
:
theorem
HCPolySupport.ZeroTraceDirichletCorrectorData.zeroTraceDirichletHarmonicRemainderTailClose_bounded
{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_bvEstimate
{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_of_bounded_of_bvEstimate
{d : ℕ}
{Q : TriadicCube d}
{a : CoeffField d}
{g : Vec d → Vec d}
(ρ : ZeroTraceDirichletCorrectorData Q a g)
{s BV : ℝ}
(hBV_nonneg : 0 ≤ BV)
(hbounded : ρ.zeroTraceDirichletHarmonicRemainderTailBounded s)
(hestimate : ρ.zeroTraceDirichletHarmonicRemainderBVEstimate s BV)
:
theorem
HCPolySupport.ZeroTraceDirichletCorrectorData.zeroTraceDirichletHarmonicRemainderTailClose_of_bvEstimate
{d : ℕ}
{Q : TriadicCube d}
{a : CoeffField d}
{g : Vec d → Vec d}
(ρ : ZeroTraceDirichletCorrectorData Q a g)
{s BV : ℝ}
(hs : 0 < s)
(hBV_nonneg : 0 ≤ BV)
(hestimate : ρ.zeroTraceDirichletHarmonicRemainderBVEstimate s BV)
:
theorem
HCPolySupport.ZeroTraceDirichletCorrectorData.zeroTraceDirichletHarmonicRemainderTailClose_iff_bounded_and_bvEstimate
{d : ℕ}
{Q : TriadicCube d}
{a : CoeffField d}
{g : Vec d → Vec d}
{ρ : ZeroTraceDirichletCorrectorData Q a g}
{s BV : ℝ}
:
theorem
HCPolySupport.ZeroTraceDirichletCorrectorData.zeroTraceDirichletHarmonicRemainderTailClose_iff_bvEstimate_of_pos
{d : ℕ}
{Q : TriadicCube d}
{a : CoeffField d}
{g : Vec d → Vec d}
{ρ : ZeroTraceDirichletCorrectorData Q a g}
{s BV : ℝ}
(hs : 0 < s)
:
ρ.zeroTraceDirichletHarmonicRemainderTailClose s BV ↔ 0 ≤ BV ∧ ρ.zeroTraceDirichletHarmonicRemainderBVEstimate s BV
theorem
HCPolySupport.ZeroTraceDirichletCorrectorData.zeroTraceDirichletHarmonicRemainderScaledAveragedTail_le_of_bvEstimate_of_selector
{d : ℕ}
{Q : TriadicCube d}
{a : CoeffField d}
{g : Vec d → Vec d}
{ρ : ZeroTraceDirichletCorrectorData Q a g}
{s BV : ℝ}
(hestimate : ρ.zeroTraceDirichletHarmonicRemainderBVEstimate s BV)
(v : TriadicCube d → Vec d → Vec d)
(hselector :
∀ (R : TriadicCube d),
(∃ (n : ℕ), R ∈ descendantsAtDepth Q n) →
∃ (ω : MeanZeroNeumannCorrectorData R a fun (x : Vec d) => g x - cubeAverageVec R g) (w0 :
AHarmonicFunction a (cubeSet R)),
(v R = fun (x : Vec d) => w0.toH1.grad x) ∧ ∀ x ∈ cubeSet R, ρ.toH10.grad x = w0.toH1.grad x + ω.toH1MeanZero.toH1Function.grad x)
(m k : ℕ)
:
A descendantwise zero-trace harmonic-remainder BV estimate controls the
scaled averaged harmonic-remainder tail used by the weak-flux RHS iteration,
for any selector whose values are produced by the local Neumann-corrector
decompositions.
theorem
HCPolySupport.ZeroTraceDirichletCorrectorData.zeroTraceDirichletHarmonicRemainderBVEstimate_of_zeroForce_energy_bounds
{d : ℕ}
[NeZero d]
{Q : TriadicCube d}
{a : CoeffField d}
{g : Vec d → Vec d}
(ρ : ZeroTraceDirichletCorrectorData Q a g)
{s BV lam Lam : ℝ}
(hs : 0 < s)
(hs_le : s ≤ 1)
(hEll_desc : ∀ (R : TriadicCube d), (∃ (n : ℕ), R ∈ descendantsAtDepth Q n) → IsEllipticFieldOn lam Lam (cubeSet R) a)
(henergy :
∀ (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) →
250 * s⁻¹ ^ 2 * (lambdaSq R (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ * cubeAverage R (coefficientEnergyDensity a fun (x : Vec d) => w0.toH1.grad x) ≤ (coarsePoincareRHSDepthWeight s j)⁻¹ * BV)
:
The zero-force coarse-Poincare RHS theorem reduces the harmonic-remainder
BV estimate to descendantwise coefficient-energy control of the selected
harmonic remainders.
theorem
HCPolySupport.ZeroTraceDirichletCorrectorData.zeroTraceDirichletHarmonicRemainderBVEstimate_of_corrector_neumann_energy_bounds
{d : ℕ}
[NeZero d]
{Q : TriadicCube d}
{a : CoeffField d}
{g : Vec d → Vec d}
(ρ : ZeroTraceDirichletCorrectorData Q a g)
{s BV Bρ Bω lam Lam : ℝ}
(hs : 0 < s)
(hs_le : s ≤ 1)
(hEll_desc : ∀ (R : TriadicCube d), (∃ (n : ℕ), R ∈ descendantsAtDepth Q n) → IsEllipticFieldOn lam Lam (cubeSet R) a)
(hρEnergy :
∀ (j : ℕ),
∀ R ∈ descendantsAtDepth Q j,
500 * s⁻¹ ^ 2 * (lambdaSq R (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ * cubeAverage R (coefficientEnergyDensity a fun (x : Vec d) => ρ.toH10.grad x) ≤ (coarsePoincareRHSDepthWeight s j)⁻¹ * Bρ)
(hωEnergy :
∀ (j : ℕ),
∀ R ∈ descendantsAtDepth Q j,
∀ (ω : MeanZeroNeumannCorrectorData R a fun (x : Vec d) => g x - cubeAverageVec R g),
500 * s⁻¹ ^ 2 * (lambdaSq R (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ * cubeAverage R (coefficientEnergyDensity a fun (x : Vec d) => ω.toH1MeanZero.toH1Function.grad x) ≤ (coarsePoincareRHSDepthWeight s j)⁻¹ * Bω)
(hbudget : Bρ + Bω ≤ BV)
:
The local identity ρ = w0 + ω reduces the harmonic-remainder BV estimate
to separate coefficient-energy tail bounds for the zero-trace gradient and the
centered Neumann corrector.
theorem
HCPolySupport.ZeroTraceDirichletCorrectorData.zeroTraceDirichletHarmonicRemainderBVEstimate_of_corrector_energy_and_neumann_seminorm_bounds
{d : ℕ}
[NeZero d]
{Q : TriadicCube d}
{a : CoeffField d}
{g : Vec d → Vec d}
(ρ : ZeroTraceDirichletCorrectorData Q a g)
{s BV Bρ Bω lam Lam : ℝ}
(hs : 0 < s)
(hs_le : s ≤ 1)
(hEll_desc : ∀ (R : TriadicCube d), (∃ (n : ℕ), R ∈ descendantsAtDepth Q n) → IsEllipticFieldOn lam Lam (cubeSet R) a)
(hg_mem_desc : ∀ (j : ℕ), ∀ R ∈ descendantsAtDepth Q j, MeasureTheory.MemLp g 2 (normalizedCubeMeasure R))
(hgBdd_centered_desc :
∀ (j : ℕ),
∀ R ∈ descendantsAtDepth Q j,
BddAbove
(Set.range fun (N : ℕ) =>
cubeBesovPositiveVectorPartialSeminormTwo R s N fun (x : Vec d) => g x - cubeAverageVec R g))
(hρEnergy :
∀ (j : ℕ),
∀ R ∈ descendantsAtDepth Q j,
500 * s⁻¹ ^ 2 * (lambdaSq R (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ * cubeAverage R (coefficientEnergyDensity a fun (x : Vec d) => ρ.toH10.grad x) ≤ (coarsePoincareRHSDepthWeight s j)⁻¹ * Bρ)
(hωSeminormTail :
∀ (j : ℕ),
∀ R ∈ descendantsAtDepth Q j,
∀ (ω : MeanZeroNeumannCorrectorData R a fun (x : Vec d) => g x - cubeAverageVec R g),
500 * s⁻¹ ^ 2 * (lambdaSq R (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ * (↑d * ((3 ^ (↑d + s) * cubeBesovNegativeVectorSeminormTwo R s fun (x : Vec d) => ω.toH1MeanZero.toH1Function.grad x) * cubeBesovPositiveVectorSeminormTwo R s fun (x : Vec d) => g x - cubeAverageVec R g)) ≤ (coarsePoincareRHSDepthWeight s j)⁻¹ * Bω)
(hbudget : Bρ + Bω ≤ BV)
:
The centered Neumann-corrector energy identity controls the Neumann half of
the harmonic-remainder BV reduction by the product of the corrector negative
seminorm and the centered forcing positive seminorm.
theorem
HCPolySupport.ZeroTraceDirichletCorrectorData.zeroTraceDirichletHarmonicRemainderBVEstimate_of_corrector_energy_and_neumann_young_bounds
{d : ℕ}
[NeZero d]
{Q : TriadicCube d}
{a : CoeffField d}
{g : Vec d → Vec d}
(ρ : ZeroTraceDirichletCorrectorData Q a g)
{s BV Bρ BωNeg BωForce lam Lam : ℝ}
(hs : 0 < s)
(hs_le : s ≤ 1)
(hEll_desc : ∀ (R : TriadicCube d), (∃ (n : ℕ), R ∈ descendantsAtDepth Q n) → IsEllipticFieldOn lam Lam (cubeSet R) a)
(hg_mem_desc : ∀ (j : ℕ), ∀ R ∈ descendantsAtDepth Q j, MeasureTheory.MemLp g 2 (normalizedCubeMeasure R))
(hgBdd_centered_desc :
∀ (j : ℕ),
∀ R ∈ descendantsAtDepth Q j,
BddAbove
(Set.range fun (N : ℕ) =>
cubeBesovPositiveVectorPartialSeminormTwo R s N fun (x : Vec d) => g x - cubeAverageVec R g))
(hρEnergy :
∀ (j : ℕ),
∀ R ∈ descendantsAtDepth Q j,
500 * s⁻¹ ^ 2 * (lambdaSq R (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ * cubeAverage R (coefficientEnergyDensity a fun (x : Vec d) => ρ.toH10.grad x) ≤ (coarsePoincareRHSDepthWeight s j)⁻¹ * Bρ)
(hωNegSqTail :
∀ (j : ℕ),
∀ R ∈ descendantsAtDepth Q j,
∀ (ω : MeanZeroNeumannCorrectorData R a fun (x : Vec d) => g x - cubeAverageVec R g),
250 * s⁻¹ ^ 2 * (lambdaSq R (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ * (cubeBesovNegativeVectorSeminormTwo R s fun (x : Vec d) => ω.toH1MeanZero.toH1Function.grad x) ^ 2 ≤ (coarsePoincareRHSDepthWeight s j)⁻¹ * BωNeg)
(hcenteredForceSqTail :
∀ (j : ℕ),
∀ R ∈ descendantsAtDepth Q j,
250 * s⁻¹ ^ 2 * (lambdaSq R (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ * (↑d * (3 ^ (↑d + s) * cubeBesovPositiveVectorSeminormTwo R s fun (x : Vec d) => g x - cubeAverageVec R g)) ^ 2 ≤ (coarsePoincareRHSDepthWeight s j)⁻¹ * BωForce)
(hbudget : Bρ + (BωNeg + BωForce) ≤ BV)
:
def
HCPolySupport.ZeroTraceDirichletCorrectorData.zeroTraceDirichletPoincareDisplayedComponentBoundsClose
{d : ℕ}
(Q : TriadicCube d)
(a : CoeffField d)
(a0 : Mat d)
(C s : ℝ)
(g : Vec d → Vec d)
:
Displayed Poincare component estimates after inserting the energy envelope.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
HCPolySupport.ZeroTraceDirichletCorrectorData.zeroTraceDirichletPoincareDisplayedComponentBoundsClose_of_bounds
{d : ℕ}
(Q : TriadicCube d)
(a : CoeffField d)
(a0 : Mat d)
(C s : ℝ)
(g : Vec d → Vec d)
{BPoincareEnergy BPoincareForce : ℝ}
(hPoincareEnergy :
matNorm a0 ^ 2 * (250 * s⁻¹ ^ 2 * (lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ * zeroTraceDirichletEnergyEnvelope Q a s g) ≤ 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)
:
theorem
HCPolySupport.ZeroTraceDirichletCorrectorData.zeroTraceDirichletPoincareDisplayedComponentBoundsClose_of_displayed_bound
{d : ℕ}
(Q : TriadicCube d)
(a : CoeffField d)
(a0 : Mat d)
(C s : ℝ)
(g : Vec d → Vec d)
(hPoincareBudget :
zeroTraceDirichletPoincareDisplayedScalarBudget Q a a0 s g ≤ (C * coarseFluxResponseRHSPoincareCorrectionBound Q a a0 s g) ^ 2)
:
theorem
HCPolySupport.ZeroTraceDirichletCorrectorData.zeroTraceDirichletPoincareDisplayedComponentBoundsClose_displayed_bound
{d : ℕ}
{Q : TriadicCube d}
{a : CoeffField d}
{a0 : Mat d}
{C s : ℝ}
{g : Vec d → Vec d}
(h : zeroTraceDirichletPoincareDisplayedComponentBoundsClose Q a a0 C s g)
:
zeroTraceDirichletPoincareDisplayedScalarBudget Q a a0 s g ≤ (C * coarseFluxResponseRHSPoincareCorrectionBound Q a a0 s g) ^ 2
theorem
HCPolySupport.ZeroTraceDirichletCorrectorData.zeroTraceDirichletPoincareDisplayedComponentBoundsClose_iff_displayed_bound
{d : ℕ}
(Q : TriadicCube d)
(a : CoeffField d)
(a0 : Mat d)
(C s : ℝ)
(g : Vec d → Vec d)
:
zeroTraceDirichletPoincareDisplayedComponentBoundsClose Q a a0 C s g ↔ zeroTraceDirichletPoincareDisplayedScalarBudget Q a a0 s g ≤ (C * coarseFluxResponseRHSPoincareCorrectionBound Q a a0 s g) ^ 2