Explicit differential identities for the Section 3 shear fields.

theorem AVenhance.Infra.Section3.spaceGrad_sineCoordinate (A ω : ℝ) (i j : Fin 2) (x : Homogenization.Vec 2) : spaceGrad (fun (y : Homogenization.Vec 2) => A * Real.sin (ω * y i)) x j = if j = i then A * ω * Real.cos (ω * x i) else 0

theorem AVenhance.Infra.Section3.psi_sineCoordinate {β : ℝ} {Λ m : ℕ} (k : ℤ) (x : Homogenization.Vec 2) : psi β Λ m k x = a β Λ m * epsilon β Λ m ^ 2 * if k % 4 = 1 then Real.sin (2 * Real.pi / epsilon β Λ m * x 0) else if k % 4 = 3 then Real.sin (2 * Real.pi / epsilon β Λ m * x 1) else 0

The stream function is a coordinate sine (or zero), with frequency 2π/ε_m.

theorem AVenhance.Infra.Section3.psi_spaceGrad_formula {β : ℝ} {Λ m : ℕ} (k : ℤ) (x : Homogenization.Vec 2) (hε : epsilon β Λ m ≠ 0) : spaceGrad (psi β Λ m k) x = if k % 4 = 1 then ![a β Λ m * epsilon β Λ m * (2 * Real.pi) * Real.cos (2 * Real.pi * x 0 / epsilon β Λ m), 0] else if k % 4 = 3 then ![0, a β Λ m * epsilon β Λ m * (2 * Real.pi) * Real.cos (2 * Real.pi * x 1 / epsilon β Λ m)] else 0

The stream function is a single coordinate sine (or zero), with frequency 2π/ε_m.

theorem AVenhance.Infra.Section3.ShearFormula.sigmaMat_mulVec_formula (v : Homogenization.Vec 2) : sigmaMat.mulVec v = ![-v 1, v 0]

The rotation matrix is the counterclockwise quarter-turn.

theorem AVenhance.Infra.Section3.uShear_eq_sigma_spaceGrad {β : ℝ} {Λ m : ℕ} (k : ℤ) (x : Homogenization.Vec 2) (hε : epsilon β Λ m ≠ 0) : uShear β Λ m k x = sigmaMat.mulVec (spaceGrad (psi β Λ m k) x)

u_{m,k}=σ∇ψ_{m,k} (source e.ukm.explicit and e.def.streamr).