VelGradContract: the gradient of the stream drift is O(ε_m^{β-2})

∂_j (streamVel (Φ_m))_i = ± ∂_j ∂_{i'} Φ_m, and Φ_m = ∑_{k ≤ m} increments, whose second derivatives are ≲ ε_k^{β-2} (stream-regularity estimates). The scales ε_k^{β-2} grow geometrically with ratio at least 128^{2-β}, so the sum is ≲ ε_m^{β-2}.

noncomputable def AVenhance.Infra.FullTheorem.NoSelectionInputs.hess2 (f : Homogenization.Vec 2 → ℝ) (i j : Fin 2) (x : Homogenization.Vec 2) : ℝ

Second derivative ∂_j ∂_i f.

Equations

• AVenhance.Infra.FullTheorem.NoSelectionInputs.hess2 f i j x = (fderiv ℝ (fun (y : Homogenization.Vec 2) => (fderiv ℝ f y) (Homogenization.basisVec i)) x) (Homogenization.basisVec j)

theorem AVenhance.Infra.FullTheorem.NoSelectionInputs.hess2_add {f g : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (i j : Fin 2) (x : Homogenization.Vec 2) : hess2 (f + g) i j x = hess2 f i j x + hess2 g i j x

theorem AVenhance.Infra.FullTheorem.NoSelectionInputs.hess2_eq_iterated {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (i j : Fin 2) (x : Homogenization.Vec 2) : hess2 f i j x = (iteratedFDeriv ℝ 2 f x) fun (k : Fin 2) => Homogenization.basisVec (if k = 0 then j else i)

theorem AVenhance.Infra.FullTheorem.NoSelectionInputs.slice_contDiff {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hseq : IsStreamSeq I Φ) (m : ℕ) (t : ℝ) : ContDiff ℝ (↑⊤) (Φ m t)

theorem AVenhance.Infra.FullTheorem.NoSelectionInputs.hess2_increment_le {β C : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hseq : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) {m : ℕ} (hm : 1 ≤ m) (t : ℝ) (x : Homogenization.Vec 2) (i j : Fin 2) : |hess2 (Φ m t - Φ (m - 1) t) i j x| ≤ 2 ^ 16 * epsilon β I.Λ m ^ (β - 2)

Second derivative of an increment.

theorem AVenhance.Infra.FullTheorem.NoSelectionInputs.inv_step {a b q : ℝ} (ha : 0 < a) (hb : 0 < b) (h : b ≤ a * q) : a⁻¹ ≤ q * b⁻¹

Abstract inversion step.

theorem AVenhance.Infra.FullTheorem.NoSelectionInputs.eps_neg_step {β : ℝ} (I : Ingredients β) (m : ℕ) : epsilon β I.Λ m ^ (β - 2) ≤ ↑I.Λ ^ (-(2 - β)) * epsilon β I.Λ (m + 1) ^ (β - 2)

theorem AVenhance.Infra.FullTheorem.NoSelectionInputs.hess2_partial_le {β C : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hseq : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) {c q : ℝ} (hq1 : q < 1) (hqΛ : ↑I.Λ ^ (-(2 - β)) ≤ q) (hc : 2 ^ 16 ≤ c * (1 - q)) (t : ℝ) (x : Homogenization.Vec 2) (i j : Fin 2) (n : ℕ) : |hess2 (Φ n t) i j x| ≤ c * epsilon β I.Λ n ^ (β - 2)

Partial sums of the Hessian.

theorem AVenhance.Infra.FullTheorem.NoSelectionInputs.abs_spaceGrad_streamVel_le {ψ : ℝ → Homogenization.Vec 2 → ℝ} (t : ℝ) {B : ℝ} (hB : ∀ (a b : Fin 2) (x : Homogenization.Vec 2), |hess2 (ψ t) a b x| ≤ B) (x : Homogenization.Vec 2) (i j : Fin 2) : |spaceGrad (fun (y : Homogenization.Vec 2) => streamVel ψ t y i) x j| ≤ B

theorem AVenhance.Infra.FullTheorem.NoSelectionInputs.velGrad (β C₀ : ℝ) : VelGradContract β C₀