Coefficient jets of the e_{m-1} matrix (e.monster.est.tiny)

The matrix B_t(y) = K_m(t) - κ_{m-1} I + s_{m-1}(t, y) multiplying ∇(T_{N*-1} - T_{N*}) in iterateError has all spatial jets bounded by κ_{m-1} C_B · n! · (2^{10} ε_{m-1}^{-1} ε_{m-1}^{-2δ})^n.

This is the first conjunct of iterate_TForcing_profiles_from_flow (Section4), reproduced without its (here unneeded) mean hypothesis hmean, with the flow interfaces discharged by the unconditional flow bounds iterate_flowGrad_zero_bound / iterate_flowGrad_word_bound, and |K_m| ≤ K κ_{m-1} from iterate_chain_upgrade_inputs.

theorem AVenhance.Infra.Section5.Contracts.sc_coeff_profile_of_flow {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) {κm κprev K Cflow r₀ ρ : ℝ} (hκ : 0 ≤ κprev) (hK : 0 ≤ K) (hCf : 0 ≤ Cflow) (hr : 0 ≤ r₀) (hρ : 0 < ρ) (hρ1 : ρ ≤ 1) (hflow : ∀ (t : ℝ) (l : ℤ), ContDiff ℝ (↑⊤) (I.flowGrad hΦ m l t)) (hKm : ∀ (t : ℝ) (j k : Fin 2), |I.Kmat κm m t j k| ≤ K * κprev) (hκscale : |κm| ≤ κprev) (hrad1 : 1 ≤ r₀ / ρ) (hzero : ∀ (t : ℝ) (x : Homogenization.Vec 2) (l : ℤ), I.hatXiML m l t ≠ 0 → ∀ (j k : Fin 2), |(I.flowGrad hΦ m l t x - 1) j k| ≤ Cflow * ρ) (hpositive : ∀ (t : ℝ) (x : Homogenization.Vec 2) (l : ℤ), I.hatXiML m l t ≠ 0 → ∀ (p : List (Fin 2)), 1 ≤ p.length → ∀ (j k : Fin 2), |Section4.iterateSpatialWord p (fun (y : Homogenization.Vec 2) => (I.flowGrad hΦ m l t y - 1) j k) x| ≤ Cflow * ↑p.length.factorial * r₀ ^ p.length) (t : ℝ) (x : Homogenization.Vec 2) (p : List (Fin 2)) (j k : Fin 2) : |Section4.iterateMatrixWord (fun (y : Homogenization.Vec 2) => I.Kmat κm m t - κprev • 1 + I.sMat hΦ m κm t y) p x j k| ≤ κprev * (K + 1 + (2 * K * Cflow + 4 * (K + 1) * Cflow * (Cflow + 1))) * ↑p.length.factorial * (2 * (r₀ / ρ)) ^ p.length

First conjunct of iterate_TForcing_profiles_from_flow, with no mean hypothesis.

theorem AVenhance.Infra.Section5.Contracts.sc_coeff_profile (β C₀ : ℝ) : ∃ (CB : ℝ), 0 ≤ CB ∧ ∃ (C₁ : ℝ), ∀ (I : Ingredients β), I.Czeta ≤ C₀ → I.Cxi ≤ C₀ → I.Chat ≤ C₀ → C₁ ≤ ↑I.Λ → ∀ (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (hΦ : IsStreamSeq I Φ), ∀ κ ∈ permissibleSet β I.Λ, ∀ (M : ℕ), 1 ≤ M → κ ∈ permittedInterval β I.Λ M → ∀ (m : ℕ), 2 ≤ m → m ≤ M → ∀ (t : ℝ) (x : Homogenization.Vec 2) (p : List (Fin 2)) (j k : Fin 2), |Section4.iterateMatrixWord (fun (y : Homogenization.Vec 2) => I.Kmat (I.kappaSeq κ M m) m t - I.kappaSeq κ M (m - 1) • 1 + I.sMat hΦ m (I.kappaSeq κ M m) t y) p x j k| ≤ I.kappaSeq κ M (m - 1) * CB * ↑p.length.factorial * (2 * (2 ^ 10 / epsilon β I.Λ (m - 1) / epsilon β I.Λ (m - 1) ^ (2 * delta β))) ^ p.length

Coefficient jets of the matrix of iterateError, with constants chosen before I.