Finite A/q aggregation for the H_{m,r} material step.

@[reducible, inline]

abbrev AVenhance.Infra.Section5.AmnrPairIndex : Type

Iteration index together with the two tensor indices of an Amnr pair.

Equations

• AVenhance.Infra.Section5.AmnrPairIndex = ((ℕ × Fin 2) × Fin 2)

def AVenhance.Infra.Section5.amnrPairSet (N : ℕ) : Finset AmnrPairIndex

All tensor-index pairs with iteration index below the specified cutoff.

Equations

• AVenhance.Infra.Section5.amnrPairSet N = (Finset.range N ×ˢ Finset.univ) ×ˢ Finset.univ

noncomputable def AVenhance.Infra.Section5.amnrPairFlux {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (r : ℕ) (a : AmnrPairIndex) (z : ST) : Homogenization.Vec 2

Flux of one Amnr tensor pair against the next time primitive.

Equations

• AVenhance.Infra.Section5.amnrPairFlux I hΦ m κ T r a z i = I.Amnr hΦ m κ a.1.1 T r z.1 z.2 i a.1.2 a.2 * I.qMNR κ m a.1.1 (r + 1) z.1 a.1.2 a.2

noncomputable def AVenhance.Infra.Section5.amnrPairIncrement {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (r : ℕ) (a : AmnrPairIndex) (z : ST) : Homogenization.Vec 2

Difference of consecutive Amnr tensor-pair contributions in the material recurrence.

Equations

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

noncomputable def AVenhance.Infra.Section5.amnrPairEndpointFlux {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (r : ℕ) (a : AmnrPairIndex) (z : ST) : Homogenization.Vec 2

Endpoint flux of one Amnr tensor pair against its current time primitive.

Equations

• AVenhance.Infra.Section5.amnrPairEndpointFlux I hΦ m κ T r a z i = I.Amnr hΦ m κ a.1.1 T r z.1 z.2 i a.1.2 a.2 * I.qMNR κ m a.1.1 r z.1 a.1.2 a.2

noncomputable def AVenhance.Infra.Section5.amnrPairFluxSum {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m N : ℕ) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (r : ℕ) (z : ST) : Homogenization.Vec 2

Sum of the Amnr pair fluxes below a finite iteration cutoff.

Equations

• AVenhance.Infra.Section5.amnrPairFluxSum I hΦ m N κ T r z = ∑ a ∈ AVenhance.Infra.Section5.amnrPairSet N, AVenhance.Infra.Section5.amnrPairFlux I hΦ m κ T r a z

noncomputable def AVenhance.Infra.Section5.amnrPairIncrementSum {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m N : ℕ) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (r : ℕ) (z : ST) : Homogenization.Vec 2

Sum of the Amnr pair increments below a finite iteration cutoff.

Equations

• AVenhance.Infra.Section5.amnrPairIncrementSum I hΦ m N κ T r z = ∑ a ∈ AVenhance.Infra.Section5.amnrPairSet N, AVenhance.Infra.Section5.amnrPairIncrement I hΦ m κ T r a z

noncomputable def AVenhance.Infra.Section5.amnrPairEndpointFluxSum {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m N : ℕ) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (r : ℕ) (z : ST) : Homogenization.Vec 2

Sum of the Amnr endpoint pair fluxes below a finite iteration cutoff.

Equations

• AVenhance.Infra.Section5.amnrPairEndpointFluxSum I hΦ m N κ T r z = ∑ a ∈ AVenhance.Infra.Section5.amnrPairSet N, AVenhance.Infra.Section5.amnrPairEndpointFlux I hΦ m κ T r a z

theorem AVenhance.Infra.Section5.stLieDerivative_finset_sum {ι : Type u_1} (S : Finset ι) (F : ι → ST → Homogenization.Vec 2) (b : ST → Homogenization.Vec 2) (p : ST) (hF : ∀ a ∈ S, DifferentiableAt ℝ (F a) p) : stLieDerivative (fun (z : ST) => ∑ a ∈ S, F a z) b p = ∑ a ∈ S, stLieDerivative (F a) b p

The row-corrected material derivative is linear over finite sums.

theorem AVenhance.Infra.Section5.frozen_amnr_fluxSum_material_increment {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m N : ℕ) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (r : ℕ) (p : ST) (hp : 0 < p.1) (hb : ContDiff ℝ 2 fun (z : ST) => streamVel (Φ (m - 1)) z.1 z.2) (hdiv : ∀ (z : ST), stDiv (fun (w : ST) => streamVel (Φ (m - 1)) w.1 w.2) z = 0) (hA : ∀ (n : ℕ) (i j k : Fin 2) (z : ST), 0 < z.1 → DifferentiableAt ℝ (fun (w : ST) => I.Amnr hΦ m κ n T r w.1 w.2 i j k) z) (hPair : ∀ (a : AmnrPairIndex) (z : ST), 0 < z.1 → DifferentiableAt ℝ (amnrPairFlux I hΦ m κ T r a) z) (hFlux : ContDiffAt ℝ 2 (amnrPairFluxSum I hΦ m N κ T r) p) : (fderiv ℝ (stDiv (amnrPairFluxSum I hΦ m N κ T r)) p) (1, streamVel (Φ (m - 1)) p.1 p.2) = stDiv (amnrPairIncrementSum I hΦ m N κ T r) p

and ∂ₜ q_{r+1}=-q_r aggregate to the material increment of the finite A_{m,n,r} q_{m,n,r+1} sum. The hypotheses expose only the smoothness needed to differentiate that finite flux and its factors.