Quantitative L2 normal ordering with exact finite jet budgets.

theorem AVenhance.Infra.Section4.amnr_word_L2_le_on_of_finite_mixed_bounds_and_lower_gradients {U : Set AmnrSpace} (hU : IsOpen U) {μ : MeasureTheory.Measure AmnrSpace} (hμ : μ.AbsolutelyContinuous (MeasureTheory.volume.restrict U)) {b : AmnrSpace → Homogenization.Vec 2} {f : AmnrSpace → ℝ} {N cut : ℕ} (hb : ContDiff ℝ (↑⊤) b) (hf : ContDiffOn ℝ (↑N) f U) {S H G Cb : ℝ} (hS : 0 < S) (hH : 0 < H) (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))) (hbudget : amnrBudget w ≤ N) (hcut : amnrMaterialCount w ≤ cut) : MeasureTheory.eLpNorm (amnrWord b w f) 2 μ ≤ ENNReal.ofReal (amnrNormalOrderConstant N Cb N * ↑(amnrCanonicalSamples N cut).card * G * amnrWeight S H w)

Canonical L2 jets and source velocity-gradient jets control every ordered word at the same weighted budget and material level. The finite envelope is integrated after pointwise normal ordering, so no pointwise temperature bound is assumed.