Source-generic ansatz material equation (corrected form).

The right-hand side of the source transport equation is an arbitrary real Src; nothing about the flux form of the source is used. The proof is a copy of frozen_ansatz_material_equation_of_source with the hsource' split dropped.

theorem AVenhance.Infra.Section5.LeftJacobian.AnsatzMaterial.vecDot_spaceGrad_eq_fderiv {f : Homogenization.Vec 2 → ℝ} {x : Homogenization.Vec 2} (v : Homogenization.Vec 2) : Homogenization.vecDot v (spaceGrad f x) = (fderiv ℝ f x) v

theorem AVenhance.Infra.Section5.LeftJacobian.AnsatzMaterial.jointVector_time_component {F : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {L : ℝ × Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2} {t : ℝ} {x : Homogenization.Vec 2} (hF : HasFDerivAt (Function.uncurry F) L (t, x)) (j : Fin 2) : HasDerivAt (fun (s : ℝ) => F s x j) (L (1, 0) j) t

theorem AVenhance.Infra.Section5.LeftJacobian.AnsatzMaterial.jointVector_space {F : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {L : ℝ × Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2} {t : ℝ} {x : Homogenization.Vec 2} (hF : HasFDerivAt (Function.uncurry F) L (t, x)) : HasFDerivAt (F t) (L ∘SL ContinuousLinearMap.prod 0 (ContinuousLinearMap.id ℝ (Homogenization.Vec 2))) x

theorem AVenhance.Infra.Section5.LeftJacobian.AnsatzMaterial.chiMK_zero_of_not_odd {β : ℝ} (I : Ingredients β) (κ : ℝ) (m : ℕ) (k : ℤ) (t : ℝ) (hk : ¬Odd k) : I.chiMK κ m k t = fun (x : Homogenization.Vec 2) => 0

theorem AVenhance.Infra.Section5.LeftJacobian.AnsatzMaterial.chiTilde_zero_of_not_odd {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (k : ℤ) (t : ℝ) (hk : ¬Odd k) : I.chiTilde hΦ m κ k t = fun (x : Homogenization.Vec 2) => 0

theorem AVenhance.Infra.Section5.LeftJacobian.AnsatzMaterial.xiMK_deriv_zero_off_nearSupport {β : ℝ} (I : Ingredients β) (m : ℕ) (t ρ : ℝ) (hρ : 0 < ρ) (k : ℤ) (hk : k ∉ xiMKNearSupportFinset I m t ρ) : deriv (I.xiMK m k) t = 0

theorem AVenhance.Infra.Section5.LeftJacobian.AnsatzMaterial.finite_odd_sum_eq_tsum {S : Finset ℤ} (F : { k : ℤ // Odd k } → ℝ) (hzero : ∀ (q : { k : ℤ // Odd k }), ↑q ∉ S → F q = 0) : (have f := fun (k : ℤ) => if hk : Odd k then F ⟨k, hk⟩ else 0; ∑ k ∈ S with Odd k, f k) = ∑' (q : { k : ℤ // Odd k }), F q

theorem AVenhance.Infra.Section5.LeftJacobian.AnsatzMaterial.near_sum_eq_active_odd_support {β : ℝ} (I : Ingredients β) (m : ℕ) (hm : 1 ≤ m) (t ρ : ℝ) (hρ : 0 < ρ) (F : ℤ → ℝ) (hEven : ∀ (k : ℤ), ¬Odd k → F k = 0) : ∑ k ∈ xiMKNearSupportFinset I m t ρ, I.xiMK m k t * F k = ∑ q ∈ ⋯.toFinset, I.xiMK m (↑q) t * F ↑q

theorem AVenhance.Infra.Section5.LeftJacobian.variantA_ansatz_material_equation_of_source {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (hm : 1 ≤ m) (κm κprev : ℝ) (θ₀ : Homogenization.Vec 2 → ℝ) (θprev : ℝ → Homogenization.Vec 2 → ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (hT : I.IsTIterates hΦ m κm κprev θ₀ θprev T) (t : ℝ) (ht : 0 < t) (x : Homogenization.Vec 2) (ρ : ℝ) (hρ : 0 < ρ) (LT LH : Homogenization.Vec 2 →L[ℝ] ℝ) (hTtime : HasDerivAt (fun (s : ℝ) => T (Nstar β) s x) (deriv (fun (s : ℝ) => T (Nstar β) s x) t) t) (hHtime : HasDerivAt (fun (s : ℝ) => I.Hm hΦ m κm (T (Nstar β)) s x) (deriv (fun (s : ℝ) => I.Hm hΦ m κm (T (Nstar β)) s x) t) t) (hξ : ∀ k ∈ xiMKNearSupportFinset I m t ρ, HasDerivAt (I.xiMK m k) (deriv (I.xiMK m k) t) t) (hTx : HasFDerivAt (T (Nstar β) t) LT x) (hHx : HasFDerivAt (I.Hm hΦ m κm (T (Nstar β)) t) LH x) (Lχ LG : ℤ → ℝ × Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2) (hχ : ∀ k ∈ xiMKNearSupportFinset I m t ρ, HasFDerivAt (Function.uncurry fun (s : ℝ) (y : Homogenization.Vec 2) => I.chiTilde hΦ m κm k s y) (Lχ k) (t, x)) (hG : ∀ k ∈ xiMKNearSupportFinset I m t ρ, HasFDerivAt (Function.uncurry fun (s : ℝ) (y : Homogenization.Vec 2) => G I hΦ m (T (Nstar β)) (lIdx β I.Λ m k) s y) (LG k) (t, x)) (Src : ℝ) (hsource : deriv (fun (s : ℝ) => T (Nstar β) s x) t + Homogenization.vecDot (streamVel (Φ (m - 1)) t x) (spaceGrad (T (Nstar β) t) x) + deriv (fun (s : ℝ) => I.Hm hΦ m κm (T (Nstar β)) s x) t + (fderiv ℝ (I.Hm hΦ m κm (T (Nstar β)) t) x) (streamVel (Φ (m - 1)) t x) = Src) : deriv (fun (s : ℝ) => I.ansatz hΦ m κm (T (Nstar β)) s x) t + Homogenization.vecDot (streamVel (Φ (m - 1)) t x) (spaceGrad (I.ansatz hΦ m κm (T (Nstar β)) t) x) = cutoff1 I hΦ m κm (T (Nstar β)) t x + ∑ q ∈ ⋯.toFinset, I.xiMK m (↑q) t * Homogenization.vecDot (fun (j : Fin 2) => deriv (fun (s : ℝ) => I.chiMK κm m (↑q) s (I.xFlowInv hΦ m (lIdx β I.Λ m ↑q) t x) j) t) (G I hΦ m (T (Nstar β)) (lIdx β I.Λ m ↑q) t x) + ∑ q ∈ ⋯.toFinset, I.xiMK m (↑q) t * Homogenization.vecDot (I.chiTilde hΦ m κm (↑q) t x) ((I.flowGrad hΦ m (lIdx β I.Λ m ↑q) t x).mulVec (gradDiv (fun (s : ℝ) (y : Homogenization.Vec 2) => (I.Kmat κm m s + I.sMat hΦ m κm s y).mulVec (spaceGrad (T (Nstar β) s) y) + iterateError I hΦ m κm κprev T s y) t x)) + Src

Source-generic ansatz material equation: the source transport equation for T_{m-1}+H_m may have an arbitrary real right-hand side Src, which appears unchanged in the material derivative of the ansatz.