A normal-ordering constant independent of the lower material cutoff.
theorem
AVenhance.Infra.Section4.amnr_word_L2_le_uniform_cut
{U : Set AmnrSpace}
(hU : IsOpen U)
{μ : MeasureTheory.Measure AmnrSpace}
(hμ : μ.AbsolutelyContinuous (MeasureTheory.volume.restrict U))
{b : AmnrSpace → Homogenization.Vec 2}
{f : AmnrSpace → ℝ}
{N cut : ℕ}
(hcutN : cut ≤ N)
(hb : ContDiff ℝ (↑⊤) b)
(hf : ContDiffOn ℝ (↑N) f U)
{S H G Cb : ℝ}
(hS : 0 < S)
(hH : 0 < H)
(hG : 0 ≤ G)
(hCb : 0 ≤ Cb)
(hfb :
∀ (α : List (Fin 2)) (n : ℕ),
α.length + 2 * n ≤ N →
n ≤ cut →
MeasureTheory.eLpNorm (amnrWord b (amnrMixedWord α n) f) 2 μ ≤ ENNReal.ofReal (G * amnrWeight S H (amnrMixedWord α n)))
(hBb :
∀ (p i : Fin 2) (α : List (Fin 2)),
∀ n < cut,
α.length + 2 * n + 2 ≤ N →
∀ z ∈ U,
|amnrWord b (amnrMixedWord α n) (amnrVelocityGradient b p i) z| ≤ Cb * H * amnrWeight S H (amnrMixedWord α n))
(w : List (Option (Fin 2)))
(hw : amnrBudget w ≤ N)
(hc : amnrMaterialCount w ≤ cut)
:
MeasureTheory.eLpNorm (amnrWord b w f) 2 μ ≤ ENNReal.ofReal (amnrNormalOrderConstant N Cb N * ↑(amnrCanonicalSamples N N).card * G * amnrWeight S H w)
A lower-material canonical estimate controls any ordered word with the same total budget using one constant for all cutoffs up to N.