Proved composed analytic inputs for all four slow factors. The order-zero bound is obtained from the same positive-T-jet calculation as every other order.
theorem
AVenhance.Infra.Section5.slowFactorH_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)
(i j : Fin 2)
:
ContDiff ℝ (↑⊤) (slowFactorH Q T i j)
theorem
AVenhance.Infra.Section5.slowFactorGradDiv_smooth
{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)
(i : Fin 2)
:
ContDiff ℝ (↑⊤) (slowFactorGradDiv B T i)
theorem
AVenhance.Infra.Section5.slowFactorContractH_smooth
{A Q : Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ}
{T : Homogenization.Vec 2 → ℝ}
(hA : ∀ (i j : Fin 2), ContDiff ℝ ↑⊤ fun (x : Homogenization.Vec 2) => A x i j)
(hQ : ∀ (i j : Fin 2), ContDiff ℝ ↑⊤ fun (x : Homogenization.Vec 2) => Q x i j)
(hT : ContDiff ℝ (↑⊤) T)
(a j : Fin 2)
:
ContDiff ℝ (↑⊤) (slowFactorContractH A Q T a j)
theorem
AVenhance.Infra.Section5.slowFactorChoice1_composed_bounds
(X : Ergodic.PeriodicVolumePreservingDiffeomorphism 2)
{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 CX R : ℝ}
(hCQ : 0 ≤ CQ)
(hM : 0 ≤ M)
(hL : 0 < L)
(hCX : 0 < CX)
(hR : 0 < R)
(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 (MeasureTheory.volume.restrict (Torus.unitCell 2)) ≤ ENNReal.ofReal (M * ↑w.length.factorial * L ^ w.length))
(hXb :
∀ (n : ℕ) (w : Fin n → Fin 2),
0 < n → ∀ (x : Homogenization.Vec 2) (j : Fin 2), |Ergodic.spatialJet n X.toFun w x j| ≤ CX * ↑n.factorial * R ^ n)
{B : Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ}
(hB : ∀ (i j : Fin 2), ContDiff ℝ ↑⊤ fun (x : Homogenization.Vec 2) => B x i j)
{CB ξ : ℝ}
(hCB : 0 ≤ CB)
(hξ : |ξ| ≤ 1)
(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)
(j : Fin 2)
(hper : Ergodic.IsZPeriodic (slowFactorChoice1 ξ Q B T j))
:
theorem
AVenhance.Infra.Section5.slowFactorChoice3_composed_bounds
(X : Ergodic.PeriodicVolumePreservingDiffeomorphism 2)
{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 CX R : ℝ}
(hCQ : 0 ≤ CQ)
(hM : 0 ≤ M)
(hL : 0 < L)
(hCX : 0 < CX)
(hR : 0 < R)
(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 (MeasureTheory.volume.restrict (Torus.unitCell 2)) ≤ ENNReal.ofReal (M * ↑w.length.factorial * L ^ w.length))
(hXb :
∀ (n : ℕ) (w : Fin n → Fin 2),
0 < n → ∀ (x : Homogenization.Vec 2) (j : Fin 2), |Ergodic.spatialJet n X.toFun w x j| ≤ CX * ↑n.factorial * R ^ n)
{Y : Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ}
(hY : ∀ (i j : Fin 2), ContDiff ℝ ↑⊤ fun (x : Homogenization.Vec 2) => Y x i j)
{CY ξ : ℝ}
(hCY : 0 ≤ CY)
(hξ : |ξ| ≤ 1)
(hYb :
∀ (i j : Fin 2) (w : List (Fin 2)) (x : Homogenization.Vec 2),
|Section4.amnrSpaceWord w (fun (y : Homogenization.Vec 2) => Y y i j) x| ≤ CY * ↑w.length.factorial * L ^ w.length)
(a j : Fin 2)
(hper : Ergodic.IsZPeriodic (slowFactorChoice3 ξ Y Q T a j))
: