Transport integration by parts for the material oscillatory terms in l.V.

theorem AVenhance.Infra.Section4.IteratesMaterial.material_cell_integrable {f : Homogenization.Vec 2 → ℝ} (hf : Continuous f) : MeasureTheory.IntegrableOn f unitCube MeasureTheory.volume

theorem AVenhance.Infra.Section4.IteratesMaterial.material_gradient_continuous {u : Homogenization.Vec 2 → ℝ} (hu : ContDiff ℝ (↑⊤) u) : Continuous (spaceGrad u)

theorem AVenhance.Infra.Section4.IteratesMaterial.material_stream_continuous {φ : Homogenization.Vec 2 → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) : Continuous (streamVel (fun (x : ℝ) => φ) 0)

theorem AVenhance.Infra.Section4.IteratesMaterial.material_dot_continuous {a b : Homogenization.Vec 2 → Homogenization.Vec 2} (ha : Continuous a) (hb : Continuous b) : Continuous fun (x : Homogenization.Vec 2) => Homogenization.vecDot (a x) (b x)

theorem AVenhance.Infra.Section4.iterate_amnrOp_timeOnly {b : AmnrSpace → Homogenization.Vec 2} {f : ℝ → ℝ} {z : AmnrSpace} (hf : DifferentiableAt ℝ f z.1) (d : Option (Fin 2)) : amnrOp b d (fun (y : AmnrSpace) => f y.1) z = match d with | none => deriv f z.1 | some val => 0

theorem AVenhance.Infra.Section4.iterate_stream_transport_pairing_skew {φ u v : Homogenization.Vec 2 → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφper : IsZ2Periodic φ) (hu : ContDiff ℝ (↑⊤) u) (hv : ContDiff ℝ (↑⊤) v) (hup : IsZ2Periodic u) (hvp : IsZ2Periodic v) : ∫ (x : Homogenization.Vec 2) in unitCube, u x * Homogenization.vecDot (streamVel (fun (x : ℝ) => φ) 0 x) (spaceGrad v x) = -∫ (x : Homogenization.Vec 2) in unitCube, v x * Homogenization.vecDot (streamVel (fun (x : ℝ) => φ) 0 x) (spaceGrad u x)

Polarization of the stream energy cancellation gives the transport integration by parts needed for two different increment derivatives.

theorem AVenhance.Infra.Section4.iterate_material_product_pairing {φ u v : ℝ → Homogenization.Vec 2 → ℝ} {t : ℝ} (hφ : ContDiff ℝ (↑⊤) (φ t)) (hφp : IsZ2Periodic (φ t)) (hu : ContDiff ℝ (↑⊤) (u t)) (hv : ContDiff ℝ (↑⊤) (v t)) (hup : IsZ2Periodic (u t)) (hvp : IsZ2Periodic (v t)) (huTime : MeasureTheory.IntegrableOn (fun (x : Homogenization.Vec 2) => v t x * deriv (fun (s : ℝ) => u s x) t) unitCube MeasureTheory.volume) (hvTime : MeasureTheory.IntegrableOn (fun (x : Homogenization.Vec 2) => u t x * deriv (fun (s : ℝ) => v s x) t) unitCube MeasureTheory.volume) : (∫ (x : Homogenization.Vec 2) in unitCube, u t x * amnrMaterial (streamVel φ) v t x) + ∫ (x : Homogenization.Vec 2) in unitCube, v t x * amnrMaterial (streamVel φ) u t x = (∫ (x : Homogenization.Vec 2) in unitCube, u t x * deriv (fun (s : ℝ) => v s x) t) + ∫ (x : Homogenization.Vec 2) in unitCube, v t x * deriv (fun (s : ℝ) => u s x) t

The material product pairing has exactly the same spatial integral as its temporal product pairing. The stream terms cancel by transport IBP.

theorem AVenhance.Infra.Section4.iterate_material_time_mul {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {q : ℝ → ℝ} {h : ℝ → Homogenization.Vec 2 → ℝ} {t : ℝ} {x : Homogenization.Vec 2} (hq : DifferentiableAt ℝ q t) (hh : DifferentiableAt ℝ (fun (z : AmnrSpace) => h z.1 z.2) (t, x)) : amnrMaterial b (fun (s : ℝ) (y : Homogenization.Vec 2) => q s * h s y) t x = deriv q t * h t x + q t * amnrMaterial b h t x

Material differentiation of a time coefficient times a space-time field. Only entrywise differentiability is needed; the drift is arbitrary.

theorem AVenhance.Infra.Section4.iterate_material_matrix_contract {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {Q : ℝ → Matrix (Fin 2) (Fin 2) ℝ} {H : ℝ → Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ} {t : ℝ} {x : Homogenization.Vec 2} (hQ : ∀ (i j : Fin 2), DifferentiableAt ℝ (fun (s : ℝ) => Q s i j) t) (hH : ∀ (i j : Fin 2), DifferentiableAt ℝ (fun (z : AmnrSpace) => H z.1 z.2 i j) (t, x)) : amnrMaterial b (fun (s : ℝ) (y : Homogenization.Vec 2) => ∑ i : Fin 2, ∑ j : Fin 2, Q s i j * H s y i j) t x = ∑ i : Fin 2, ∑ j : Fin 2, deriv (fun (s : ℝ) => Q s i j) t * H t x i j + ∑ i : Fin 2, ∑ j : Fin 2, Q t i j * amnrMaterial b (fun (s : ℝ) (y : Homogenization.Vec 2) => H s y i j) t x

The finite primitive/Hessian contraction obeys the material product rule. This is the algebra behind the first-increment half-square cancellation.