Periodic integration by parts against a Lipschitz periodic function

The classical periodic integration by parts is available for C¹ factors. Here one factor is only differentiable with a bounded (measurable) partial derivative; the line integration by parts then still holds because the derivative is interval integrable.

theorem AVenhance.Infra.Section5.RelativeError.periodicFiniteUnitCube : MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict unitCube)

theorem AVenhance.Infra.Section5.RelativeError.ForcedEnergyPeriodic.insertNth_one_eq_shift (i : Fin 2) (z : Homogenization.Vec 1) : i.insertNth 1 z = i.insertNth 0 z + latticeShift fun (j : Fin 2) => if j = i then 1 else 0

The two endpoints of a coordinate insertion line differ by an integer shift.

theorem AVenhance.Infra.Section5.RelativeError.ForcedEnergyPeriodic.periodic_insertNth_endpoints (i : Fin 2) (z : Homogenization.Vec 1) {f : Homogenization.Vec 2 → ℝ} (hf : IsZ2Periodic f) : f (i.insertNth 1 z) = f (i.insertNth 0 z)

theorem AVenhance.Infra.Section5.RelativeError.measurable_spaceGrad_component (ξ : Homogenization.Vec 2 → ℝ) (i : Fin 2) : Measurable fun (x : Homogenization.Vec 2) => spaceGrad ξ x i

A partial derivative of a differentiable function is measurable.

theorem AVenhance.Infra.Section5.RelativeError.continuous_integrableOn_unitCube {f : Homogenization.Vec 2 → ℝ} (hf : Continuous f) : MeasureTheory.IntegrableOn f unitCube MeasureTheory.volume

A continuous function is integrable on the unit cube.

theorem AVenhance.Infra.Section5.RelativeError.integrableOn_unitCube_mul_continuous {a c : Homogenization.Vec 2 → ℝ} (ha : Measurable a) {C : ℝ} (hC : ∀ (x : Homogenization.Vec 2), |a x| ≤ C) (hc : Continuous c) : MeasureTheory.IntegrableOn (fun (x : Homogenization.Vec 2) => a x * c x) unitCube MeasureTheory.volume

A bounded measurable factor times a continuous factor is integrable on the unit cube.

theorem AVenhance.Infra.Section5.RelativeError.integral_cell_coord_ibp_differentiable (i : Fin 2) {ξ g : Homogenization.Vec 2 → ℝ} (hξ : Differentiable ℝ ξ) (hξp : IsZ2Periodic ξ) (hξb : ∃ (C : ℝ), ∀ (x : Homogenization.Vec 2), |spaceGrad ξ x i| ≤ C) (hg : ContDiff ℝ 1 g) (hgp : IsZ2Periodic g) : ∫ (x : Homogenization.Vec 2) in unitCube, ξ x * spaceGrad g x i = -∫ (x : Homogenization.Vec 2) in unitCube, spaceGrad ξ x i * g x

Periodic integration by parts in one coordinate, with a merely differentiable factor with bounded partial derivative.

theorem AVenhance.Infra.Section5.RelativeError.spaceGrad_mixed_symm {θ : Homogenization.Vec 2 → ℝ} (hθ : ContDiff ℝ 2 θ) (x : Homogenization.Vec 2) (i j : Fin 2) : spaceGrad (fun (y : Homogenization.Vec 2) => spaceGrad θ y j) x i = spaceGrad (fun (y : Homogenization.Vec 2) => spaceGrad θ y i) x j

Mixed partial derivatives of a C² function commute.

theorem AVenhance.Infra.Section5.RelativeError.spaceGrad_component_continuous' {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ 1 f) (j : Fin 2) : Continuous fun (x : Homogenization.Vec 2) => spaceGrad f x j

theorem AVenhance.Infra.Section5.RelativeError.sigmaMat_mulVec_apply_zero (a : Homogenization.Vec 2) : sigmaMat.mulVec a 0 = -a 1

The coordinates of σ a.

theorem AVenhance.Infra.Section5.RelativeError.sigmaMat_mulVec_apply_one (a : Homogenization.Vec 2) : sigmaMat.mulVec a 1 = a 0

theorem AVenhance.Infra.Section5.RelativeError.spaceGrad_mul_apply {ψ k : Homogenization.Vec 2 → ℝ} (hψ : Differentiable ℝ ψ) (hk : Differentiable ℝ k) (x : Homogenization.Vec 2) (i : Fin 2) : spaceGrad (fun (y : Homogenization.Vec 2) => ψ y * k y) x i = spaceGrad ψ x i * k x + ψ x * spaceGrad k x i

Product rule for coordinate derivatives.

theorem AVenhance.Infra.Section5.RelativeError.spaceGrad_contDiff_component {θ : Homogenization.Vec 2 → ℝ} {n : ℕ} (hθ : ContDiff ℝ (↑(n + 1)) θ) (j : Fin 2) : ContDiff ℝ ↑n fun (x : Homogenization.Vec 2) => spaceGrad θ x j

theorem AVenhance.Infra.Section5.RelativeError.skew_flux_cell_identity {ξ θ ψ : Homogenization.Vec 2 → ℝ} (hξ : Differentiable ℝ ξ) (hξp : IsZ2Periodic ξ) (hξb : ∀ (i : Fin 2), ∃ (C : ℝ), ∀ (x : Homogenization.Vec 2), |spaceGrad ξ x i| ≤ C) (hθ : ContDiff ℝ 2 θ) (hθp : IsZ2Periodic θ) (hψ : ContDiff ℝ 1 ψ) (hψp : IsZ2Periodic ψ) : ∫ (x : Homogenization.Vec 2) in unitCube, Homogenization.vecDot (sigmaMat.mulVec (spaceGrad ξ x)) (spaceGrad θ x) * ψ x = ∫ (x : Homogenization.Vec 2) in unitCube, ξ x * Homogenization.vecDot (sigmaMat.mulVec (spaceGrad θ x)) (spaceGrad ψ x)

Skew cancellation: the flux ξ σ ∇θ represents the transport σ∇ξ·∇θ against any periodic test, for periodic C² functions θ and a merely Lipschitz periodic ξ.