Composed analyticity of the slow factor of normie3 #
n3Slow_{pj} = slowFactorChoice3 ξ_k Y F (T t) p j with Y = Fᵀ (the transpose of the flow
Jacobian, not 1 - Fᵀ), so the choice-3 composed bound of SlowFactorBoundsComposition
applies with the word bound 41 of the entries of Q = F (sdj_Q_word).
theorem
AVenhance.Infra.Section5.Contracts.n3Slow_eq_choice3
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
(m : ℕ)
(T : ℝ → Homogenization.Vec 2 → ℝ)
(k : ℤ)
(t : ℝ)
(hT : ContDiff ℝ (↑⊤) (T t))
(p j : Fin 2)
:
theorem
AVenhance.Infra.Section5.Contracts.n3c_core
{β : ℝ}
(A : ℝ)
(hA : 1 ≤ A)
{K : ℝ}
(hK1 : 1 ≤ K)
(hK : ∀ (n : ℕ), (↑n + 3) ^ 5 ≤ K * 2 ^ n)
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
{m : ℕ}
(hm : 2 ≤ m)
{S : ℝ}
(hS : 0 ≤ S)
(T : ℝ → Homogenization.Vec 2 → ℝ)
(hJets : RelativeError.PositiveTemperatureJets A (epsilon β I.Λ (m - 1) ^ (1 + gamma β / 2)) S T)
(hTs : ∀ (t : ℝ), 0 ≤ t → ContDiff ℝ (↑⊤) (T t))
(hTp : ∀ (t : ℝ), 0 ≤ t → IsZ2Periodic (T t))
{t : ℝ}
(ht : t ∈ Set.Ioo 0 1)
{k : ℤ}
(hξ : I.xiMK m k t ≠ 0)
(p j : Fin 2)
:
Ergodic.HasCoordinateAnalyticL2Bounds
(fun (x : Homogenization.Vec 2) => ↑(n3Slow I hΦ m T k t p j (I.xFlow hΦ m (lIdx β I.Λ m k) t x)))
(64 * 41 * 41 * A * max A (2 ^ 14) ^ 2 * S * ((epsilon β I.Λ (m - 1) ^ (1 + gamma β / 2)) ^ 2)⁻¹)
(epsilon β I.Λ (m - 1) ^ (1 + gamma β / 2) / (2 * 2 ^ 14 * 33 * K * max A (2 ^ 14)))
The core of n3_slow_composed_bounds, with the constants explicit. Here A₁ = max A 2^14,
K is the absolute polynomial-versus-exponential constant.
theorem
AVenhance.Infra.Section5.Contracts.n3_slow_composed_bounds
(β A : ℝ)
(hA : 1 ≤ A)
:
∃ (c₁ : ℝ) (c₂ : ℝ),
0 < c₁ ∧ 0 < c₂ ∧ ∀ (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ},
2 ≤ m →
∀ {S : ℝ},
0 ≤ S →
∀ (T : ℝ → Homogenization.Vec 2 → ℝ),
RelativeError.PositiveTemperatureJets A (epsilon β I.Λ (m - 1) ^ (1 + gamma β / 2)) S T →
(∀ (t : ℝ), 0 ≤ t → ContDiff ℝ (↑⊤) (T t)) →
(∀ (t : ℝ), 0 ≤ t → IsZ2Periodic (T t)) →
epsilon β I.Λ (m - 1) ^ (2 * delta β) ≤ 1 / 4 →
∀ {t : ℝ},
t ∈ Set.Ioo 0 1 →
∀ {k : ℤ},
I.xiMK m k t ≠ 0 →
∀ (p j : Fin 2),
Ergodic.HasCoordinateAnalyticL2Bounds
(fun (x : Homogenization.Vec 2) =>
↑(n3Slow I hΦ m T k t p j (I.xFlow hΦ m (lIdx β I.Λ m k) t x)))
(c₁ * S * ((epsilon β I.Λ (m - 1) ^ (1 + gamma β / 2)) ^ 2)⁻¹)
(epsilon β I.Λ (m - 1) ^ (1 + gamma β / 2) / c₂)
Composed analyticity of the slow factor of normie3 on supp ξ_{m,k}. The constants
depend only on the jet constant A and β.