source endpoint potentials and the finite H_m telescope.

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

The endpoint flux potential at order r, namely div Σ_n A_{m,n,r} q_{m,n,r}.

Equations

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

theorem AVenhance.Infra.Section5.frozen_hm_material_telescope {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (t : ℝ) (x : Homogenization.Vec 2) (Dt : ℕ → ℝ) (LH : ℕ → Homogenization.Vec 2 →L[ℝ] ℝ) (hDt : ∀ r ∈ Finset.range (Jcut β), HasDerivAt (fun (s : ℝ) => I.Hmr hΦ m κ T r s x) (Dt r) t) (hDx : ∀ r ∈ Finset.range (Jcut β), HasFDerivAt (I.Hmr hΦ m κ T r t) (LH r) x) (hstep : ∀ r ∈ Finset.range (Jcut β), Dt r + (LH r) (b t x) = hmEndpoint I hΦ m κ T (r + 1) t x - hmEndpoint I hΦ m κ T r t x) : deriv (fun (s : ℝ) => I.Hm hΦ m κ T s x) t + (fderiv ℝ (I.Hm hΦ m κ T t) x) (b t x) = hmEndpoint I hΦ m κ T (Jcut β) t x - hmEndpoint I hΦ m κ T 0 t x

The sum for H_m telescopes to its endpoint potentials once the source-specific per-index A/q transport rule is proved. The rule hstep is the remaining analytic input; this wrapper only performs the finite sum differentiation and telescope.