Adjoint transfer for supplied cube Lᵖ data #
Derived from the Dirichlet and Neumann arguments ported from
scottnarmstrong/CoarseGraining at c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
The radial-truncation, Hölder and exponent calculations are independent of the
boundary condition. Clients supply the adjoint field, its estimate and the
cross-pairing identity. No prior Lᵖ membership of the field being estimated is
assumed.
theorem
HCPolySupport.CubeCalderonZygmund.cubeEuclideanLpENorm_le_of_adjoint_bound
{d : ℕ}
(Q : TriadicCube d)
(q : FiniteLpExponent)
(h : CubeEuclideanLpField Q q)
{F : Vec d → Vec d}
(hF : MemVectorL2 (openCubeSet Q) F)
{K : ENNReal}
(hK : K ≠ ⊤)
(hadjoint :
∀ (G : CubeEuclideanL2LpField Q q.conjugate),
MemVectorL2 (openCubeSet Q) G.toField →
∃ (V : Vec d → Vec d),
MemVectorL2 (openCubeSet Q) V ∧ (cubeBoundedMeasurableDomain Q).normalizedEuclideanLpENorm q.conjugate.exponent V ≤ K * (cubeBoundedMeasurableDomain Q).normalizedEuclideanLpENorm q.conjugate.exponent G.toField ∧ ∫ (x : Vec d), vecDot (F x) (G.toField x) ∂(cubeBoundedMeasurableDomain Q).normalizedVolume = ∫ (x : Vec d), vecDot (h.toField x) (V x) ∂(cubeBoundedMeasurableDomain Q).normalizedVolume)
:
A finite adjoint bound and cross-pairing identity yield the supplied-field
Lᵖ estimate on any cube, independently of the adjoint boundary condition.