Composed analyticity of the twistie1 slow factor

For ξ_{m,k}(t) ≠ 0 the slow factor f = ξ_{m,k} (∇X ∘ X⁻¹) ∇ ∇·(B ∇T) (component j, choice e.fg.choice.1) composed with the flow slice X = X_{m-1,l_k}(t) is analytic in L²(𝕋²) with amplitude C_f and radius r, in terms of the jets of the coefficient B = K_m + s_{m-1} and of the positive jets of T at the common rate L ≥ 2^{10}/ε_{m-1} (slowFactorChoice1_composed_bounds).

theorem AVenhance.Infra.Section5.Contracts.se_analyticL2_mono {f : Homogenization.Vec 2 → ℂ} {Cf r r' : ℝ} (hCf : 0 ≤ Cf) (hr' : 0 < r') (hrr : r' ≤ r) (h : Ergodic.HasCoordinateAnalyticL2Bounds f Cf r) : Ergodic.HasCoordinateAnalyticL2Bounds f Cf r'

Monotonicity of the analytic L² bounds in the radius.

theorem AVenhance.Infra.Section5.Contracts.se_slowFactorGradDiv_periodic {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) (hBper : IsZ2Periodic B) (hT : ContDiff ℝ (↑⊤) T) (hTper : IsZ2Periodic T) (i : Fin 2) : IsZ2Periodic (slowFactorGradDiv B T i)

Periodicity of ∇ ∇·(B ∇ T) (component i).

theorem AVenhance.Infra.Section5.Contracts.se_slowFactorChoice1_periodic {ξ : ℝ} {Q B : Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ} {T : Homogenization.Vec 2 → ℝ} (hQper : IsZ2Periodic Q) (hB : ∀ (i j : Fin 2), ContDiff ℝ ↑⊤ fun (x : Homogenization.Vec 2) => B x i j) (hBper : IsZ2Periodic B) (hT : ContDiff ℝ (↑⊤) T) (hTper : IsZ2Periodic T) (j : Fin 2) : Ergodic.IsZPeriodic (slowFactorChoice1 ξ Q B T j)

theorem AVenhance.Infra.Section5.Contracts.se_xFlow_hXb {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 2 ≤ m) (k : ℤ) {t : ℝ} (hξ : I.xiMK m k t ≠ 0) (n : ℕ) (w : Fin n → Fin 2) : 0 < n → ∀ (x : Homogenization.Vec 2) (j : Fin 2), |Ergodic.spatialJet n (LeftToShow.xFlowDiffeo I hΦ m (lIdx β I.Λ m k) t).toFun w x j| ≤ epsilon β I.Λ (m - 1) / 2 ^ 13 * ↑n.factorial * (2 ^ 14 / epsilon β I.Λ (m - 1)) ^ n

The derivative bound |∇ⁿ X| ≤ (ε/2^{13}) n! (2^{14}/ε)^n of the flow slice in the form required by the composition lemma.

theorem AVenhance.Infra.Section5.Contracts.se_choice1_analytic {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 2 ≤ m) (k : ℤ) {t : ℝ} (hξ : I.xiMK m k t ≠ 0) (hsmall : epsilon β I.Λ (m - 1) ^ (2 * delta β) ≤ 1) {B : Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ} (hB : ∀ (i j : Fin 2), ContDiff ℝ ↑⊤ fun (x : Homogenization.Vec 2) => B x i j) (hBper : IsZ2Periodic B) {T : Homogenization.Vec 2 → ℝ} (hT : ContDiff ℝ (↑⊤) T) (hTper : IsZ2Periodic T) {CB M L : ℝ} (hCB : 0 ≤ CB) (hM : 0 ≤ M) (hL : 2 ^ 10 / epsilon β I.Λ (m - 1) ≤ L) (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 (MeasureTheory.volume.restrict (Torus.unitCell 2)) ≤ ENNReal.ofReal (M * ↑w.length.factorial * L ^ w.length)) (j : Fin 2) : Ergodic.HasCoordinateAnalyticL2Bounds (fun (x : Homogenization.Vec 2) => ↑(slowFactorChoice1 (I.xiMK m k t) (I.flowGrad hΦ m (lIdx β I.Λ m k) t) B T j (I.xFlow hΦ m (lIdx β I.Λ m k) t x))) (2048 * 40 * CB * M * L ^ 3) ((16 * L)⁻¹ / 2 ^ 11)

Composed analyticity of the slow factor of twistie1 (e.fg.choice.1, e.checking.f.ergodic): the composition f ∘ X_{m-1,l_k}(t) has analytic L² bounds with amplitude 2048 · 40 · C_B M L³ and radius (16 L)⁻¹ / 2^{11}, from the jets of B and the positive jets of T at the rate L ≥ 2^{10}/ε_{m-1}.