Auxiliary facts for the stream-difference estimate

The slice identity ∫ σ∇ξ·∇θ ψ = ∫ ξ σ∇θ·∇ψ with its integrability, and basic regularity facts about an admissible stream.

theorem AVenhance.Infra.Section5.RelativeError.skew_flux_slice {ξ θ ψ : Homogenization.Vec 2 → ℝ} (hξ : Differentiable ℝ ξ) (hξp : IsZ2Periodic ξ) (hξb : ∀ (i : Fin 2), ∃ (C : ℝ), ∀ (x : Homogenization.Vec 2), |spaceGrad ξ x i| ≤ C) (hθ : ContDiff ℝ (↑⊤) θ) (hθp : IsZ2Periodic θ) (hψ : ContDiff ℝ (↑⊤) ψ) (hψp : IsZ2Periodic ψ) : MeasureTheory.IntegrableOn (fun (x : Homogenization.Vec 2) => Homogenization.vecDot (sigmaMat.mulVec (spaceGrad ξ x)) (spaceGrad θ x) * ψ x) unitCube MeasureTheory.volume ∧ ∫ (x : Homogenization.Vec 2) in unitCube, Homogenization.vecDot (sigmaMat.mulVec (spaceGrad ξ x)) (spaceGrad θ x) * ψ x = ∫ (x : Homogenization.Vec 2) in unitCube, Homogenization.vecDot (fun (i : Fin 2) => ξ x * sigmaMat.mulVec (spaceGrad θ x) i) (spaceGrad ψ x)

Cross transport σ∇ξ·∇θ ψ is integrable on the cell, and equals the flux pairing ξ σ∇θ·∇ψ.

theorem AVenhance.Infra.Section5.RelativeError.spaceGrad_sub_apply {f h : Homogenization.Vec 2 → ℝ} (hf : Differentiable ℝ f) (hh : Differentiable ℝ h) (x : Homogenization.Vec 2) (i : Fin 2) : spaceGrad (fun (y : Homogenization.Vec 2) => f y - h y) x i = spaceGrad f x i - spaceGrad h x i

The coordinates of the gradient of a difference.

theorem AVenhance.Infra.Section5.RelativeError.admissible_slice_contDiff {Ψ : ℝ → Homogenization.Vec 2 → ℝ} (hΨ : IsAdmissibleStream Ψ) (s : ℝ) : ContDiff ℝ (↑⊤) (Ψ s)

Time slices of an admissible stream are smooth.

theorem AVenhance.Infra.Section5.RelativeError.admissible_slice_periodic {Ψ : ℝ → Homogenization.Vec 2 → ℝ} (hΨ : IsAdmissibleStream Ψ) (s : ℝ) : IsZ2Periodic (Ψ s)

Time slices of an admissible stream are space periodic.

theorem AVenhance.Infra.Section5.RelativeError.smooth_periodic_grad_bound {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hp : IsZ2Periodic f) (i : Fin 2) : ∃ (C : ℝ), ∀ (x : Homogenization.Vec 2), |spaceGrad f x i| ≤ C

Gradient coordinates of a smooth periodic function are globally bounded.