: calculus helpers for the source material equation (local copies of the private lemmas of SourceMaterialEquation).

theorem AVenhance.Infra.Section5.LeftJacobian.vecDiv_add_of_differentiableAt {V W : Homogenization.Vec 2 → Homogenization.Vec 2} {x : Homogenization.Vec 2} (hV : DifferentiableAt ℝ V x) (hW : DifferentiableAt ℝ W x) : vecDiv (fun (y : Homogenization.Vec 2) => V y + W y) x = vecDiv V x + vecDiv W x

theorem AVenhance.Infra.Section5.LeftJacobian.vecDiv_add3_of_differentiableAt {U V W : Homogenization.Vec 2 → Homogenization.Vec 2} {x : Homogenization.Vec 2} (hU : DifferentiableAt ℝ U x) (hV : DifferentiableAt ℝ V x) (hW : DifferentiableAt ℝ W x) : vecDiv (fun (y : Homogenization.Vec 2) => U y + V y + W y) x = vecDiv U x + vecDiv V x + vecDiv W x

theorem AVenhance.Infra.Section5.LeftJacobian.stDiv_eq_vecDiv {F : ST → Homogenization.Vec 2} {t : ℝ} {x : Homogenization.Vec 2} (hF : DifferentiableAt ℝ F (t, x)) : stDiv F (t, x) = vecDiv (fun (y : Homogenization.Vec 2) => F (t, y)) x

noncomputable def AVenhance.Infra.Section5.LeftJacobian.terminalTail {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) : Homogenization.Vec 2 → Homogenization.Vec 2

The terminal A_{Jcut} q_{Jcut} tail of d.

Equations

• One or more equations did not get rendered due to their size.