Real-valued periodic integration by parts on the unit cell.

def AVenhance.Infra.Classical.PeriodicCalculus.closedUnitCell : Set (Homogenization.Vec 2)

Closed spatial unit cell used for compactness and periodic integration.

Equations

• AVenhance.Infra.Classical.PeriodicCalculus.closedUnitCell = Set.univ.pi fun (x : Fin 2) => Set.Icc 0 1

theorem AVenhance.Infra.Classical.PeriodicCalculus.isCompact_closedUnitCell : IsCompact closedUnitCell

theorem AVenhance.Infra.Classical.PeriodicCalculus.unitCell_subset_closedUnitCell : Torus.unitCell 2 ⊆ closedUnitCell

theorem AVenhance.Infra.Classical.PeriodicCalculus.continuous_integrableOn_unitCell {f : Homogenization.Vec 2 → ℝ} (hf : Continuous f) : MeasureTheory.IntegrableOn f (Torus.unitCell 2) MeasureTheory.volume

theorem AVenhance.Infra.Classical.integral_unitCell_coord_ibp_real (i : Fin 2) {f g : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ 1 f) (hg : ContDiff ℝ 1 g) (hpf : IsZ2Periodic f) (hpg : IsZ2Periodic g) : ∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, f x * spaceGrad g x i = -∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, spaceGrad f x i * g x

Real periodic integration by parts, transferred from the complex-valued torus calculus.

theorem AVenhance.Infra.Classical.PeriodicCalculus.spaceGrad_sq {w : Homogenization.Vec 2 → ℝ} (hw : ContDiff ℝ 1 w) (x : Homogenization.Vec 2) (i : Fin 2) : spaceGrad (fun (y : Homogenization.Vec 2) => w y ^ 2) x i = 2 * w x * spaceGrad w x i

theorem AVenhance.Infra.Classical.integral_unitCell_transport_energy_zero (b : Homogenization.Vec 2 → Homogenization.Vec 2) (hb : ContDiff ℝ 1 b) (hbp : ∀ (i : Fin 2), IsZ2Periodic fun (x : Homogenization.Vec 2) => b x i) (hdiv : ∀ (x : Homogenization.Vec 2), vecDiv b x = 0) (w : Homogenization.Vec 2 → ℝ) (hw : ContDiff ℝ 1 w) (hwp : IsZ2Periodic w) : ∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, Homogenization.vecDot (b x) (spaceGrad w x) * w x = 0

Smooth periodic transport contributes no quadratic energy on the unit torus when its classical divergence vanishes.

theorem AVenhance.Infra.Classical.streamVel_unitCell_transport_energy_zero (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (t : ℝ) (w : Homogenization.Vec 2 → ℝ) (hw : ContDiff ℝ 1 w) (hwp : IsZ2Periodic w) : ∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, Homogenization.vecDot (streamVel φ t x) (spaceGrad w x) * w x = 0

The admissible stream drift has vanishing quadratic transport energy for any smooth periodic test function on the torus.

theorem AVenhance.Infra.Classical.periodic_spaceGrad_component {f : Homogenization.Vec 2 → ℝ} (hper : IsZ2Periodic f) (i : Fin 2) : IsZ2Periodic fun (x : Homogenization.Vec 2) => spaceGrad f x i

Coordinate derivatives of a smooth periodic real function remain periodic.

theorem AVenhance.Infra.Classical.integral_unitCell_lap_mul {f g : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (hpf : IsZ2Periodic f) (hpg : IsZ2Periodic g) : ∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, f x * spaceLap g x = -∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, Homogenization.vecDot (spaceGrad f x) (spaceGrad g x)

The periodic Laplacian transfers one derivative to an independent test function.

theorem AVenhance.Infra.Classical.integral_unitCell_lap_energy {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hper : IsZ2Periodic f) : ∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, f x * spaceLap f x = -∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, Homogenization.vecDot (spaceGrad f x) (spaceGrad f x)

Spatial integration by parts gives the quadratic Laplacian energy identity on the unit cell.