One material level from lower canonical gradient and flux jets.

theorem AVenhance.Infra.Section4.amnr_gradient_material_step_L2 {U : Set AmnrSpace} (hU : IsOpen U) {μ : MeasureTheory.Measure AmnrSpace} (hμ : μ.AbsolutelyContinuous (MeasureTheory.volume.restrict U)) {b : AmnrSpace → Homogenization.Vec 2} (hb : ContDiff ℝ (↑⊤) b) {g F : Fin 2 → AmnrSpace → ℝ} (hg : ∀ (p : Fin 2), ContDiffOn ℝ (↑⊤) (g p) U) {N r : ℕ} (hF : ∀ (q : Fin 2), ContDiffOn ℝ (↑N) (F q) U) {κ S H G GF Cb : ℝ} (hκ : 0 ≤ κ) (hS : 0 < S) (hH : 0 < H) (hG : 0 ≤ G) (hGF : 0 ≤ GF) (hCb : 0 ≤ Cb) (hgb : ∀ (p : Fin 2) (α : List (Fin 2)) (n : ℕ), α.length + 2 * n ≤ N → n ≤ r → MeasureTheory.eLpNorm (amnrWord b (amnrMixedWord α n) (g p)) 2 μ ≤ ENNReal.ofReal (G * amnrWeight S H (amnrMixedWord α n))) (hFb : ∀ (q : Fin 2) (α : List (Fin 2)) (n : ℕ), α.length + 2 * n ≤ N → n ≤ r → MeasureTheory.eLpNorm (amnrWord b (amnrMixedWord α n) (F q)) 2 μ ≤ ENNReal.ofReal (GF * amnrWeight S H (amnrMixedWord α n))) (hBb : ∀ (q p : Fin 2) (α : List (Fin 2)) (n : ℕ), α.length + 2 * n + 2 ≤ N → ∀ z ∈ U, |amnrWord b (amnrMixedWord α n) (amnrVelocityGradient b q p) z| ≤ Cb * H * amnrWeight S H (amnrMixedWord α n)) (p : Fin 2) (hEq : Set.EqOn (amnrOp b none (g p)) (fun (z : AmnrSpace) => κ * ∑ q : Fin 2, amnrWord b [some q, some q] (g p) z + ∑ q : Fin 2, amnrWord b [some p, some q] (F q) z - ∑ q : Fin 2, amnrVelocityGradient b q p z * g q z) U) (α : List (Fin 2)) (hbudget : α.length + 2 * (r + 1) ≤ N) : MeasureTheory.eLpNorm (amnrWord b (amnrMixedWord α (r + 1)) (g p)) 2 μ ≤ ENNReal.ofReal (((2 * κ * amnrNormalOrderConstant N Cb N * ↑(amnrCanonicalSamples N N).card * G + 2 * amnrNormalOrderConstant N Cb N * ↑(amnrCanonicalSamples N N).card * GF) * S ^ 2 + 2 ^ (N + 1) * Cb * H * G) * amnrWeight S H (amnrMixedWord α r))