Temperature, flow and cutoff inputs of the composed slow-factor bounds

• ξ_{m,k} is bounded by one;
• PositiveTemperatureJets give the L²(unitCell) word bounds of T t;
• the Section 2 derivative bounds of the flow slice give the pointwise coordinate-jet bounds of X.toFun (through the normalized seminorm snorm).

theorem AVenhance.Infra.Section5.Contracts.sdi_xiMK_abs_le_one {β : ℝ} (I : Ingredients β) (m : ℕ) (k : ℤ) (t : ℝ) : |I.xiMK m k t| ≤ 1

Temperature

theorem AVenhance.Infra.Section5.Contracts.sdi_T_word_bound {A ρ S : ℝ} {T : ℝ → Homogenization.Vec 2 → ℝ} (hJets : RelativeError.PositiveTemperatureJets A ρ S T) (hA : 0 ≤ A) (hρ : 0 < ρ) (hS : 0 ≤ S) {L : ℝ} (hL : A / ρ ≤ L) {t : ℝ} (ht : t ∈ Set.Icc 0 1) (hTt : ContDiff ℝ (↑⊤) (T t)) (w : List (Fin 2)) (hw : 0 < w.length) : MeasureTheory.eLpNorm (Section4.amnrSpaceWord w (T t)) 2 (MeasureTheory.volume.restrict (Torus.unitCell 2)) ≤ ENNReal.ofReal (A * S * ↑w.length.factorial * L ^ w.length)

Positive temperature jets give the L²(unitCell) word bounds of T t.

Flow slice

theorem AVenhance.Infra.Section5.Contracts.sdi_orderedPartial_eq_iteratedFDeriv {n : ℕ} {f : Homogenization.Vec 2 → Homogenization.Vec 2} (hf : ContDiff ℝ (↑⊤) f) (x : Homogenization.Vec 2) (J : Fin n → Fin 2) : FaaDiBruno.orderedPartial n f x J = (iteratedFDeriv ℝ n f x) fun (j : Fin n) => Homogenization.basisVec (J j)

theorem AVenhance.Infra.Section5.Contracts.sdi_xFlow_jet_bound {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 2 ≤ m) (k : ℤ) {t : ℝ} (ht : t ∈ Set.Ioo 0 1) (hξ : I.xiMK m k t ≠ 0) {K : ℝ} (hK : ∀ (n : ℕ), (↑n + 3) ^ 5 ≤ K * 2 ^ n) (n : ℕ) (w : Fin n → Fin 2) (hn : 0 < n) (x : Homogenization.Vec 2) (j : Fin 2) : |Ergodic.spatialJet n (I.xFlow hΦ m (lIdx β I.Λ m k) t) w x j| ≤ K * epsilon β I.Λ (m - 1) * ↑n.factorial * (2 * 2 ^ 14 / epsilon β I.Λ (m - 1)) ^ n

Pointwise coordinate-jet bounds of the flow slice on supp ξ_{m,k}: |∂^w X_j| ≤ K ε · n! · (2·2^14/ε)^n (e.flow.for.ergodic).