Smooth periodic integration by parts on half-open fundamental cells.

noncomputable def AVenhance.Infra.Torus.coordDeriv {d : ℕ} (i : Fin d) (f : Homogenization.Vec d → ℂ) (x : Homogenization.Vec d) : ℂ

The classical coordinate derivative, evaluated in the unit coordinate direction.

Equations

• AVenhance.Infra.Torus.coordDeriv i f x = (fderiv ℝ f x) (Homogenization.basisVec i)

def AVenhance.Infra.Torus.Calculus.closedUnitCell (d : ℕ) : Set (Homogenization.Vec d)

Closed spatial unit cell used for compactness and periodic integration.

Equations

• AVenhance.Infra.Torus.Calculus.closedUnitCell d = Set.univ.pi fun (x : Fin d) => Set.Icc 0 1

theorem AVenhance.Infra.Torus.Calculus.isCompact_closedUnitCell (d : ℕ) : IsCompact (closedUnitCell d)

theorem AVenhance.Infra.Torus.Calculus.unitCell_subset_closedUnitCell (d : ℕ) : unitCell d ⊆ closedUnitCell d

theorem AVenhance.Infra.Torus.Calculus.continuous_integrableOn_unitCell {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] {f : Homogenization.Vec d → E} (hf : Continuous f) : MeasureTheory.IntegrableOn f (unitCell d) MeasureTheory.volume

theorem AVenhance.Infra.Torus.Calculus.insertNth_one_eq_integerTranslate {n : ℕ} (i : Fin (n + 1)) (z : Homogenization.Vec n) : i.insertNth 1 z = i.insertNth 0 z + intVector fun (j : Fin (n + 1)) => if j = i then 1 else 0

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

theorem AVenhance.Infra.Torus.Calculus.periodic_insertNth_endpoints {n : ℕ} (i : Fin (n + 1)) (z : Homogenization.Vec n) {f : Homogenization.Vec (n + 1) → ℂ} (hf : IsZdPeriodic f) : f (i.insertNth 1 z) = f (i.insertNth 0 z)

theorem AVenhance.Infra.Torus.Calculus.hasDerivAt_comp_insertNth_complex {n : ℕ} {f : Homogenization.Vec (n + 1) → ℂ} (hf : Differentiable ℝ f) (i : Fin (n + 1)) (z : Homogenization.Vec n) (t : ℝ) : HasDerivAt (fun (s : ℝ) => f (i.insertNth s z)) (coordDeriv i f (i.insertNth t z)) t

theorem AVenhance.Infra.Torus.Calculus.line_integral_ibp {n : ℕ} (i : Fin (n + 1)) {f g : Homogenization.Vec (n + 1) → ℂ} (hf : ContDiff ℝ 1 f) (hg : ContDiff ℝ 1 g) (hpf : IsZdPeriodic f) (hpg : IsZdPeriodic g) (z : Homogenization.Vec n) : ∫ (t : ℝ) in Set.Ioc 0 1, f (i.insertNth t z) * coordDeriv i g (i.insertNth t z) = -∫ (t : ℝ) in Set.Ioc 0 1, coordDeriv i f (i.insertNth t z) * g (i.insertNth t z)

theorem AVenhance.Infra.Torus.integral_unitCell_coord_ibp {n : ℕ} (i : Fin (n + 1)) {f g : Homogenization.Vec (n + 1) → ℂ} (hf : ContDiff ℝ 1 f) (hg : ContDiff ℝ 1 g) (hpf : IsZdPeriodic f) (hpg : IsZdPeriodic g) : ∫ (x : Homogenization.Vec (n + 1)) in unitCell (n + 1), f x * coordDeriv i g x = -∫ (x : Homogenization.Vec (n + 1)) in unitCell (n + 1), coordDeriv i f x * g x

Smooth periodic integration by parts on the ℤ^d unit cell.

theorem AVenhance.Infra.Torus.integral_unitCell_coord_deriv_eq_zero {n : ℕ} (i : Fin (n + 1)) {f : Homogenization.Vec (n + 1) → ℂ} (hf : ContDiff ℝ 1 f) (hpf : IsZdPeriodic f) : ∫ (x : Homogenization.Vec (n + 1)) in unitCell (n + 1), coordDeriv i f x = 0

Vanishing of the integral of any coordinate derivative of a smooth periodic complex-valued function over its unit cell.