One term of the twistie1 ergodic estimate

For ξ_{m,k}(t) ≠ 0 and a component j, the centered HDot⁻¹ norm of f_{k,j} · (χ_{m,k,j} ∘ X⁻¹_{m-1,l_k}) is bounded by the centered App C estimate centered_frozen_hMinusOneNorm_le_of_fastPeriodicProduct_flow with

• the fast factor g = χ_{m,k,j} (zero mean, fast periodic at N = ε_m⁻¹, |g| ≤ G_χ),
• the slow factor f = f_{k,j} (‖f‖_{L²(𝕋²)} ≤ 4 ‖∇ ∇·((K_m + s_{m-1}) ∇T)‖_{L²}),
• the composed analyticity se_choice1_analytic (amplitude C_f, radius r).

noncomputable def AVenhance.Infra.Section5.Contracts.seCE : ℝ

The absolute constant of the App C estimate.

Equations

• AVenhance.Infra.Section5.Contracts.seCE = 1 + 64 * AVenhance.Infra.Ergodic.ergodicFourierWeight 2 ^ (1 / 2) + 1024 * (2 + 1)

theorem AVenhance.Infra.Section5.Contracts.seCE_nonneg : 0 ≤ seCE

theorem AVenhance.Infra.Section5.Contracts.se_seGd_continuous {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) {T : ℝ → Homogenization.Vec 2 → ℝ} (t : ℝ) (hB : ∀ (i j : Fin 2), ContDiff ℝ ↑⊤ fun (x : Homogenization.Vec 2) => (I.Kmat κ m t + I.sMat hΦ m κ t x) i j) (hT : ContDiff ℝ (↑⊤) (T t)) : Continuous (seGd I hΦ m κ T t)

theorem AVenhance.Infra.Section5.Contracts.se_choice1_sq_le {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 2 ≤ m) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (k : ℤ) {t : ℝ} (hξ : I.xiMK m k t ≠ 0) (hsmall : epsilon β I.Λ (m - 1) ^ (2 * delta β) ≤ 1) (j : Fin 2) (x : Homogenization.Vec 2) : section5SlowChoice1 I hΦ m κ T k t j x ^ 2 ≤ 16 * Homogenization.vecNormSq (seGd I hΦ m κ T t x)

Pointwise: |f_{k,j}|² ≤ 16 |∇ ∇·(B ∇T)|².

theorem AVenhance.Infra.Section5.Contracts.se_choice1_smooth {ξ : ℝ} {Q B : 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) (hB : ∀ (i j : Fin 2), ContDiff ℝ ↑⊤ fun (x : Homogenization.Vec 2) => B x i j) (hT : ContDiff ℝ (↑⊤) T) (j : Fin 2) : ContDiff ℝ (↑⊤) (slowFactorChoice1 ξ Q B T j)

theorem AVenhance.Infra.Section5.Contracts.se_cellAverage_choice1_le {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 2 ≤ m) (κ : ℝ) {T : ℝ → Homogenization.Vec 2 → ℝ} (k : ℤ) {t : ℝ} (hξ : I.xiMK m k t ≠ 0) (hsmall : epsilon β I.Λ (m - 1) ^ (2 * delta β) ≤ 1) (hB : ∀ (i j : Fin 2), ContDiff ℝ ↑⊤ fun (x : Homogenization.Vec 2) => (I.Kmat κ m t + I.sMat hΦ m κ t x) i j) (hT : ContDiff ℝ (↑⊤) (T t)) (j : Fin 2) : (Ergodic.cellAverage fun (x : Homogenization.Vec 2) => |section5SlowChoice1 I hΦ m κ T k t j x| ^ 2) ≤ 16 * gradNormSq (seGd I hΦ m κ T t)

‖f_{k,j}‖²_{L²(𝕋²)} ≤ 16 ‖∇ ∇·(B ∇T)‖²_{L²(𝕋²)}.

