Coarse-graining support: Support.Book.Ch03.Theorems.EnergyRHS.Neumann #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Energy RHS: Neumann estimate #
theorem
HCPolySupport.Book.Ch03.neumannForcedSolutionEnergyAverage_le_force_scale_noteConstants_expanded_publicCoeffField
{d : ℕ}
[NeZero d]
{Q : TriadicCube d}
{a : CoeffFamily d}
{s : ℝ}
{g : Vec d → Vec d}
(w : NeumannForcedCubeSolution Q a g)
(hs : 0 < s)
(hs_lt : s < 1)
(hg : ForceBesovRegularity Q s g)
:
cubeAverage Q (coefficientEnergyDensity (publicCoeffField Q a) fun (x : Vec d) => w.toH1MeanZero.toH1Function.grad x) ≤ 500 * s⁻¹ ^ 2 * (lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) (publicCoeffField Q a))⁻¹ * (↑d * (3 ^ (↑d + s) * √2)) ^ 2 * cubeBesovPositiveVectorSeminormTwo Q s g ^ 2
Public Neumann forced solutions supply the deterministic mean-zero corrector-energy estimate on the half-open cube.
theorem
HCPolySupport.Book.Ch03.neumannForcedSolutionEnergyNorm_le_sqrt_force_scale_noteConstants_expanded_publicCoeffField
{d : ℕ}
[NeZero d]
{Q : TriadicCube d}
{a : CoeffFamily d}
{s : ℝ}
{g : Vec d → Vec d}
(w : NeumannForcedCubeSolution Q a g)
(hs : 0 < s)
(hs_lt : s < 1)
(hg : ForceBesovRegularity Q s g)
:
Square-root form of the public Neumann forced-solution energy envelope before the final dimension-only constant absorption.
theorem
HCPolySupport.Book.Ch03.neumannForcedSolutionEnergyNorm_le_publicRHS_of_constant
{d : ℕ}
[NeZero d]
{C : ℝ}
(hC_nonneg : 0 ≤ C)
(hC_neumann : √500 * (↑d * (Real.rpow 3 (↑d + 1) * √2)) ≤ C)
{Q : TriadicCube d}
{a : CoeffFamily d}
{s : ℝ}
{g : Vec d → Vec d}
(w : NeumannForcedCubeSolution Q a g)
(hs : 0 < s)
(hs_lt : s < 1)
(hg : ForceBesovRegularity Q s g)
:
Public Neumann forced-solution energy estimate, assuming the displayed constant dominates the dimension-only scalar from the deterministic envelope.