Material cancellation and bounds for the actual fast velocity increment.

theorem AVenhance.Infra.Section4.amnr_streamVel_sub {φ ψ : ℝ → Homogenization.Vec 2 → ℝ} (t : ℝ) (x : Homogenization.Vec 2) (hφ : DifferentiableAt ℝ (φ t) x) (hψ : DifferentiableAt ℝ (ψ t) x) : streamVel (fun (t : ℝ) (x : Homogenization.Vec 2) => φ t x - ψ t x) t x = streamVel φ t x - streamVel ψ t x

Rotation of the actual spatial gradient commutes with subtracting smooth scalar streams.

theorem AVenhance.Infra.Section4.amnr_streamIncrement_contDiff {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) : ContDiff ℝ ↑⊤ fun (z : AmnrSpace) => Φ m z.1 z.2 - Φ (m - 1) z.1 z.2

Smoothness of the actual scalar stream increment comes from the defining admissibility of its two streams.

theorem AVenhance.Infra.Section4.amnr_fastVelocity_component {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (i : Fin 2) : (fun (z : AmnrSpace) => streamVel (Φ m) z.1 z.2 i - streamVel (Φ (m - 1)) z.1 z.2 i) = (if i = 0 then -1 else 1) • amnrOp (fun (z : AmnrSpace) => streamVel (Φ (m - 1)) z.1 z.2) (some (if i = 0 then 1 else 0)) fun (z : AmnrSpace) => Φ m z.1 z.2 - Φ (m - 1) z.1 z.2

The actual fast velocity is the rotated spatial gradient of the actual stream increment, in the source's two coordinate conventions.

theorem AVenhance.Infra.Section4.amnr_amplitude_gradient_scale {E β : ℝ} (hE : 0 < E) : E ^ (β - 2) * E = E ^ (β - 1)

Abstract real conversion from the stream amplitude to its gradient rate.