Coarse-graining support: Support.Deterministic.CoarsePoincareRHS.Regularity #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
RHS regularity package for Chapter 3 #
This file records the Lean-facing form of the manuscript assumption
g ∈ H^s(Q; R^d) used by the deterministic right-hand-side estimates.
structure
HCPolySupport.CubeVectorBesovHRegularity
{d : ℕ}
(Q : TriadicCube d)
(s : ℝ)
(g : Vec d → Vec d)
:
Note-facing H^s regularity for a vector right-hand side on one cube.
The current Besov development consumes this assumption through L²
membership and boundedness of the positive-order partial Besov seminorms.
- memLp : MeasureTheory.MemLp g 2 (normalizedCubeMeasure Q)
- partialSeminorms_bddAbove : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q s N g)
Instances For
theorem
HCPolySupport.CubeVectorBesovHRegularity.of_exponent_le
{d : ℕ}
{Q : TriadicCube d}
{s t : ℝ}
{g : Vec d → Vec d}
(hg : CubeVectorBesovHRegularity Q t g)
(hst : s ≤ t)
: