Explicit one-dimensional calculations for a sinusoidal shear. The variable x is the unit-period fast coordinate x₁ / ε; spatial derivatives below are rescaled by ε⁻¹, so the formula keeps the source parameters a, ε, and κ.

noncomputable def AVenhance.Infra.Shear.streamProfile (a ε x : ℝ) : ℝ

Stream function profile a ε² sin (2π x) in the unit-period fast variable.

Equations

• AVenhance.Infra.Shear.streamProfile a ε x = a * ε ^ 2 * Real.sin (2 * Real.pi * x)

noncomputable def AVenhance.Infra.Shear.velocityProfile (a ε x : ℝ) : ℝ

The physical shear speed ∂ₓ₁ ψ = 2π a ε cos (2π x₁ / ε).

Equations

• AVenhance.Infra.Shear.velocityProfile a ε x = 2 * Real.pi * a * ε * Real.cos (2 * Real.pi * x)

noncomputable def AVenhance.Infra.Shear.stationaryCorrector (a ε κ x : ℝ) : ℝ

The stationary corrector for the second coordinate, with the sign solving -κ Δχ + u₂ = 0.

Equations

• AVenhance.Infra.Shear.stationaryCorrector a ε κ x = -(a * ε ^ 3 / (2 * Real.pi * κ)) * Real.cos (2 * Real.pi * x)

noncomputable def AVenhance.Infra.Shear.cellAverage (f : ℝ → ℝ) : ℝ

The spatial average over one period of the fast coordinate.

Equations

• AVenhance.Infra.Shear.cellAverage f = ∫ (x : ℝ) in 0..1, f x

@[simp]

theorem AVenhance.Infra.Shear.streamProfile_add_one (a ε x : ℝ) : streamProfile a ε (x + 1) = streamProfile a ε x

@[simp]

theorem AVenhance.Infra.Shear.velocityProfile_add_one (a ε x : ℝ) : velocityProfile a ε (x + 1) = velocityProfile a ε x

@[simp]

theorem AVenhance.Infra.Shear.stationaryCorrector_add_one (a ε κ x : ℝ) : stationaryCorrector a ε κ (x + 1) = stationaryCorrector a ε κ x

theorem AVenhance.Infra.Shear.average_sin_sq : (cellAverage fun (x : ℝ) => Real.sin (2 * Real.pi * x) ^ 2) = 1 / 2