The corrector and stream profile use the same scalar shear coordinate after composition with the inverse flow.

def AVenhance.Infra.Section5.FrozenShearOrthogonality.coordinateVector (c : Fin 2) (r : ℝ) : Homogenization.Vec 2

The coordinate vector with value r in coordinate c and zero in the other coordinate.

Equations

• AVenhance.Infra.Section5.FrozenShearOrthogonality.coordinateVector c r j = if j = c then r else 0

theorem AVenhance.Infra.Section5.FrozenShearOrthogonality.coordinateVector_contDiff (c : Fin 2) : ContDiff ℝ (↑⊤) (coordinateVector c)

theorem AVenhance.Infra.Section5.FrozenShearOrthogonality.psi_spatial_contDiff {β : ℝ} (I : Ingredients β) (m : ℕ) (k : ℤ) : ContDiff ℝ (↑⊤) (psi β I.Λ m k)

theorem AVenhance.Infra.Section5.frozen_shear_orthogonality_component {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (k : ℤ) (t : ℝ) (x : Homogenization.Vec 2) (i : Fin 2) : Homogenization.vecDot (spaceGrad (fun (y : Homogenization.Vec 2) => psi β I.Λ m k (I.xFlowInv hΦ m (lIdx β I.Λ m k) t y)) x) (sigmaMat.mulVec (spaceGrad (fun (y : Homogenization.Vec 2) => I.chiTilde hΦ m κ k t y i) x)) = 0

Orthogonality e.ortho.tilde for every component of the twisted corrector, with the exact common coordinate selected by k mod 4.