theorem AVenhance.Infra.Section5.Contracts.se_term_bound {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 2 ≤ m) {κm : ℝ} (hκm : 0 < κm) (Tn : ℝ → Homogenization.Vec 2 → ℝ) {t : ℝ} (k : ℤ) (hξ : I.xiMK m k t ≠ 0) (hsmall : epsilon β I.Λ (m - 1) ^ (2 * delta β) ≤ 1 / 8) (hB : ∀ (i j : Fin 2), ContDiff ℝ ↑⊤ fun (x : Homogenization.Vec 2) => (I.Kmat κm m t + I.sMat hΦ m κm t x) i j) (hBper : IsZ2Periodic fun (x : Homogenization.Vec 2) => I.Kmat κm m t + I.sMat hΦ m κm t x) (hT : ContDiff ℝ (↑⊤) (Tn t)) (hTper : IsZ2Periodic (Tn 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) => (I.Kmat κm m t + I.sMat hΦ m κm t y) i j) x| ≤ CB * ↑w.length.factorial * L ^ w.length) (hTb : ∀ (w : List (Fin 2)), 0 < w.length → MeasureTheory.eLpNorm (Section4.amnrSpaceWord w (Tn t)) 2 (MeasureTheory.volume.restrict (Torus.unitCell 2)) ≤ ENNReal.ofReal (M * ↑w.length.factorial * L ^ w.length)) (hsep : 2 ≤ (16 * L)⁻¹ / 2 ^ 11 * ↑(ergodicFrequency β I.Λ m)) (j : Fin 2) : hMinusOneNorm (Ergodic.centerCell fun (x : Homogenization.Vec 2) => section5SlowChoice1 I hΦ m κm Tn k t j x * I.chiTilde hΦ m κm k t x j) ≤ ENNReal.ofReal (12 * (seCE / ↑(ergodicFrequency β I.Λ m) * (4 * √(gradNormSq (seGd I hΦ m κm Tn t))) * (epsilon β I.Λ m * (a β I.Λ m * epsilon β I.Λ m ^ 2 / κm)) + seCE * (2048 * 40 * CB * M * L ^ 3) * (epsilon β I.Λ m * (a β I.Λ m * epsilon β I.Λ m ^ 2 / κm)) * Real.exp (-((16 * L)⁻¹ / 2 ^ 11) * ↑(ergodicFrequency β I.Λ m) / 4096)))

One term of the centered ergodic estimate.

theorem AVenhance.Infra.Section5.Contracts.se_slice_hMinus {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 2 ≤ m) {κm : ℝ} (hκm : 0 < κm) (Tn : ℝ → Homogenization.Vec 2 → ℝ) {t : ℝ} (hmean : Homogenization.MeanZeroOn unitCube (twistie1 I hΦ m κm Tn t)) (hsmall : epsilon β I.Λ (m - 1) ^ (2 * delta β) ≤ 1 / 8) (hB : ∀ (i j : Fin 2), ContDiff ℝ ↑⊤ fun (x : Homogenization.Vec 2) => (I.Kmat κm m t + I.sMat hΦ m κm t x) i j) (hBper : IsZ2Periodic fun (x : Homogenization.Vec 2) => I.Kmat κm m t + I.sMat hΦ m κm t x) (hT : ContDiff ℝ (↑⊤) (Tn t)) (hTper : IsZ2Periodic (Tn 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) => (I.Kmat κm m t + I.sMat hΦ m κm t y) i j) x| ≤ CB * ↑w.length.factorial * L ^ w.length) (hTb : ∀ (w : List (Fin 2)), 0 < w.length → MeasureTheory.eLpNorm (Section4.amnrSpaceWord w (Tn t)) 2 (MeasureTheory.volume.restrict (Torus.unitCell 2)) ≤ ENNReal.ofReal (M * ↑w.length.factorial * L ^ w.length)) (hsep : 2 ≤ (16 * L)⁻¹ / 2 ^ 11 * ↑(ergodicFrequency β I.Λ m)) : hMinusOneNorm (twistie1 I hΦ m κm Tn t) ≤ ENNReal.ofReal (72 * (seCE / ↑(ergodicFrequency β I.Λ m) * (4 * √(gradNormSq (seGd I hΦ m κm Tn t))) * (epsilon β I.Λ m * (a β I.Λ m * epsilon β I.Λ m ^ 2 / κm)) + seCE * (2048 * 40 * CB * M * L ^ 3) * (epsilon β I.Λ m * (a β I.Λ m * epsilon β I.Λ m ^ 2 / κm)) * Real.exp (-((16 * L)⁻¹ / 2 ^ 11) * ↑(ergodicFrequency β I.Λ m) / 4096)))

Slice estimate. At a time t where twistie1(t) has mean zero, its HDot⁻¹ norm is bounded by the sum over the (at most six) pairs (k, j) of the centered App C estimates.