Statement file: uShear (Section3). This file contains exactly one declaration of the formalization's public statement surface.

noncomputable def AVenhance.uShear (β : ℝ) (Λ m : ℕ) (k : ℤ) (x : Homogenization.Vec 2) : Homogenization.Vec 2

e.ukm.explicit (label 2738, lines 2731-2749): u_{m,k} = ∇^⊥ ψ_{m,k}, written out: 2π a_m ε_m cos(2π x₁/ε_m) e₂ if k ∈ 4ℤ+1, -2π a_m ε_m cos(2π x₂/ε_m) e₁ if k ∈ 4ℤ+3, 0 if k ∈ 2ℤ.

Equations

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