Concrete differentiated coefficient-gradient products in the four slow factors. Matrix rows are derivative coordinates, as in the gradMatrix.

noncomputable def AVenhance.Infra.Section5.slowFactorG (Q : Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ) (T : Homogenization.Vec 2 → ℝ) (j : Fin 2) : Homogenization.Vec 2 → ℝ

Component of Q grad T, with the derivative-row matrix convention.

Equations

• AVenhance.Infra.Section5.slowFactorG Q T j = ∑ k : Fin 2, (fun (x : Homogenization.Vec 2) => Q x j k) * AVenhance.Infra.Section4.amnrSpaceWord [k] T

noncomputable def AVenhance.Infra.Section5.slowFactorH (Q : Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ) (T : Homogenization.Vec 2 → ℝ) (i j : Fin 2) : Homogenization.Vec 2 → ℝ

The (i,j) entry of grad(Q grad T).

Equations

• AVenhance.Infra.Section5.slowFactorH Q T i j = AVenhance.Infra.Section4.amnrSpaceWord [i] (AVenhance.Infra.Section5.slowFactorG Q T j)

noncomputable def AVenhance.Infra.Section5.slowFactorDiv (B : Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ) (T : Homogenization.Vec 2 → ℝ) : Homogenization.Vec 2 → ℝ

Component of the divergence of B grad T.

Equations

• AVenhance.Infra.Section5.slowFactorDiv B T = ∑ j : Fin 2, AVenhance.Infra.Section4.amnrSpaceWord [j] (AVenhance.Infra.Section5.slowFactorG B T j)

noncomputable def AVenhance.Infra.Section5.slowFactorGradDiv (B : Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ) (T : Homogenization.Vec 2 → ℝ) (i : Fin 2) : Homogenization.Vec 2 → ℝ

Component of grad div(B grad T), whose T factor always has positive order.

Equations

• AVenhance.Infra.Section5.slowFactorGradDiv B T i = AVenhance.Infra.Section4.amnrSpaceWord [i] (AVenhance.Infra.Section5.slowFactorDiv B T)

theorem AVenhance.Infra.Section5.slowFactorG_word_bound {Q : Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ} {T : Homogenization.Vec 2 → ℝ} (hQ : ∀ (i j : Fin 2), ContDiff ℝ ↑⊤ fun (x : Homogenization.Vec 2) => Q x i j) (hT : ContDiff ℝ (↑⊤) T) {CQ M L : ℝ} (hCQ : 0 ≤ CQ) (hM : 0 ≤ M) (hL : 0 ≤ L) (μ : MeasureTheory.Measure (Homogenization.Vec 2)) (hQb : ∀ (i j : Fin 2) (w : List (Fin 2)) (x : Homogenization.Vec 2), |Section4.amnrSpaceWord w (fun (y : Homogenization.Vec 2) => Q y i j) x| ≤ CQ * ↑w.length.factorial * L ^ w.length) (hTb : ∀ (w : List (Fin 2)), 0 < w.length → MeasureTheory.eLpNorm (Section4.amnrSpaceWord w T) 2 μ ≤ ENNReal.ofReal (M * ↑w.length.factorial * L ^ w.length)) (j : Fin 2) (w : List (Fin 2)) : MeasureTheory.eLpNorm (Section4.amnrSpaceWord w (slowFactorG Q T j)) 2 μ ≤ ENNReal.ofReal (4 * CQ * M * L * ↑w.length.factorial * (4 * L) ^ w.length)

Q grad T is analytic in the averaged norm from positive T jets alone.

theorem AVenhance.Infra.Section5.slowFactorG_smooth {Q : Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ} {T : Homogenization.Vec 2 → ℝ} (hQ : ∀ (i j : Fin 2), ContDiff ℝ ↑⊤ fun (x : Homogenization.Vec 2) => Q x i j) (hT : ContDiff ℝ (↑⊤) T) (j : Fin 2) : ContDiff ℝ (↑⊤) (slowFactorG Q T j)

theorem AVenhance.Infra.Section5.slowFactorH_word_bound {Q : Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ} {T : Homogenization.Vec 2 → ℝ} (hQ : ∀ (i j : Fin 2), ContDiff ℝ ↑⊤ fun (x : Homogenization.Vec 2) => Q x i j) (hT : ContDiff ℝ (↑⊤) T) {CQ M L : ℝ} (hCQ : 0 ≤ CQ) (hM : 0 ≤ M) (hL : 0 ≤ L) (μ : MeasureTheory.Measure (Homogenization.Vec 2)) (hQb : ∀ (i j : Fin 2) (w : List (Fin 2)) (x : Homogenization.Vec 2), |Section4.amnrSpaceWord w (fun (y : Homogenization.Vec 2) => Q y i j) x| ≤ CQ * ↑w.length.factorial * L ^ w.length) (hTb : ∀ (w : List (Fin 2)), 0 < w.length → MeasureTheory.eLpNorm (Section4.amnrSpaceWord w T) 2 μ ≤ ENNReal.ofReal (M * ↑w.length.factorial * L ^ w.length)) (i j : Fin 2) (w : List (Fin 2)) : MeasureTheory.eLpNorm (Section4.amnrSpaceWord w (slowFactorH Q T i j)) 2 μ ≤ ENNReal.ofReal (32 * CQ * M * L ^ 2 * ↑w.length.factorial * (8 * L) ^ w.length)

Actual all-order Hessian-factor bound, including its order-zero case.

theorem AVenhance.Infra.Section5.slowFactorGradDiv_word_bound {B : Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ} {T : Homogenization.Vec 2 → ℝ} (hB : ∀ (i j : Fin 2), ContDiff ℝ ↑⊤ fun (x : Homogenization.Vec 2) => B x i j) (hT : ContDiff ℝ (↑⊤) T) {CB M L : ℝ} (hCB : 0 ≤ CB) (hM : 0 ≤ M) (hL : 0 ≤ L) (μ : MeasureTheory.Measure (Homogenization.Vec 2)) (hBb : ∀ (i j : Fin 2) (w : List (Fin 2)) (x : Homogenization.Vec 2), |Section4.amnrSpaceWord w (fun (y : Homogenization.Vec 2) => B y i j) x| ≤ CB * ↑w.length.factorial * L ^ w.length) (hTb : ∀ (w : List (Fin 2)), 0 < w.length → MeasureTheory.eLpNorm (Section4.amnrSpaceWord w T) 2 μ ≤ ENNReal.ofReal (M * ↑w.length.factorial * L ^ w.length)) (i : Fin 2) (w : List (Fin 2)) : MeasureTheory.eLpNorm (Section4.amnrSpaceWord w (slowFactorGradDiv B T i)) 2 μ ≤ ENNReal.ofReal (1024 * CB * M * L ^ 3 * ↑w.length.factorial * (8 * L) ^ w.length)

The differentiated divergence needs no zeroth T estimate.