Conditional norm transport to a selected extension representative #
An indexed operator's strong bound on compactly supported L^(6/5) inputs
and the selected operator's component bounds imply the vector-valued
gradient bound. The weak-gradient construction in WeakCZConsumption
supplies the separate distributional pairing and does not identify a rough
classical representative.
theorem
CKN.Core.Endgame.hasCZGradientBound_of_extension_component_bounds
(Ccomp C_CZ : ℝ)
(hCcomp : 0 ≤ Ccomp)
(hconst : 3 * Ccomp ≤ C_CZ)
(T : Fin 3 → Fin 3 → (Foundation.Parabolic.Vec3 → ℝ) → Foundation.Parabolic.Vec3 → ℝ)
(hbound :
∀ (i j : Fin 3) (G : Foundation.Parabolic.Vec3 → ℝ),
MeasureTheory.MemLp G (ENNReal.ofReal (6 / 5)) MeasureTheory.volume →
HasCompactSupport G →
MeasureTheory.eLpNorm (T i j G) (ENNReal.ofReal (6 / 5)) MeasureTheory.volume ≤ ENNReal.ofReal Ccomp * MeasureTheory.eLpNorm G (ENNReal.ofReal (6 / 5)) MeasureTheory.volume)
:
Transport an indexed extension's L^(6/5) bounds and aggregate the three output coordinates.